# HG changeset patch
# User clasohm
# Date 794228656 -3600
# Node ID 806721cfbf460d699bf3aa087a0ddb569e5aa693
# Parent  ff1574a81019c69a0fba59b9be6adf7d7ca367ff
new version of HOL/IMP with curried function application

diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Com.ML
--- /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)))"];
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Com.thy
--- /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
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Denotation.ML
--- /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)]);
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Denotation.thy
--- /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
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Equiv.ML
--- /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";
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Equiv.thy
--- /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
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Properties.ML
--- /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();
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/Properties.thy
--- /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"
diff -r ff1574a81019 -r 806721cfbf46 src/HOL/IMP/ROOT.ML
--- /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";