Equivalence of op. and den. sem. for simple while language.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Denotation.thy Wed Aug 31 15:15:54 1994 +0200
@@ -0,0 +1,47 @@
+(* Title: ZF/IMP/Denotation.thy
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+
+Denotational semantics of expressions & commands
+*)
+
+Denotation = Com +
+
+consts
+ A :: "aexp => env => nat"
+ B :: "bexp => env => bool"
+ C :: "com => (env*env)set"
+ Gamma :: "[bexp,com,(env*env)set] => (env*env)set"
+
+rules
+ A_nat_def "A(N(n)) == (%sigma. n)"
+ A_loc_def "A(X(x)) == (%sigma. sigma(x))"
+ A_op1_def "A(Op1(f,a)) == (%sigma. f(A(a,sigma)))"
+ A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))"
+
+
+ B_true_def "B(true) == (%sigma. True)"
+ B_false_def "B(false) == (%sigma. False)"
+ B_op_def "B(ROp(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))"
+
+
+ B_not_def "B(noti(b)) == (%sigma. ~B(b,sigma))"
+ B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) & B(b1,sigma))"
+ B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) | B(b1,sigma))"
+
+ C_skip_def "C(skip) == id"
+ C_assign_def "C(x := a) == {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
+
+ C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
+ C_if_def "C(ifc b then c0 else c1) == \
+\ {io. io:C(c0) & B(b,fst(io))} Un \
+\ {io. io:C(c1) & ~B(b,fst(io))}"
+
+ Gamma_def "Gamma(b,c) == \
+\ (%phi.{io. io : (phi O C(c)) & B(b,fst(io))} Un \
+\ {io. io : id & ~B(b,fst(io))})"
+
+ C_while_def "C(while b do c) == lfp(Gamma(b,c))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Equiv.ML Wed Aug 31 15:15:54 1994 +0200
@@ -0,0 +1,104 @@
+(* Title: ZF/IMP/Equiv.ML
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+*)
+
+goal Equiv.thy "(<a,sigma> -a-> n) = (A(a,sigma) = n)";
+by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
+by (aexp.induct_tac "a" 1); (* struct. ind. *)
+by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *)
+by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
+ addSEs aexp_elim_cases)));
+val aexp_iff = result();
+
+val aexp1 = aexp_iff RS iffD1;
+val aexp2 = aexp_iff RS iffD2;
+
+
+goal Equiv.thy "(<b,sigma> -b-> w) = (B(b,sigma) = w)";
+by (res_inst_tac [("x","w")] spec 1); (* quantify w *)
+by (bexp.induct_tac "b" 1); (* struct. ind. *)
+by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *)
+by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs)
+ addSDs [aexp1] addSEs bexp_elim_cases)
+ THEN ALLGOALS(best_tac HOL_cs));
+
+val bexp_iff = result();
+
+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,sigma> -c-> sigma' ==> <sigma,sigma'> : 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_rewrite_rules));
+(* skip *)
+by (fast_tac comp_cs 1);
+(* assign *)
+by (asm_full_simp_tac (prod_ss addsimps [aexp1]) 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);
+
+val com1 = result();
+
+
+val com_cs = comp_cs addSIs [aexp2,bexp2] addIs evalc.intrs;
+
+goal Equiv.thy "!x:C(c). <c,fst(x)> -c-> snd(x)";
+by (com.induct_tac "c" 1);
+by (rewrite_tac C_rewrite_rules);
+by (safe_tac com_cs);
+by (ALLGOALS (asm_full_simp_tac prod_ss));
+
+(* skip *)
+by (fast_tac com_cs 1);
+
+(* assign *)
+by (fast_tac com_cs 1);
+
+(* comp *)
+by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
+by (asm_full_simp_tac prod_ss 1);
+by (fast_tac com_cs 1);
+
+(* while *)
+by (etac (Gamma_mono RSN (2,induct)) 1);
+by (rewrite_goals_tac [Gamma_def]);
+by (safe_tac com_cs);
+by (EVERY1 [dtac bspec, atac]);
+by (ALLGOALS (asm_full_simp_tac prod_ss));
+
+(* while, if *)
+by (ALLGOALS (fast_tac com_cs));
+val com2 = result();
+
+
+(**** 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);
+val com_equivalence = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Equiv.thy Wed Aug 31 15:15:54 1994 +0200
@@ -0,0 +1,7 @@
+(* Title: ZF/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/IMP/ROOT.ML Wed Aug 31 15:15:54 1994 +0200
@@ -0,0 +1,20 @@
+(* Title: ZF/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.
+
+*)
+
+ZF_build_completed; (*Make examples fail if ZF did*)
+
+writeln"Root file for ZF/IMP";
+proof_timing := true;
+loadpath := [".","IMP"];
+time_use_thy "Equiv";