# Theory Com

theory Com
imports ZF
```(*  Title:      ZF/IMP/Com.thy
Author:     Heiko Loetzbeyer and Robert Sandner, TU München
*)

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›

and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2]

and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2]