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