# HG changeset patch
# User nipkow
# Date 830785707 -7200
# Node ID afd3b60660dbf9059ecbf18c47afb99236d78277
# Parent  0bcc8cab3461d5bdc8a5c263538c96f26b0a11d8
Natural and Transition semantics.

diff -r 0bcc8cab3461 -r afd3b60660db src/HOL/IMP/Natural.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Natural.ML	Mon Apr 29 15:48:27 1996 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/IMP/Natural.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow & Larry Paulson, TUM
+    Copyright   1996 TUM
+*)
+
+open Natural;
+
+val evalc_elim_cases = map (evalc.mk_cases com.simps)
+   ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
+    "<IF b THEN c1 ELSE c2, s> -c-> t"];
+
+val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
+
+val evalc_cs = set_cs addSEs evalc_elim_cases
+                      addEs  [evalc_WHILE_case];
+
+(* evaluation of com is deterministic *)
+goal Natural.thy "!c s t. <c,s> -c-> t --> (!u. <c,s> -c-> u --> u=t)";
+by (rtac evalc.mutual_induct 1);
+by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7);
+by (ALLGOALS (deepen_tac evalc_cs 4));
+qed_spec_mp "com_det";
diff -r 0bcc8cab3461 -r afd3b60660db src/HOL/IMP/Natural.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Natural.thy	Mon Apr 29 15:48:27 1996 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/IMP/Natural.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Robert Sandner, TUM
+    Copyright   1996 TUM
+
+Natural semantics of commands
+*)
+
+Natural = Com +
+
+(** Execution of commands **)
+consts  evalc    :: "(com*state*state)set"
+        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
+
+translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
+
+constdefs assign :: [state,val,loc] => state    ("_[_'/_]" [95,0,0] 95)
+  "s[m/x] ==  (%y. if y=x then m else s y)"
+
+
+inductive "evalc"
+  intrs
+    Skip    "<SKIP,s> -c-> s"
+
+    Assign  "<x := a,s> -c-> s[a(s)/x]"
+
+    Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
+            ==> <c0 ; c1, s> -c-> s1"
+
+    IfTrue "[| b s; <c0,s> -c-> s1 |] 
+            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
+
+    IfFalse "[| ~b s; <c1,s> -c-> s1 |] 
+             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
+
+    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
+
+    WhileTrue  "[| b s;  <c,s> -c-> s2;  <WHILE b DO c, s2> -c-> s1 |] 
+               ==> <WHILE b DO c, s> -c-> s1"
+
+end
diff -r 0bcc8cab3461 -r afd3b60660db src/HOL/IMP/Transition.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Transition.ML	Mon Apr 29 15:48:27 1996 +0200
@@ -0,0 +1,123 @@
+(*  Title:      HOL/IMP/Transition.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow & Robert Sandner, TUM
+    Copyright   1996 TUM
+
+Equivalence of Natural and Transition semantics
+*)
+
+open Transition;
+
+val relpow_cs = rel_cs addSEs [rel_pow_0_E];
+
+val evalc1_elim_cases = map (evalc1.mk_cases com.simps)
+   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t", "(c1;c2, s) -1-> t",
+    "(IF b THEN c1 ELSE c2, s) -1-> t", "(WHILE b DO c,s) -1-> t"];
+
+val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs);
+
+goal Transition.thy "!!c. (c,s) -(0)-> (SKIP,u) ==> c = SKIP & s = u";
+by(fast_tac evalc1_cs 1);
+val hlemma1 = result();
+
+goal Transition.thy "!!s. (SKIP,s) -(m)-> (SKIP,t) ==> s = t & m = 0";
+be rel_pow_E2 1;
+by (Asm_full_simp_tac 1);
+by (eresolve_tac evalc1_elim_cases 1);
+val hlemma2 = result();
+
+
+goal Transition.thy
+  "!s t u c d. (c,s) -(n)-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
+\              (c;d, s) -*-> (SKIP, u)";
+by(nat_ind_tac "n" 1);
+ (* case n = 0 *)
+ by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2])1);
+(* induction step *)
+by (safe_tac (HOL_cs addSDs [rel_pow_Suc_D2]));
+by(split_all_tac 1);
+by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+qed_spec_mp "lemma1";
+
+
+goal Transition.thy "!c s s1. <c,s> -c-> s1 --> (c,s) -*-> (SKIP,s1)";
+br evalc.mutual_induct 1;
+
+(* SKIP *)
+br rtrancl_refl 1;
+
+(* ASSIGN *)
+by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
+
+(* SEMI *)
+by (fast_tac (set_cs addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
+
+(* IF *)
+by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+
+(* WHILE *)
+by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
+by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow]
+                        addIs [rtrancl_into_rtrancl2,lemma1]) 1);
+
+qed_spec_mp "evalc_impl_evalc1";
+
+
+goal Transition.thy
+  "!c d s u. (c;d,s) -(n)-> (SKIP,u) --> \
+\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -(m)-> (SKIP,u) & m <= n)";
+by(nat_ind_tac "n" 1);
+ (* case n = 0 *)
+ by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1);
+(* induction step *)
+by (fast_tac (HOL_cs addSIs [rtrancl_refl,le_SucI,le_refl]
+                     addSDs [rel_pow_Suc_D2]
+                     addSEs (evalc1_elim_cases@
+                             [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2])) 1);
+qed_spec_mp "lemma2";
+
+goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
+by (com.induct_tac "c" 1);
+by (safe_tac (evalc1_cs addSDs [rtrancl_imp_UN_rel_pow]));
+
+(* SKIP *)
+by (fast_tac (evalc1_cs addSEs rel_pow_E2::evalc1_elim_cases) 1);
+
+(* ASSIGN *)
+by (fast_tac (evalc1_cs addSDs [hlemma2]
+                        addSEs rel_pow_E2::evalc1_elim_cases
+                        addss !simpset) 1);
+
+(* SEMI *)
+by (fast_tac (evalc1_cs addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
+
+(* IF *)
+be rel_pow_E2 1;
+by (Asm_full_simp_tac 1);
+by (fast_tac (evalc1_cs addSDs[rel_pow_imp_rtrancl]addEs evalc1_elim_cases) 1);
+
+(* WHILE, induction on the length of the computation *)
+by(rotate_tac 1 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("x","s")] spec 1);
+by(res_inst_tac [("n","n")] less_induct 1);
+by (strip_tac 1);
+be rel_pow_E2 1;
+ by (Asm_full_simp_tac 1);
+by (eresolve_tac evalc1_elim_cases 1);
+
+(* WhileFalse *)
+ by (fast_tac (evalc1_cs addSDs [hlemma2]) 1);
+
+(* WhileTrue *)
+by(fast_tac(evalc1_cs addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
+
+qed_spec_mp "evalc1_impl_evalc";
+
+
+(**** proof of the equivalence of evalc and evalc1 ****)
+
+goal Transition.thy "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)";
+by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1);
+qed "evalc1_eq_evalc";
diff -r 0bcc8cab3461 -r afd3b60660db src/HOL/IMP/Transition.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Transition.thy	Mon Apr 29 15:48:27 1996 +0200
@@ -0,0 +1,40 @@
+(*  Title:      HOL/IMP/Transition.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Robert Sandner, TUM
+    Copyright   1996 TUM
+
+Transition semantics of commands
+*)
+
+Transition = Natural + RelPow +
+
+consts  evalc1    :: "((com*state)*(com*state))set"        
+	"@evalc1" :: "[(com*state),(com*state)] => bool"   
+				("_ -1-> _" [81,81] 100)
+	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
+				("_ -(_)-> _" [81,81] 100)
+	"@evalc*" :: "[(com*state),(com*state)] => bool"   
+				("_ -*-> _" [81,81] 100)
+
+translations
+       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
+        "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
+	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
+	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
+	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
+
+
+inductive "evalc1"
+  intrs
+    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
+
+    Semi1   "(SKIP;c,s) -1-> (c,s)"	
+    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
+
+    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
+    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
+
+    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
+    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
+
+end