--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Com.ML Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,30 @@
+(* Title: HOL/IMP/Com.ML
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+*)
+
+open Com;
+
+val evala_elim_cases = map (evala.mk_cases aexp.simps)
+ ["<N(n),sigma> -a-> i", "<X(x),sigma> -a-> i",
+ "<Op1 f e,sigma> -a-> i", "<Op2 f a1 a2,sigma> -a-> i"
+ ];
+
+val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
+ ["<true,sigma> -b-> x", "<false,sigma> -b-> x",
+ "<ROp f a0 a1,sigma> -b-> x", "<noti(b),sigma> -b-> x",
+ "<b0 andi b1,sigma> -b-> x", "<b0 ori b1,sigma> -b-> x"
+ ];
+
+val evalb_simps = map (fn s => prove_goal Com.thy s
+ (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
+ ["(<true,sigma> -b-> w) = (w=True)",
+ "(<false,sigma> -b-> w) = (w=False)",
+ "(<ROp f a0 a1,sigma> -b-> w) = \
+\ (? m. <a0,sigma> -a-> m & (? n. <a1,sigma> -a-> n & w = f m n))",
+ "(<noti(b),sigma> -b-> w) = (? x. <b,sigma> -b-> x & w = (~x))",
+ "(<b0 andi b1,sigma> -b-> w) = \
+\ (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x&y)))",
+ "(<b0 ori b1,sigma> -b-> w) = \
+\ (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x|y)))"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Com.thy Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,112 @@
+(* Title: HOL/IMP/Com.thy
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+
+Arithmetic expressions, Boolean expressions, Commands
+
+And their Operational semantics
+*)
+
+Com = Arith +
+
+(** Arithmetic expressions **)
+types loc
+ state = "loc => nat"
+ n2n = "nat => nat"
+ n2n2n = "nat => nat => nat"
+
+arities loc :: term
+
+datatype
+ aexp = N (nat)
+ | X (loc)
+ | Op1 (n2n, aexp)
+ | Op2 (n2n2n, aexp, aexp)
+
+(** Evaluation of arithmetic expressions **)
+consts evala :: "(aexp*state*nat)set"
+ "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50)
+translations
+ "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
+inductive "evala"
+ intrs
+ N "<N(n),s> -a-> n"
+ X "<X(x),s> -a-> s(x)"
+ Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
+ Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |] \
+\ ==> <Op2 f e0 e1,s> -a-> f n0 n1"
+
+types n2n2b = "[nat,nat] => bool"
+
+(** Boolean expressions **)
+
+datatype
+ bexp = true
+ | false
+ | ROp (n2n2b, aexp, aexp)
+ | noti (bexp)
+ | andi (bexp,bexp) (infixl 60)
+ | ori (bexp,bexp) (infixl 60)
+
+(** Evaluation of boolean expressions **)
+consts evalb :: "(bexp*state*bool)set"
+ "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50)
+
+translations
+ "<be,sig> -b-> b" == "<be,sig,b> : evalb"
+
+inductive "evalb"
+ intrs (*avoid clash with ML constructors true, false*)
+ tru "<true,s> -b-> True"
+ fls "<false,s> -b-> False"
+ ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
+\ ==> <ROp f a0 a1,s> -b-> f n0 n1"
+ noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
+ andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
+\ ==> <b0 andi b1,s> -b-> (w0 & w1)"
+ ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
+\ ==> <b0 ori b1,s> -b-> (w0 | w1)"
+
+(** Commands **)
+
+datatype
+ com = skip
+ | ":=" (loc,aexp) (infixl 60)
+ | semic (com,com) ("_; _" [60, 60] 10)
+ | whileC (bexp,com) ("while _ do _" 60)
+ | ifC (bexp, com, com) ("ifc _ then _ else _" 60)
+
+(** Execution of commands **)
+consts evalc :: "(com*state*state)set"
+ "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
+ "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95)
+
+translations
+ "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
+
+rules
+ assign_def "s[m/x] == (%y. if (y=x) m (s y))"
+
+inductive "evalc"
+ intrs
+ skip "<skip,s> -c-> s"
+
+ assign "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
+
+ semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
+\ ==> <c0 ; c1, s> -c-> s1"
+
+ ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
+\ ==> <ifc b then c0 else c1, s> -c-> s1"
+
+ ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
+\ ==> <ifc b then c0 else c1, s> -c-> s1"
+
+ whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
+
+ whileTrue "[| <b,s> -b-> True; <c,s> -c-> s2; \
+\ <while b do c, s2> -c-> s1 |] \
+\ ==> <while b do c, s> -c-> s1 "
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Denotation.ML Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,24 @@
+(* Title: HOL/IMP/Denotation.ML
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+*)
+
+open Denotation;
+
+(**** Rewrite Rules for A,B,C ****)
+
+val A_simps =
+ [A_nat,A_loc,A_op1,A_op2];
+
+val B_simps = map (fn t => t RS eq_reflection)
+ [B_true,B_false,B_op,B_not,B_and,B_or]
+
+val C_simps = map (fn t => t RS eq_reflection)
+ [C_skip,C_assign,C_comp,C_if,C_while];
+
+(**** mono (Gamma(b,c)) ****)
+
+qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
+ "mono (Gamma b c)"
+ (fn _ => [(best_tac comp_cs 1)]);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Denotation.thy Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,46 @@
+(* Title: HOL/IMP/Denotation.thy
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+
+Denotational semantics of expressions & commands
+*)
+
+Denotation = Com +
+
+types com_den = "(state*state)set"
+consts
+ A :: "aexp => state => nat"
+ B :: "bexp => state => bool"
+ C :: "com => com_den"
+ Gamma :: "[bexp,com_den] => (com_den => com_den)"
+
+primrec A aexp
+ A_nat "A(N(n)) = (%s. n)"
+ A_loc "A(X(x)) = (%s. s(x))"
+ A_op1 "A(Op1 f a) = (%s. f(A a s))"
+ A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+
+primrec B bexp
+ B_true "B(true) = (%s. True)"
+ B_false "B(false) = (%s. False)"
+ B_op "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+ B_not "B(noti(b)) = (%s. ~(B b s))"
+ B_and "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
+ B_or "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+
+defs
+ Gamma_def "Gamma b cd == \
+\ (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
+\ {st. st : id & ~B b (fst st)})"
+
+primrec C com
+ C_skip "C(skip) = id"
+ C_assign "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
+ C_comp "C(c0 ; c1) = C(c1) O C(c0)"
+ C_if "C(ifc b then c0 else c1) = \
+\ {st. st:C(c0) & (B b (fst st))} Un \
+\ {st. st:C(c1) & ~(B b (fst st))}"
+ C_while "C(while b do c) = lfp (Gamma b (C c))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Equiv.ML Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,85 @@
+(* Title: HOL/IMP/Equiv.ML
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+*)
+
+goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A a s)";
+by (aexp.induct_tac "a" 1); (* struct. ind. *)
+by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps))); (* rewr. Den. *)
+by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
+ addSEs evala_elim_cases)));
+bind_thm("aexp_iff", result() RS spec);
+
+goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B b s)";
+by (bexp.induct_tac "b" 1);
+by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
+ addsimps (aexp_iff::B_simps@evalb_simps))));
+bind_thm("bexp_iff", result() RS spec);
+
+val bexp1 = bexp_iff RS iffD1;
+val bexp2 = bexp_iff RS iffD2;
+
+val BfstI = read_instantiate_sg (sign_of Equiv.thy)
+ [("P","%x.B ?b x")] (fst_conv RS ssubst);
+val BfstD = read_instantiate_sg (sign_of Equiv.thy)
+ [("P","%x.B ?b x")] (fst_conv RS subst);
+
+goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)";
+
+(* start with rule induction *)
+be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
+by (rewrite_tac (Gamma_def::C_simps));
+ (* simplification with HOL_ss again too agressive *)
+(* skip *)
+by (fast_tac comp_cs 1);
+(* assign *)
+by (asm_full_simp_tac (prod_ss addsimps [aexp_iff]) 1);
+(* comp *)
+by (fast_tac comp_cs 1);
+(* if *)
+by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1);
+by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1);
+(* while *)
+by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
+by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
+
+qed "com1";
+
+
+val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs);
+
+goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
+by (com.induct_tac "c" 1);
+by (rewrite_tac C_simps);
+by (safe_tac comp_cs);
+by (ALLGOALS (asm_full_simp_tac com_ss));
+
+(* comp *)
+by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
+by (asm_full_simp_tac com_ss 1);
+
+(* while *)
+by (etac (Gamma_mono RSN (2,induct)) 1);
+by (rewrite_goals_tac [Gamma_def]);
+by (safe_tac comp_cs);
+by (EVERY1 [dtac bspec, atac]);
+by (ALLGOALS (asm_full_simp_tac com_ss));
+
+qed "com2";
+
+
+(**** Proof of Equivalence ****)
+
+val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1];
+
+goal Equiv.thy "C(c) = {io . <c,fst(io)> -c-> snd(io)}";
+by (rtac equalityI 1);
+(* => *)
+by (fast_tac com_iff_cs 1);
+(* <= *)
+by (REPEAT (step_tac com_iff_cs 1));
+by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1);
+qed "com_equivalence";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Equiv.thy Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,7 @@
+(* Title: HOL/IMP/Equiv.thy
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+*)
+
+Equiv = Denotation
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Properties.ML Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/IMP/Properties.ML
+ ID: $Id$
+ Author: Tobias Nipkow, TUM
+ Copyright 1994 TUM
+
+IMP is deterministic.
+*)
+
+(* evaluation of aexp is deterministic *)
+goal Com.thy "!m n. <a,s> -a-> m & <a,s> -a-> n --> m=n";
+by(res_inst_tac[("aexp","a")]Com.aexp.induct 1);
+by(REPEAT(fast_tac (HOL_cs addSIs evala.intrs addSEs evala_elim_cases) 1));
+bind_thm("aexp_detD", conjI RS (result() RS spec RS spec RS mp));
+
+(* evaluation of bexp is deterministic *)
+goal Com.thy "!v w. <b,s> -b-> v & <b,s> -b-> w --> v=w";
+by(res_inst_tac[("bexp","b")]Com.bexp.induct 1);
+by(REPEAT(fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases
+ addDs [aexp_detD]) 1));
+bind_thm("bexp_detD", conjI RS (result() RS spec RS spec RS mp));
+
+
+val evalc_elim_cases = map (evalc.mk_cases com.simps)
+ ["<skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
+ "<ifc b then c1 else c2, s> -c-> t", "<while b do c,s> -c-> t"];
+
+(* evaluation of com is deterministic *)
+goal Com.thy "!!c. <c,s> -c-> t ==> !u. <c,s> -c-> u --> u=t";
+(* start with rule induction *)
+be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
+by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases addDs [aexp_detD]) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
+by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
+by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
+ atac, dtac bexp_detD, atac, etac False_neq_True]);
+by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
+ dtac bexp_detD, atac, etac (sym RS False_neq_True),
+ fast_tac HOL_cs]);
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Properties.thy Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,1 @@
+Properties = "Com"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/ROOT.ML Fri Mar 03 12:04:16 1995 +0100
@@ -0,0 +1,21 @@
+(* Title: CHOL/IMP/ROOT.ML
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+
+Executes the formalization of the denotational and operational semantics of a
+simple while-language, including an equivalence proof. The whole development
+essentially formalizes/transcribes chapters 2 and 5 of
+
+Glynn Winskel. The Formal Semantics of Programming Languages.
+MIT Press, 1993.
+
+*)
+
+CHOL_build_completed; (*Make examples fail if CHOL did*)
+
+writeln"Root file for CHOL/IMP";
+proof_timing := true;
+loadpath := [".","IMP"];
+time_use_thy "Properties";
+time_use_thy "Equiv";