(* Title: ZF/IMP/Com.thy
Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
section \<open>Arithmetic expressions, boolean expressions, commands\<close>
theory Com imports ZF begin
subsection \<open>Arithmetic expressions\<close>
consts
loc :: i
aexp :: i
datatype \<subseteq> "univ(loc \<union> (nat -> nat) \<union> ((nat \<times> 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 \<open>-a->\<close> 50)
where "p -a-> n == \ evala"
inductive
domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat"
intros
N: "[| n \ nat; sigma \ loc->nat |] ==> -a-> n"
X: "[| x \ loc; sigma \ loc->nat |] ==> -a-> sigma`x"
Op1: "[| -a-> n; f \ nat -> nat |] ==> -a-> f`n"
Op2: "[| -a-> n0; -a-> n1; f \ (nat\nat) -> nat |]
==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
type_intros aexp.intros apply_funtype
subsection \<open>Boolean expressions\<close>
consts bexp :: i
datatype \<subseteq> "univ(aexp \<union> ((nat \<times> 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 \<open>-b->\<close> 50)
where "p -b-> b == \ evalb"
inductive
domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool"
intros
true: "[| sigma \ loc -> nat |] ==> -b-> 1"
false: "[| sigma \ loc -> nat |] ==> -b-> 0"
ROp: "[| -a-> n0; -a-> n1; f \ (nat*nat)->bool |]
==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
noti: "[| -b-> w |] ==> -b-> not(w)"
andi: "[| -b-> w0; -b-> w1 |]
==> <b0 andi b1,sigma> -b-> (w0 and w1)"
ori: "[| -b-> w0; -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 \<open>Commands\<close>
consts com :: i
datatype com =
skip (\<open>\<SKIP>\<close> [])
| 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 \<open>-c->\<close> 50)
where "p -c-> s == \ evalc"
inductive
domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)"
intros
skip: "[| sigma \ loc -> nat |] ==> <\,sigma> -c-> sigma"
assign: "[| m \ nat; x \ loc; -a-> m |]
==> <x \<ASSN> a,sigma> -c-> sigma(x:=m)"
semi: "[| -c-> 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-> 0 |]
==> <\<WHILE> b \<DO> c,sigma> -c-> sigma"
while1: "[| c \ com; -b-> 1; -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 \<open>Misc lemmas\<close>
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
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
