# HG changeset patch
# User nipkow
# Date 978427630 -3600
# Node ID 994877ee68cbd86bb2b93fdcfc0aa819278d2c97
# Parent  9d766f21cf415852d52a30e83edfe890666cec15
*** empty log message ***

diff -r 9d766f21cf41 -r 994877ee68cb src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Mon Jan 01 11:52:04 2001 +0100
+++ b/src/HOL/Induct/Com.ML	Tue Jan 02 10:27:10 2001 +0100
@@ -30,29 +30,15 @@
 Unify.search_bound := 60;
 
 (*Command execution is functional (deterministic) provided evaluation is*)
-Goal "Function ev ==> Function(exec ev)";
-by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
+Goal "univalent ev ==> univalent(exec ev)";
+by (simp_tac (simpset() addsimps [univalent_def]) 1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (etac exec.induct 1);
 by (Blast_tac 3);
 by (Blast_tac 1);
-by (rewrite_goals_tac [Function_def, Unique_def]);
+by (rewrite_goals_tac [univalent_def]);
 by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
-qed "Function_exec";
-
-
-Goalw [assign_def] "(s[v/x])x = v";
-by (Simp_tac 1);
-qed "assign_same";
+qed "univalent_exec";
 
-Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
-by (Asm_simp_tac 1);
-qed "assign_different";
-
-Goalw [assign_def] "s[s x/x] = s";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "assign_triv";
-
-Addsimps [assign_same, assign_different, assign_triv];
+Addsimps [fun_upd_same, fun_upd_other];
diff -r 9d766f21cf41 -r 994877ee68cb src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Mon Jan 01 11:52:04 2001 +0100
+++ b/src/HOL/Induct/Com.thy	Tue Jan 02 10:27:10 2001 +0100
@@ -6,7 +6,7 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
 *)
 
-Com = Datatype +
+Com = Main +
 
 types loc
       state = "loc => nat"
@@ -14,23 +14,22 @@
 
 arities loc :: term
 
-(*To avoid a mutually recursive datatype declaration, expressions and commands
-  are combined to form a single datatype.*)
 datatype
   exp = N nat
       | X loc
       | Op n2n2n exp exp
-      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
-      | SKIP
+      | valOf com exp          ("VALOF _ RESULTIS _"  60)
+and
+  com = SKIP
       | ":="  loc exp          (infixl  60)
-      | Semi  exp exp          ("_;;_"  [60, 60] 60)
-      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
-      | While exp exp          ("WHILE _ DO _"  60)
+      | Semi  com com          ("_;;_"  [60, 60] 60)
+      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
+      | While exp com          ("WHILE _ DO _"  60)
 
 (** Execution of commands **)
-consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
+consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
        "@exec"  :: "((exp*state) * (nat*state)) set => 
-                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
+                    [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
 
 translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
 
@@ -40,16 +39,12 @@
 translations
     "esig -|[eval]-> ns" => "(esig,ns) : eval"
 
-constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
-  "s[m/x] ==  (%y. if y=x then m else s y)"
-
-
 (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
 inductive "exec eval"
   intrs
     Skip    "(SKIP,s) -[eval]-> s"
 
-    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
+    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
 
     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
             ==> (c0 ;; c1, s) -[eval]-> s1"
@@ -65,11 +60,4 @@
     WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
                 ==> (WHILE e DO c, s) -[eval]-> s3"
-
-constdefs
-    Unique   :: "['a, 'b, ('a*'b) set] => bool"
-    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
-
-    Function :: "('a*'b) set => bool"
-    "Function r == ALL x y. (x,y): r --> Unique x y r"
 end
diff -r 9d766f21cf41 -r 994877ee68cb src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Mon Jan 01 11:52:04 2001 +0100
+++ b/src/HOL/Induct/Exp.ML	Tue Jan 02 10:27:10 2001 +0100
@@ -19,8 +19,8 @@
 AddSEs eval_elim_cases;
 
 
-Goal "(X x, s[n/x]) -|-> (n, s[n/x])";
-by (rtac (assign_same RS subst) 1 THEN resolve_tac eval.intrs 1);
+Goal "(X x, s(x:=n)) -|-> (n, s(x:=n))";
+by (rtac (fun_upd_same RS subst) 1 THEN resolve_tac eval.intrs 1);
 qed "var_assign_eval";
 
 AddSIs [var_assign_eval];
@@ -66,33 +66,32 @@
   the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   functional on the argument (c,s).
 *)
-Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
+Goal "(c,s) -[eval Int {((e,s),(n,t)). ALL nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 \
 \     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
 by (etac exec.induct 1);
 by (ALLGOALS Full_simp_tac);
-by (Blast_tac 3);
-by (Blast_tac 1);
-by (rewtac Unique_def);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addEs [exec_WHILE_case]) 1);
+      by (Blast_tac 1);
+     by (Force_tac 1);
+    by (Blast_tac 1);
+   by (Blast_tac 1);
+  by (Blast_tac 1);
+ by (blast_tac (claset() addEs [exec_WHILE_case]) 1);
 by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
 by (Clarify_tac 1);
 by (etac exec_WHILE_case 1);
