(* Title: ZF/IMP/Com.thy ID: $Id: Com.thy,v 1.19 2005/06/17 14:15:10 haftmann Exp $ Author: Heiko Loetzbeyer and Robert Sandner, TU München *) header {* Arithmetic expressions, boolean expressions, commands *} theory Com imports Main 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 syntax "_evala" :: "[i, i] => o" (infixl "-a->" 50) translations "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 60) | ori ("b0 ∈ bexp", "b1 ∈ bexp") (infixl 60) consts evalb :: i syntax "_evalb" :: "[i,i] => o" (infixl "-b->" 50) translations "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 syntax "_evalc" :: "[i, i] => o" (infixl "-c->" 50) translations "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
lemmas evala_1:
〈a, b〉 -a-> b1 ==> a ∈ aexp
and evala_2:
〈a, b〉 -a-> b1 ==> b ∈ loc -> nat
and evala_3:
a -a-> b ==> b ∈ nat
lemmas evala_1:
〈a, b〉 -a-> b1 ==> a ∈ aexp
and evala_2:
〈a, b〉 -a-> b1 ==> b ∈ loc -> nat
and evala_3:
a -a-> b ==> b ∈ nat
lemmas evalb_1:
〈a, b〉 -b-> b1 ==> a ∈ bexp
and evalb_2:
〈a, b〉 -b-> b1 ==> b ∈ loc -> nat
and evalb_3:
a -b-> b ==> b ∈ bool
lemmas evalb_1:
〈a, b〉 -b-> b1 ==> a ∈ bexp
and evalb_2:
〈a, b〉 -b-> b1 ==> b ∈ loc -> nat
and evalb_3:
a -b-> b ==> b ∈ bool
lemmas evalc_1:
〈a, b〉 -c-> b1 ==> a ∈ com
and evalc_2:
〈a, b〉 -c-> b1 ==> b ∈ loc -> nat
and evalc_3:
a -c-> b ==> b ∈ loc -> nat
lemmas evalc_1:
〈a, b〉 -c-> b1 ==> a ∈ com
and evalc_2:
〈a, b〉 -c-> b1 ==> b ∈ loc -> nat
and evalc_3:
a -c-> b ==> b ∈ loc -> nat
lemmas evala_N_E:
[| 〈N(n), sigma〉 -a-> i; [| i ∈ nat; sigma ∈ loc -> nat; n = i |] ==> Q |] ==> Q
and evala_X_E:
[| 〈X(x), sigma〉 -a-> i; [| x ∈ loc; sigma ∈ loc -> nat; i = sigma ` x |] ==> Q |] ==> Q
and evala_Op1_E:
[| 〈Op1(f, e), sigma〉 -a-> i; !!n. [| 〈e, sigma〉 -a-> n; f ∈ nat -> nat; i = f ` n |] ==> Q |] ==> Q
and evala_Op2_E:
[| 〈Op2(f, a1.0, a2.0), sigma〉 -a-> i; !!n0 n1. [| 〈a1.0, sigma〉 -a-> n0; 〈a2.0, sigma〉 -a-> n1; f ∈ nat × nat -> nat; i = f ` 〈n0, n1〉 |] ==> Q |] ==> Q