src/HOL/IMP/AExp.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 45216 a51a70687517 child 45238 ed2bb3b58cc4 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
 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@45212 7 type_synonym vname = string nipkow@43141 8 type_synonym val = int nipkow@45212 9 type_synonym state = "vname \ val" nipkow@43141 10 nipkow@45212 11 datatype aexp = N int | V vname | Plus aexp aexp nipkow@43141 12 nipkow@43141 13 fun aval :: "aexp \ state \ val" where nipkow@45216 14 "aval (N n) s = 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@44923 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: *} nipkow@44923 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 nipkow@44923 26 definition null_state ("<>") where nipkow@44923 27 "null_state \ \x. 0" kleing@44036 28 syntax kleing@44036 29 "_State" :: "updbinds => 'a" ("<_>") kleing@43158 30 translations nipkow@44923 31 "_State ms" => "_Update <> 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 *} nipkow@44923 36 lemma " = (<> (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 nipkow@44923 41 kleing@43158 42 text {* Variables that are not mentioned in the state are 0 by default in kleing@44036 43 the @{term ""} syntax: nipkow@44923 44 *} kleing@44036 45 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" nipkow@43141 46 nipkow@44923 47 text{* Note that this @{text"<\>"} syntax works for any function space nipkow@44923 48 @{text"\\<^isub>1 \ \\<^isub>2"} where @{text "\\<^isub>2"} has a @{text 0}. *} nipkow@44923 49 nipkow@43141 50 nipkow@43141 51 subsection "Optimization" nipkow@43141 52 nipkow@43141 53 text{* Evaluate constant subsexpressions: *} nipkow@43141 54 nipkow@43141 55 fun asimp_const :: "aexp \ aexp" where nipkow@43141 56 "asimp_const (N n) = N n" | nipkow@43141 57 "asimp_const (V x) = V x" | nipkow@43141 58 "asimp_const (Plus a1 a2) = nipkow@43141 59 (case (asimp_const a1, asimp_const a2) of nipkow@43141 60 (N n1, N n2) \ N(n1+n2) | nipkow@43141 61 (a1',a2') \ Plus a1' a2')" nipkow@43141 62 nipkow@43141 63 theorem aval_asimp_const[simp]: nipkow@43141 64 "aval (asimp_const a) s = aval a s" nipkow@45015 65 apply(induction a) nipkow@43141 66 apply (auto split: aexp.split) nipkow@43141 67 done nipkow@43141 68 nipkow@43141 69 text{* Now we also eliminate all occurrences 0 in additions. The standard nipkow@43141 70 method: optimized versions of the constructors: *} nipkow@43141 71 nipkow@43141 72 fun plus :: "aexp \ aexp \ aexp" where nipkow@43141 73 "plus (N i1) (N i2) = N(i1+i2)" | nipkow@43141 74 "plus (N i) a = (if i=0 then a else Plus (N i) a)" | nipkow@43141 75 "plus a (N i) = (if i=0 then a else Plus a (N i))" | nipkow@43141 76 "plus a1 a2 = Plus a1 a2" nipkow@43141 77 nipkow@43141 78 lemma aval_plus[simp]: nipkow@43141 79 "aval (plus a1 a2) s = aval a1 s + aval a2 s" nipkow@45015 80 apply(induction a1 a2 rule: plus.induct) nipkow@43141 81 apply simp_all (* just for a change from auto *) nipkow@43141 82 done nipkow@43141 83 nipkow@43141 84 fun asimp :: "aexp \ aexp" where nipkow@43141 85 "asimp (N n) = N n" | nipkow@43141 86 "asimp (V x) = V x" | nipkow@43141 87 "asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)" nipkow@43141 88 nipkow@43141 89 text{* Note that in @{const asimp_const} the optimized constructor was nipkow@43141 90 inlined. Making it a separate function @{const plus} improves modularity of nipkow@43141 91 the code and the proofs. *} nipkow@43141 92 nipkow@43141 93 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" nipkow@43141 94 nipkow@43141 95 theorem aval_asimp[simp]: nipkow@43141 96 "aval (asimp a) s = aval a s" nipkow@45015 97 apply(induction a) nipkow@43141 98 apply simp_all nipkow@43141 99 done nipkow@43141 100 nipkow@43141 101 end