-by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
+ by (ALLGOALS Blast_tac);
 qed "com_Unique";
 
 
 (*Expression evaluation is functional, or deterministic*)
-Goalw [Function_def] "Function eval";
-by (strip_tac 1);
+Goalw [univalent_def] "univalent eval";
+by (EVERY1[rtac allI, rtac allI, rtac impI]);
 by (split_all_tac 1);
 by (etac eval_induct 1);
 by (dtac com_Unique 4);
-by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
+by (ALLGOALS Full_simp_tac);
 by (ALLGOALS Blast_tac);
-qed "Function_eval";
+qed "univalent_eval";
 
 
 Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
@@ -215,11 +214,12 @@
 
 (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
 
+Delsimps [fun_upd_apply];
 Goal "(e',s) -|-> (v,s'') ==> \
 \              (e' = VALOF x:=e RESULTIS X x) --> \
-\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
+\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))";
 by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
+   by (ALLGOALS Asm_simp_tac);
 by (thin_tac "?PP-->?QQ" 1);
 by (Clarify_tac 1);
 by (Simp_tac 1);
@@ -228,6 +228,6 @@
 
 
 Goal "(e,s) -|-> (v,s') ==> \
-\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
+\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))";
 by (Blast_tac 1);
 qed "valof_assign2";
diff -r 9d766f21cf41 -r 994877ee68cb src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Mon Jan 01 11:52:04 2001 +0100
+++ b/src/HOL/Induct/PropLog.ML	Tue Jan 02 10:27:10 2001 +0100
@@ -56,21 +56,6 @@
 (* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
 bind_thm ("thms_notE", (thms.MP RS thms_falseE));
 
-(** The function eval **)
-
-Goalw [eval_def] "tt[[false]] = False";
-by (Simp_tac 1);
-qed "eval_false";
-
-Goalw [eval_def] "tt[[#v]] = (v:tt)";
-by (Simp_tac 1);
-qed "eval_var";
-
-Goalw [eval_def] "tt[[p->q]] = (tt[[p]]-->tt[[q]])";
-by (Simp_tac 1);
-qed "eval_imp";
-
-Addsimps [eval_false, eval_var, eval_imp];
 
 (*Soundness of the rules wrt truth-table semantics*)
 Goalw [sat_def] "H |- p ==> H |= p";
diff -r 9d766f21cf41 -r 994877ee68cb src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Mon Jan 01 11:52:04 2001 +0100
+++ b/src/HOL/Induct/PropLog.thy	Tue Jan 02 10:27:10 2001 +0100
@@ -14,7 +14,6 @@
   thms :: 'a pl set => 'a pl set
   "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
   "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
-  eval2 :: ['a pl, 'a set] => bool
   eval  :: ['a set, 'a pl] => bool      ("_[[_]]" [100,0] 100)
   hyps  :: ['a pl, 'a set] => 'a pl set
 
@@ -31,17 +30,16 @@
 
 defs
   sat_def  "H |= p  ==  (!tt. (!q:H. tt[[q]]) --> tt[[p]])"
-  eval_def "tt[[p]] == eval2 p tt"
 
 primrec
-  "eval2(false) = (%x. False)"
-  "eval2(#v) = (%tt. v:tt)"
-  "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
+         "tt[[false]] = False"
+         "tt[[#v]]    = (v:tt)"
+eval_imp "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
 
 primrec
-  "hyps(false) = (%tt.{})"
-  "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
-  "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
+  "hyps false  tt = {}"
+  "hyps (#v)   tt = {if v:tt then #v else #v->false}"
+  "hyps (p->q) tt = hyps p tt Un hyps q tt"
 
 end