Quelle  Com.thy   Sprache: Isabelle

(*  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\ \ -a-> n"
    X:   "\x \ loc; sigma \ loc->nat\ \ -a-> sigma`x"
    Op1: "\\e,sigma\ -a-> n; f \ nat -> nat\ \ -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\ \ -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                                  (‹🚫› [])
  | assignment ("x \ loc", "a \ aexp")       (infixl ‹🚫› 60)
  | semicolon ("c0 \ com", "c1 \ com")       (‹_🚫 _›  [60, 60] 10)
  | while ("b \ bexp", "c \ com")            (‹🚫 _ 🚫 _›  60)
  | "if" ("b \ bexp", "c0 \ com", "c1 \ com")    (‹🚫 _ 🚫 _ 🚫 _› 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\ \ <\,sigma> -c-> sigma"

    assign:  "\m \ nat; x \ loc; \a,sigma\ -a-> m\
              ==> <x 🚫 a,sigma> -c-> sigma(x:=m)"

    semi:    "\\c0,sigma\ -c-> sigma2; \c1,sigma2\ -c-> sigma1\
              ==> <c0🚫 c1, sigma> -c-> sigma1"

    if1:     "\b \ bexp; c1 \ com; sigma \ loc->nat;
                 ⟨b,sigma⟩ -b-> 1; ⟨c0,sigma⟩ -c-> sigma1]
              ==> <🚫 b 🚫 c0 🚫 c1, sigma> -c-> sigma1"

    if0:     "\b \ bexp; c0 \ com; sigma \ loc->nat;
                 ⟨b,sigma⟩ -b-> 0; ⟨c1,sigma⟩ -c-> sigma1]
               ==> <🚫 b 🚫 c0 🚫 c1, sigma> -c-> sigma1"

    while0:   "\c \ com; \b, sigma\ -b-> 0\
               ==> <🚫 b 🚫 c,sigma> -c-> sigma"

    while1:   "\c \ com; \b,sigma\ -b-> 1; \c,sigma\ -c-> sigma2;
                  <🚫 b 🚫 c, sigma2> -c-> sigma1]
               ==> <🚫 b 🚫 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!]: " -a-> i"
  and evala_X_E [elim!]: " -a-> i"
  and evala_Op1_E [elim!]: " -a-> i"
  and evala_Op2_E [elim!]: " -a-> i"

end