Theory Com
section ‹Arithmetic expressions, boolean expressions, commands›
theory Com imports ZF begin
subsection ‹Arithmetic expressions›
consts
loc :: i
aexp :: i
datatype ⊆ "univ(loc ∪ (nat -> nat) ∪ ((nat × nat) -> nat))"
aexp = N ("n ∈ nat")
| X ("x ∈ loc")
| Op1 ("f ∈ nat -> nat", "a ∈ aexp")
| Op2 ("f ∈ (nat × nat) -> nat", "a0 ∈ aexp", "a1 ∈ aexp")
consts evala :: i
abbreviation
evala_syntax :: "[i, i] ⇒ o" (infixl ‹-a->› 50)
where "p -a-> n ≡ ⟨p,n⟩ ∈ evala"
inductive
domains "evala" ⊆ "(aexp × (loc -> nat)) × nat"
intros
N: "⟦n ∈ nat; sigma ∈ loc->nat⟧ ⟹ <N(n),sigma> -a-> n"
X: "⟦x ∈ loc; sigma ∈ loc->nat⟧ ⟹ <X(x),sigma> -a-> sigma`x"
Op1: "⟦⟨e,sigma⟩ -a-> n; f ∈ nat -> nat⟧ ⟹ <Op1(f,e),sigma> -a-> f`n"
Op2: "⟦⟨e0,sigma⟩ -a-> n0; ⟨e1,sigma⟩ -a-> n1; f ∈ (nat×nat) -> nat⟧
⟹ <Op2(f,e0,e1),sigma> -a-> f`⟨n0,n1⟩"
type_intros aexp.intros apply_funtype
subsection ‹Boolean expressions›
consts bexp :: i
datatype ⊆ "univ(aexp ∪ ((nat × nat)->bool))"
bexp = true
| false
| ROp ("f ∈ (nat × nat)->bool", "a0 ∈ aexp", "a1 ∈ aexp")
| noti ("b ∈ bexp")
| andi ("b0 ∈ bexp", "b1 ∈ bexp") (infixl ‹andi› 60)
| ori ("b0 ∈ bexp", "b1 ∈ bexp") (infixl ‹ori› 60)
consts evalb :: i
abbreviation
evalb_syntax :: "[i,i] ⇒ o" (infixl ‹-b->› 50)
where "p -b-> b ≡ ⟨p,b⟩ ∈ evalb"
inductive
domains "evalb" ⊆ "(bexp × (loc -> nat)) × bool"
intros
true: "⟦sigma ∈ loc -> nat⟧ ⟹ ⟨true,sigma⟩ -b-> 1"
false: "⟦sigma ∈ loc -> nat⟧ ⟹ ⟨false,sigma⟩ -b-> 0"
ROp: "⟦⟨a0,sigma⟩ -a-> n0; ⟨a1,sigma⟩ -a-> n1; f ∈ (nat*nat)->bool⟧
⟹ <ROp(f,a0,a1),sigma> -b-> f`⟨n0,n1⟩ "
noti: "⟦⟨b,sigma⟩ -b-> w⟧ ⟹ <noti(b),sigma> -b-> not(w)"
andi: "⟦⟨b0,sigma⟩ -b-> w0; ⟨b1,sigma⟩ -b-> w1⟧
⟹ <b0 andi b1,sigma> -b-> (w0 and w1)"
ori: "⟦⟨b0,sigma⟩ -b-> w0; ⟨b1,sigma⟩ -b-> w1⟧
⟹ <b0 ori b1,sigma> -b-> (w0 or w1)"
type_intros bexp.intros
apply_funtype and_type or_type bool_1I bool_0I not_type
type_elims evala.dom_subset [THEN subsetD, elim_format]
subsection ‹Commands›
consts com :: i
datatype com =
skip (‹\<SKIP>› [])
| assignment ("x ∈ loc", "a ∈ aexp") (infixl ‹\<ASSN>› 60)
| semicolon ("c0 ∈ com", "c1 ∈ com") (‹_\<SEQ> _› [60, 60] 10)
| while ("b ∈ bexp", "c ∈ com") (‹\<WHILE> _ \<DO> _› 60)
| "if" ("b ∈ bexp", "c0 ∈ com", "c1 ∈ com") (‹\<IF> _ \<THEN> _ \<ELSE> _› 60)
consts evalc :: i
abbreviation
evalc_syntax :: "[i, i] ⇒ o" (infixl ‹-c->› 50)
where "p -c-> s ≡ ⟨p,s⟩ ∈ evalc"
inductive
domains "evalc" ⊆ "(com × (loc -> nat)) × (loc -> nat)"
intros
skip: "⟦sigma ∈ loc -> nat⟧ ⟹ <\<SKIP>,sigma> -c-> sigma"
assign: "⟦m ∈ nat; x ∈ loc; ⟨a,sigma⟩ -a-> m⟧
⟹ <x \<ASSN> a,sigma> -c-> sigma(x:=m)"
semi: "⟦⟨c0,sigma⟩ -c-> sigma2; ⟨c1,sigma2⟩ -c-> sigma1⟧
⟹ <c0\<SEQ> c1, sigma> -c-> sigma1"
if1: "⟦b ∈ bexp; c1 ∈ com; sigma ∈ loc->nat;
⟨b,sigma⟩ -b-> 1; ⟨c0,sigma⟩ -c-> sigma1⟧
⟹ <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"
if0: "⟦b ∈ bexp; c0 ∈ com; sigma ∈ loc->nat;
⟨b,sigma⟩ -b-> 0; ⟨c1,sigma⟩ -c-> sigma1⟧
⟹ <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"
while0: "⟦c ∈ com; ⟨b, sigma⟩ -b-> 0⟧
⟹ <\<WHILE> b \<DO> c,sigma> -c-> sigma"
while1: "⟦c ∈ com; ⟨b,sigma⟩ -b-> 1; ⟨c,sigma⟩ -c-> sigma2;
<\<WHILE> b \<DO> c, sigma2> -c-> sigma1⟧
⟹ <\<WHILE> b \<DO> c, sigma> -c-> sigma1"
type_intros com.intros update_type
type_elims evala.dom_subset [THEN subsetD, elim_format]
evalb.dom_subset [THEN subsetD, elim_format]
subsection ‹Misc lemmas›
lemmas evala_1 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
and evala_2 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2]
lemmas evalb_1 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
and evalb_2 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2]
lemmas evalc_1 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
and evalc_2 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
and evalc_3 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD2]
inductive_cases
evala_N_E [elim!]: "<N(n),sigma> -a-> i"
and evala_X_E [elim!]: "<X(x),sigma> -a-> i"
and evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
and evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i"
end