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