Homework 13

Definitions File

theory Defs
  imports "HOL-IMP.Abs_Int1" Complex_Main
begin

datatype bits = Zero | Pos nat | Neg nat | Either nat | Any

fun \<gamma>_bits :: "bits \<Rightarrow> val set" where
"\<gamma>_bits Any = UNIV" |
"\<gamma>_bits Zero = {0}" |
"\<gamma>_bits (Pos b) = {i. i \<ge> 0 \<and> \<bar>i\<bar> < 2^Suc b }" |
"\<gamma>_bits (Neg b) = {i. i \<le> 0 \<and> \<bar>i\<bar> < 2^Suc b }" |
"\<gamma>_bits (Either b) = {i. \<bar>i\<bar> < 2^Suc b}"


consts num_bits :: "val \<Rightarrow> bits"

consts plus_bits :: "bits \<Rightarrow> bits \<Rightarrow> bits"


end

Template File

theory Submission
  imports Defs
begin

instantiation bits :: order
begin

instance sorry

end

instantiation bits :: semilattice_sup_top
begin

instance sorry

end

fun num_bits :: "val \<Rightarrow> bits"  where
  "num_bits _ = Any"

value "num_bits 0 = Zero"
value "num_bits 3 = Pos 1"
value "num_bits (-42) = Neg 5"

locale bounded_bits = fixes bits :: nat
begin

fun plus_bits :: "bits \<Rightarrow> bits \<Rightarrow> bits"  where
  "plus_bits _ _ = Any"

sublocale Val_semilattice
  where \<gamma> = \<gamma>_bits and num' = num_bits and plus' = plus_bits
  sorry

sublocale Abs_Int
  where \<gamma> = \<gamma>_bits and num' = num_bits and plus' = plus_bits
  sorry

sublocale Abs_Int_mono
  where \<gamma> = \<gamma>_bits and num' = num_bits and plus' = plus_bits
  sorry

end

global_interpretation bounded_bits
  where bits="Suc (Suc (Suc 0))"
  defines AI_bits4 = AI and step_bits4 = step' and aval'_bits4 = aval'
  done

definition "steps c i = (step_bits4 \<top> ^^ i) (Abs_Int0.bot c)"

definition "test1_bits =
 ''y'' ::= N 7;;
 ''z'' ::= Plus (V ''y'') (N 2);;
 ''y'' ::= Plus (V ''x'') (N 0)"

value "show_acom (steps test1_bits 0)"
value "show_acom (steps test1_bits 1)"
value "show_acom (steps test1_bits 2)"
value "show_acom (steps test1_bits 3)"

value "show_acom (the (AI_bits4 test1_bits))"

end

Check File

theory Check
  imports Submission
begin

end