1(* Title: ZF/IMP/Com.thy 2 Author: Heiko Loetzbeyer and Robert Sandner, TU M��nchen 3*) 4 5section \<open>Arithmetic expressions, boolean expressions, commands\<close> 6 7theory Com imports ZF begin 8 9 10subsection \<open>Arithmetic expressions\<close> 11 12consts 13 loc :: i 14 aexp :: i 15 16datatype \<subseteq> "univ(loc \<union> (nat -> nat) \<union> ((nat \<times> nat) -> nat))" 17 aexp = N ("n \<in> nat") 18 | X ("x \<in> loc") 19 | Op1 ("f \<in> nat -> nat", "a \<in> aexp") 20 | Op2 ("f \<in> (nat \<times> nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp") 21 22 23consts evala :: i 24 25abbreviation 26 evala_syntax :: "[i, i] => o" (infixl \<open>-a->\<close> 50) 27 where "p -a-> n == <p,n> \<in> evala" 28 29inductive 30 domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat" 31 intros 32 N: "[| n \<in> nat; sigma \<in> loc->nat |] ==> <N(n),sigma> -a-> n" 33 X: "[| x \<in> loc; sigma \<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x" 34 Op1: "[| <e,sigma> -a-> n; f \<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n" 35 Op2: "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \<in> (nat\<times>nat) -> nat |] 36 ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>" 37 type_intros aexp.intros apply_funtype 38 39 40subsection \<open>Boolean expressions\<close> 41 42consts bexp :: i 43 44datatype \<subseteq> "univ(aexp \<union> ((nat \<times> nat)->bool))" 45 bexp = true 46 | false 47 | ROp ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp") 48 | noti ("b \<in> bexp") 49 | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl \<open>andi\<close> 60) 50 | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl \<open>ori\<close> 60) 51 52 53consts evalb :: i 54 55abbreviation 56 evalb_syntax :: "[i,i] => o" (infixl \<open>-b->\<close> 50) 57 where "p -b-> b == <p,b> \<in> evalb" 58 59inductive 60 domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool" 61 intros 62 true: "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1" 63 false: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0" 64 ROp: "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |] 65 ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> " 66 noti: "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)" 67 andi: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 68 ==> <b0 andi b1,sigma> -b-> (w0 and w1)" 69 ori: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 70 ==> <b0 ori b1,sigma> -b-> (w0 or w1)" 71 type_intros bexp.intros 72 apply_funtype and_type or_type bool_1I bool_0I not_type 73 type_elims evala.dom_subset [THEN subsetD, elim_format] 74 75 76subsection \<open>Commands\<close> 77 78consts com :: i 79datatype com = 80 skip (\<open>\<SKIP>\<close> []) 81 | assignment ("x \<in> loc", "a \<in> aexp") (infixl \<open>\<ASSN>\<close> 60) 82 | semicolon ("c0 \<in> com", "c1 \<in> com") (\<open>_\<SEQ> _\<close> [60, 60] 10) 83 | while ("b \<in> bexp", "c \<in> com") (\<open>\<WHILE> _ \<DO> _\<close> 60) 84 | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") (\<open>\<IF> _ \<THEN> _ \<ELSE> _\<close> 60) 85 86 87consts evalc :: i 88 89abbreviation 90 evalc_syntax :: "[i, i] => o" (infixl \<open>-c->\<close> 50) 91 where "p -c-> s == <p,s> \<in> evalc" 92 93inductive 94 domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)" 95 intros 96 skip: "[| sigma \<in> loc -> nat |] ==> <\<SKIP>,sigma> -c-> sigma" 97 98 assign: "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |] 99 ==> <x \<ASSN> a,sigma> -c-> sigma(x:=m)" 100 101 semi: "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] 102 ==> <c0\<SEQ> c1, sigma> -c-> sigma1" 103 104 if1: "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat; 105 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] 106 ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1" 107 108 if0: "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat; 109 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] 110 ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1" 111 112 while0: "[| c \<in> com; <b, sigma> -b-> 0 |] 113 ==> <\<WHILE> b \<DO> c,sigma> -c-> sigma" 114 115 while1: "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 116 <\<WHILE> b \<DO> c, sigma2> -c-> sigma1 |] 117 ==> <\<WHILE> b \<DO> c, sigma> -c-> sigma1" 118 119 type_intros com.intros update_type 120 type_elims evala.dom_subset [THEN subsetD, elim_format] 121 evalb.dom_subset [THEN subsetD, elim_format] 122 123 124subsection \<open>Misc lemmas\<close> 125 126lemmas evala_1 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1] 127 and evala_2 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2] 128 and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2] 129 130lemmas evalb_1 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1] 131 and evalb_2 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2] 132 and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2] 133 134lemmas evalc_1 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1] 135 and evalc_2 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2] 136 and evalc_3 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD2] 137 138inductive_cases 139 evala_N_E [elim!]: "<N(n),sigma> -a-> i" 140 and evala_X_E [elim!]: "<X(x),sigma> -a-> i" 141 and evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i" 142 and evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i" 143 144end 145