Theory Com

(*  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›

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