# Theory Com

Up to index of Isabelle/ZF/IMP

theory Com
imports Main
begin

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

### Arithmetic expressions

### Boolean expressions

### Commands

### Misc lemmas

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