Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 13

This is the task corresponding to homework 13.

Resources

Download Files

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

Terms and Conditions