src/HOL/IMP/AExp.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 44036 d03f9f28d01d child 44923 b80108b346a9 permissions -rw-r--r--
remove lemma stupid_ext
 nipkow@43141 ` 1` ```header "Arithmetic and Boolean Expressions" ``` nipkow@43141 ` 2` nipkow@43141 ` 3` ```theory AExp imports Main begin ``` nipkow@43141 ` 4` nipkow@43141 ` 5` ```subsection "Arithmetic Expressions" ``` nipkow@43141 ` 6` nipkow@43141 ` 7` ```type_synonym name = string ``` nipkow@43141 ` 8` ```type_synonym val = int ``` nipkow@43141 ` 9` ```type_synonym state = "name \ val" ``` nipkow@43141 ` 10` nipkow@43141 ` 11` ```datatype aexp = N int | V name | Plus aexp aexp ``` nipkow@43141 ` 12` nipkow@43141 ` 13` ```fun aval :: "aexp \ state \ val" where ``` nipkow@43141 ` 14` ```"aval (N n) _ = n" | ``` nipkow@43141 ` 15` ```"aval (V x) s = s x" | ``` nipkow@43141 ` 16` ```"aval (Plus a1 a2) s = aval a1 s + aval a2 s" ``` nipkow@43141 ` 17` nipkow@43141 ` 18` nipkow@43141 ` 19` ```value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)" ``` nipkow@43141 ` 20` kleing@43158 ` 21` ```text {* The same state more concisely: *} ``` kleing@43158 ` 22` ```value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))" ``` kleing@43158 ` 23` kleing@43158 ` 24` ```text {* A little syntax magic to write larger states compactly: *} ``` kleing@43158 ` 25` kleing@43250 ` 26` ```definition ``` kleing@43250 ` 27` ``` "null_heap \ \x. 0" ``` kleing@44036 ` 28` ```syntax ``` kleing@44036 ` 29` ``` "_State" :: "updbinds => 'a" ("<_>") ``` kleing@43158 ` 30` ```translations ``` kleing@44036 ` 31` ``` "_State ms" => "_Update (CONST null_heap) ms" ``` nipkow@43141 ` 32` kleing@43158 ` 33` ```text {* ``` kleing@43158 ` 34` ``` We can now write a series of updates to the function @{text "\x. 0"} compactly: ``` kleing@43158 ` 35` ```*} ``` kleing@44036 ` 36` ```lemma " = (null_heap (a := Suc 0)) (b := 2)" ``` kleing@43158 ` 37` ``` by (rule refl) ``` kleing@43158 ` 38` kleing@44036 ` 39` ```value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" ``` kleing@43158 ` 40` kleing@43158 ` 41` ```text {* Variables that are not mentioned in the state are 0 by default in ``` kleing@44036 ` 42` ``` the @{term ""} syntax: ``` kleing@43158 ` 43` ```*} ``` kleing@44036 ` 44` ```value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" ``` nipkow@43141 ` 45` nipkow@43141 ` 46` nipkow@43141 ` 47` ```subsection "Optimization" ``` nipkow@43141 ` 48` nipkow@43141 ` 49` ```text{* Evaluate constant subsexpressions: *} ``` nipkow@43141 ` 50` nipkow@43141 ` 51` ```fun asimp_const :: "aexp \ aexp" where ``` nipkow@43141 ` 52` ```"asimp_const (N n) = N n" | ``` nipkow@43141 ` 53` ```"asimp_const (V x) = V x" | ``` nipkow@43141 ` 54` ```"asimp_const (Plus a1 a2) = ``` nipkow@43141 ` 55` ``` (case (asimp_const a1, asimp_const a2) of ``` nipkow@43141 ` 56` ``` (N n1, N n2) \ N(n1+n2) | ``` nipkow@43141 ` 57` ``` (a1',a2') \ Plus a1' a2')" ``` nipkow@43141 ` 58` nipkow@43141 ` 59` ```theorem aval_asimp_const[simp]: ``` nipkow@43141 ` 60` ``` "aval (asimp_const a) s = aval a s" ``` nipkow@43141 ` 61` ```apply(induct a) ``` nipkow@43141 ` 62` ```apply (auto split: aexp.split) ``` nipkow@43141 ` 63` ```done ``` nipkow@43141 ` 64` nipkow@43141 ` 65` ```text{* Now we also eliminate all occurrences 0 in additions. The standard ``` nipkow@43141 ` 66` ```method: optimized versions of the constructors: *} ``` nipkow@43141 ` 67` nipkow@43141 ` 68` ```fun plus :: "aexp \ aexp \ aexp" where ``` nipkow@43141 ` 69` ```"plus (N i1) (N i2) = N(i1+i2)" | ``` nipkow@43141 ` 70` ```"plus (N i) a = (if i=0 then a else Plus (N i) a)" | ``` nipkow@43141 ` 71` ```"plus a (N i) = (if i=0 then a else Plus a (N i))" | ``` nipkow@43141 ` 72` ```"plus a1 a2 = Plus a1 a2" ``` nipkow@43141 ` 73` nipkow@43141 ` 74` ```code_thms plus ``` nipkow@43141 ` 75` ```code_thms plus ``` nipkow@43141 ` 76` nipkow@43141 ` 77` ```(* FIXME: dropping subsumed code eqns?? *) ``` nipkow@43141 ` 78` ```lemma aval_plus[simp]: ``` nipkow@43141 ` 79` ``` "aval (plus a1 a2) s = aval a1 s + aval a2 s" ``` nipkow@43141 ` 80` ```apply(induct a1 a2 rule: plus.induct) ``` nipkow@43141 ` 81` ```apply simp_all (* just for a change from auto *) ``` nipkow@43141 ` 82` ```done ``` nipkow@43141 ` 83` ```code_thms plus ``` nipkow@43141 ` 84` nipkow@43141 ` 85` ```fun asimp :: "aexp \ aexp" where ``` nipkow@43141 ` 86` ```"asimp (N n) = N n" | ``` nipkow@43141 ` 87` ```"asimp (V x) = V x" | ``` nipkow@43141 ` 88` ```"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)" ``` nipkow@43141 ` 89` nipkow@43141 ` 90` ```text{* Note that in @{const asimp_const} the optimized constructor was ``` nipkow@43141 ` 91` ```inlined. Making it a separate function @{const plus} improves modularity of ``` nipkow@43141 ` 92` ```the code and the proofs. *} ``` nipkow@43141 ` 93` nipkow@43141 ` 94` ```value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" ``` nipkow@43141 ` 95` nipkow@43141 ` 96` ```theorem aval_asimp[simp]: ``` nipkow@43141 ` 97` ``` "aval (asimp a) s = aval a s" ``` nipkow@43141 ` 98` ```apply(induct a) ``` nipkow@43141 ` 99` ```apply simp_all ``` nipkow@43141 ` 100` ```done ``` nipkow@43141 ` 101` nipkow@43141 ` 102` ```end ```