# HG changeset patch
# User paulson
# Date 1017750508 -7200
# Node ID d3e1d554cd6dbd0d1787149c23d726db4c3d0201
# Parent  96bf406fd3e5485368f7e0552669c7cd9cf037c2
conversion of some HOL/Induct proof scripts to Isar

diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*  Title:      HOL/Induct/Com
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Example of Mutual Induction via Iteratived Inductive Definitions: Commands
-*)
-
-AddIs exec.intrs;
-
-val exec_elim_cases = 
-    map exec.mk_cases
-       ["(SKIP,s) -[eval]-> t",
-	"(x:=a,s) -[eval]-> t", 
-	"(c1;;c2, s) -[eval]-> t",
-	"(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
-
-val exec_WHILE_case = exec.mk_cases "(WHILE b DO c,s) -[eval]-> t";
-
-AddSEs exec_elim_cases;
-
-(*This theorem justifies using "exec" in the inductive definition of "eval"*)
-Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "exec_mono";
-
-
-Unify.trace_bound := 30;
-Unify.search_bound := 60;
-
-(*Command execution is functional (deterministic) provided evaluation is*)
-Goal "single_valued ev ==> single_valued(exec ev)";
-by (simp_tac (simpset() addsimps [single_valued_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 (rewtac single_valued_def);
-by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
-qed "single_valued_exec";
-
-Addsimps [fun_upd_same, fun_upd_other];
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/Com.thy	Tue Apr 02 14:28:28 2002 +0200
@@ -6,11 +6,12 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
 *)
 
-Com = Main +
+theory Com = Main:
 
-types loc
-      state = "loc => nat"
-      n2n2n = "nat => nat => nat"
+typedecl loc
+
+types  state = "loc => nat"
+       n2n2n = "nat => nat => nat"
 
 arities loc :: type
 
@@ -26,38 +27,285 @@
       | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
       | While exp com          ("WHILE _ DO _"  60)
 
-(** Execution of commands **)
+text{* Execution of commands *}
 consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
        "@exec"  :: "((exp*state) * (nat*state)) set => 
                     [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
 
-translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
+translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
 
 syntax  eval'   :: "[exp*state,nat*state] => 
 		    ((exp*state) * (nat*state)) set => bool"
-						   ("_/ -|[_]-> _" [50,0,50] 50)
-translations
-    "esig -|[eval]-> ns" => "(esig,ns) : eval"
+					   ("_/ -|[_]-> _" [50,0,50] 50)
 
-(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
-inductive "exec eval"
-  intrs
-    Skip    "(SKIP,s) -[eval]-> s"
+translations
+    "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
 
-    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"
+text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
+inductive "exec eval"
+  intros
+    Skip:    "(SKIP,s) -[eval]-> s"
 
-    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
-            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+    Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
 
-    IfFalse "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
+    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
+             ==> (c0 ;; c1, s) -[eval]-> s1"
+
+    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1"
+    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
+              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+
+    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) 
+                 ==> (WHILE e DO c, s) -[eval]-> s1"
+
+    WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
+                    (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
+                 ==> (WHILE e DO c, s) -[eval]-> s3"
+
+declare exec.intros [intro]
+
+
+inductive_cases
+	[elim!]: "(SKIP,s) -[eval]-> t"
+    and [elim!]: "(x:=a,s) -[eval]-> t"
+    and	[elim!]: "(c1;;c2, s) -[eval]-> t"
+    and	[elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
+    and	exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
+
+
+text{*Justifies using "exec" in the inductive definition of "eval"*}
+lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
+apply (unfold exec.defs )
+apply (rule lfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+ML {*
+Unify.trace_bound := 30;
+Unify.search_bound := 60;
+*}
+
+text{*Command execution is functional (deterministic) provided evaluation is*}
+theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
+apply (simp add: single_valued_def)
+apply (intro allI) 
+apply (rule impI)
+apply (erule exec.induct)
+apply (blast elim: exec_WHILE_case)+
+done
+
+
+section {* Expressions *}
+
+text{* Evaluation of arithmetic expressions *}
+consts  eval    :: "((exp*state) * (nat*state)) set"
+       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
+
+translations
+    "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
+    "esig -|-> ns"    == "(esig,ns ) \<in> eval"
+  
+inductive eval
+  intros 
+    N [intro!]: "(N(n),s) -|-> (n,s)"
+
+    X [intro!]: "(X(x),s) -|-> (s(x),s)"
+
+    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
+                 ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
+
+    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
+                    ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
+
+  monos exec_mono
+
+
+inductive_cases
+	[elim!]: "(N(n),sigma) -|-> (n',s')"
+    and [elim!]: "(X(x),sigma) -|-> (n,s')"
+    and	[elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
+    and	[elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
+
+
+lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
+by (rule fun_upd_same [THEN subst], fast)
+
+
+text{* Make the induction rule look nicer -- though eta_contract makes the new
+    version look worse than it is...*}
+
+lemma split_lemma:
+     "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
+by auto
+
+text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
+lemma eval_induct:
+  "[| (e,s) -|-> (n,s');                                          
+      !!n s. P (N n) s n s;                                       
+      !!s x. P (X x) s (s x) s;                                   
+      !!e0 e1 f n0 n1 s s0 s1.                                    
+         [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                    
+            (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                   
+         |] ==> P (Op f e0 e1) s (f n0 n1) s1;                    
+      !!c e n s s0 s1.                                            
+         [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;  
+            (c,s) -[eval]-> s0;                                   
+            (e,s0) -|-> (n,s1); P e s0 n s1 |]                    
+         ==> P (VALOF c RESULTIS e) s n s1                        
+   |] ==> P e s n s'"
+apply (erule eval.induct, blast) 
+apply blast 
+apply blast 
+apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
+apply (auto simp add: split_lemma)
+done
+
 
-    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
-                (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
-                ==> (WHILE e DO c, s) -[eval]-> s3"
+text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
+  using eval restricted to its functional part.  Note that the execution
+  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
+  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
+  functional on the argument (c,s).
+*}
+lemma com_Unique:
+ "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1  
+  ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
+apply (erule exec.induct, simp_all)
+      apply blast
+     apply force
+    apply blast
+   apply blast
+  apply blast
+ apply (blast elim: exec_WHILE_case)
+apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
+apply clarify
+apply (erule exec_WHILE_case, blast+) 
+done
+
+
+text{*Expression evaluation is functional, or deterministic*}
+theorem single_valued_eval: "single_valued eval"
+apply (unfold single_valued_def)
+apply (intro allI, rule impI) 
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (erule eval_induct)
+apply (drule_tac [4] com_Unique)
+apply (simp_all (no_asm_use))
+apply blast+
+done
+
+
+lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"
+by (erule eval_induct, simp_all)
+
+lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl]
+
+
+text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
+lemma while_true_E [rule_format]:
+     "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"
+by (erule exec.induct, auto)
+
+
+subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  
+       WHILE e DO c *}
+
+lemma while_if1 [rule_format]:
+     "(c',s) -[eval]-> t 
+      ==> (c' = WHILE e DO c) -->  
+          (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+lemma while_if2 [rule_format]:
+     "(c',s) -[eval]-> t
+      ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) -->  
+          (WHILE e DO c, s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+
+theorem while_if:
+     "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =   
+      ((WHILE e DO c, s) -[eval]-> t)"
+by (blast intro: while_if1 while_if2)
+
+
+
+subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
+                         and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
+
+lemma if_semi1 [rule_format]:
+     "(c',s) -[eval]-> t
+      ==> (c' = (IF e THEN c1 ELSE c2);;c) -->  
+          (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+lemma if_semi2 [rule_format]:
+     "(c',s) -[eval]-> t
+      ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) -->  
+          ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =   
+                  ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
+by (blast intro: if_semi1 if_semi2)
+
+
+
+subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
+                  and  VALOF c1;;c2 RESULTIS e
+ *}
+
+lemma valof_valof1 [rule_format]:
+     "(e',s) -|-> (v,s')  
+      ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) -->  
+          (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
+by (erule eval_induct, auto)
+
+
+lemma valof_valof2 [rule_format]:
+     "(e',s) -|-> (v,s')
+      ==> (e' = VALOF c1;;c2 RESULTIS e) -->  
+          (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
+by (erule eval_induct, auto)
+
+theorem valof_valof:
+     "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =   
+      ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
+by (blast intro: valof_valof1 valof_valof2)
+
+
+subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
+
+lemma valof_skip1 [rule_format]:
+     "(e',s) -|-> (v,s')
+      ==> (e' = VALOF SKIP RESULTIS e) -->  
+          (e, s) -|-> (v,s')"
+by (erule eval_induct, auto)
+
+lemma valof_skip2:
+     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
+by blast
+
+theorem valof_skip:
+     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
+by (blast intro: valof_skip1 valof_skip2)
+
+
+subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
+
+lemma valof_assign1 [rule_format]:
+     "(e',s) -|-> (v,s'')
+      ==> (e' = VALOF x:=e RESULTIS X x) -->  
+          (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
+apply (erule eval_induct)
+apply (simp_all del: fun_upd_apply, clarify, auto) 
+done
+
+lemma valof_assign2:
+     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
+by blast
+
+
 end
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,175 +0,0 @@
-(*  Title:      HOL/ex/comb.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson
-    Copyright   1996  University of Cambridge
-
-Combinatory Logic example: the Church-Rosser Theorem
-Curiously, combinators do not include free variables.
-
-Example taken from
-    J. Camilleri and T. F. Melham.
-    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
-    Report 265, University of Cambridge Computer Laboratory, 1992.
-
-HOL system proofs may be found in
-/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
-*)
-
-(*** Reflexive/Transitive closure preserves the Church-Rosser property 
-     So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
-***)
-
-val [_, spec_mp] = [spec] RL [mp];
-
-(*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
-Goalw [diamond_def]
-    "[| diamond(r);  (x,y):r^* |] ==> \ 
-\         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
-by (etac rtrancl_induct 1);
-by (Blast_tac 1);
-by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
-                          addSDs [spec_mp]) 1);
-qed_spec_mp "diamond_strip_lemmaE";
-
-Goal "diamond(r) ==> diamond(r^*)";
-by (stac diamond_def 1);  (*unfold only in goal, not in premise!*)
-by (rtac (impI RS allI RS allI) 1);
-by (etac rtrancl_induct 1);
-by (Blast_tac 1);
-by (best_tac  (*Seems to be a brittle, undirected search*)
-    (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
-            addEs [diamond_strip_lemmaE RS exE]) 1);
-qed "diamond_rtrancl";
-
-
-(*** Results about Contraction ***)
-
-(*Derive a case for each combinator constructor*)
-val K_contractE  = contract.mk_cases "K -1-> z";
-val S_contractE  = contract.mk_cases "S -1-> z";
-val Ap_contractE = contract.mk_cases "x##y -1-> z";
-
-AddSIs [contract.K, contract.S];
-AddIs  [contract.Ap1, contract.Ap2];
-AddSEs [K_contractE, S_contractE, Ap_contractE];
-
-Goalw [I_def] "I -1-> z ==> P";
-by (Blast_tac 1);
-qed "I_contract_E";
-AddSEs [I_contract_E];
-
-Goal "K##x -1-> z ==> (EX x'. z = K##x' & x -1-> x')";
-by (Blast_tac 1);
-qed "K1_contractD";
-AddSEs [K1_contractD];
-
-Goal "x ---> y ==> x##z ---> y##z";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
-qed "Ap_reduce1";
-
-Goal "x ---> y ==> z##x ---> z##y";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
-qed "Ap_reduce2";
-
-(** Counterexample to the diamond property for -1-> **)
-
-Goal "K##I##(I##I) -1-> I";
-by (rtac contract.K 1);
-qed "KIII_contract1";
-
-Goalw [I_def] "K##I##(I##I) -1-> K##I##((K##I)##(K##I))";
-by (Blast_tac 1);
-qed "KIII_contract2";
-
-Goal "K##I##((K##I)##(K##I)) -1-> I";
-by (Blast_tac 1);
-qed "KIII_contract3";
-
-Goalw [diamond_def] "~ diamond(contract)";
-by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
-qed "not_diamond_contract";
-
-
-
-(*** Results about Parallel Contraction ***)
-
-(*Derive a case for each combinator constructor*)
-val K_parcontractE  = parcontract.mk_cases "K =1=> z";
-val S_parcontractE  = parcontract.mk_cases "S =1=> z";
-val Ap_parcontractE = parcontract.mk_cases "x##y =1=> z";
-
-AddSIs [parcontract.refl, parcontract.K, parcontract.S];
-AddIs  [parcontract.Ap];
-AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-
-(*** Basic properties of parallel contraction ***)
-
-Goal "K##x =1=> z ==> (EX x'. z = K##x' & x =1=> x')";
-by (Blast_tac 1);
-qed "K1_parcontractD";
-AddSDs [K1_parcontractD];
-
-Goal "S##x =1=> z ==> (EX x'. z = S##x' & x =1=> x')";
-by (Blast_tac 1);
-qed "S1_parcontractD";
-AddSDs [S1_parcontractD];
-
-Goal "S##x##y =1=> z ==> (EX x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')";
-by (Blast_tac 1);
-qed "S2_parcontractD";
-AddSDs [S2_parcontractD];
-
-(*The rules above are not essential but make proofs much faster*)
-
-
-(*Church-Rosser property for parallel contraction*)
-Goalw [diamond_def] "diamond parcontract";
-by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract.induct 1 THEN prune_params_tac);
-by Safe_tac;
-by (ALLGOALS Blast_tac);
-qed "diamond_parcontract";
-
-
-(*** Equivalence of x--->y and x===>y ***)
-
-Goal "contract <= parcontract";
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (etac contract.induct 1);
-by (ALLGOALS Blast_tac);
-qed "contract_subset_parcontract";
-
-(*Reductions: simply throw together reflexivity, transitivity and
-  the one-step reductions*)
-
-AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
-
-(*Example only: not used*)
-Goalw [I_def] "I##x ---> x";
-by (Blast_tac 1);
-qed "reduce_I";
-
-Goal "parcontract <= contract^*";
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (etac parcontract.induct 1 THEN prune_params_tac);
-by (ALLGOALS Blast_tac);
-qed "parcontract_subset_reduce";
-
-Goal "contract^* = parcontract^*";
-by (REPEAT 
-    (resolve_tac [equalityI, 
-                  contract_subset_parcontract RS rtrancl_mono, 
-                  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
-qed "reduce_eq_parreduce";
-
-Goal "diamond(contract^*)";
-by (simp_tac (simpset() addsimps [reduce_eq_parreduce, diamond_rtrancl, 
-                                 diamond_parcontract]) 1);
-qed "diamond_reduce";
-
-
-writeln"Reached end of file.";
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/Comb.thy	Tue Apr 02 14:28:28 2002 +0200
@@ -1,74 +1,220 @@
-(*  Title:      HOL/ex/Comb.thy
+(*  Title:      HOL/Induct/Comb.thy
     ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1996  University of Cambridge
-
-Combinatory Logic example: the Church-Rosser Theorem
-Curiously, combinators do not include free variables.
-
-Example taken from
-    J. Camilleri and T. F. Melham.
-    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
-    Report 265, University of Cambridge Computer Laboratory, 1992.
 *)
 
+header {* Combinatory Logic example: the Church-Rosser Theorem *}
 
-Comb = Main +
+theory Comb = Main:
+
+text {*
+  Curiously, combinators do not include free variables.
+
+  Example taken from \cite{camilleri-melham}.
 
-(** Datatype definition of combinators S and K, with infixed application **)
+HOL system proofs may be found in the HOL distribution at
+   .../contrib/rule-induction/cl.ml
+*}
+
+subsection {* Definitions *}
+
+text {* Datatype definition of combinators @{text S} and @{text K}. *}
+
 datatype comb = K
               | S
               | "##" comb comb (infixl 90)
 
-(** Inductive definition of contractions, -1->
-             and (multi-step) reductions, --->
-**)
+text {*
+  Inductive definition of contractions, @{text "-1->"} and
+  (multi-step) reductions, @{text "--->"}.
+*}
+
 consts
   contract  :: "(comb*comb) set"
-  "-1->"    :: [comb,comb] => bool   (infixl 50)
-  "--->"    :: [comb,comb] => bool   (infixl 50)
+  "-1->"    :: "[comb,comb] => bool"   (infixl 50)
+  "--->"    :: "[comb,comb] => bool"   (infixl 50)
 
 translations
-  "x -1-> y" == "(x,y) : contract"
-  "x ---> y" == "(x,y) : contract^*"
+  "x -1-> y" == "(x,y) \<in> contract"
+  "x ---> y" == "(x,y) \<in> contract^*"
 
 inductive contract
-  intrs
-    K     "K##x##y -1-> x"
-    S     "S##x##y##z -1-> (x##z)##(y##z)"
-    Ap1   "x-1->y ==> x##z -1-> y##z"
-    Ap2   "x-1->y ==> z##x -1-> z##y"
+  intros
+    K:     "K##x##y -1-> x"
+    S:     "S##x##y##z -1-> (x##z)##(y##z)"
+    Ap1:   "x-1->y ==> x##z -1-> y##z"
+    Ap2:   "x-1->y ==> z##x -1-> z##y"
 
+text {*
+  Inductive definition of parallel contractions, @{text "=1=>"} and
+  (multi-step) parallel reductions, @{text "===>"}.
+*}
 
-(** Inductive definition of parallel contractions, =1=>
-             and (multi-step) parallel reductions, ===>
-**)
 consts
   parcontract :: "(comb*comb) set"
-  "=1=>"    :: [comb,comb] => bool   (infixl 50)
-  "===>"    :: [comb,comb] => bool   (infixl 50)
+  "=1=>"      :: "[comb,comb] => bool"   (infixl 50)
+  "===>"      :: "[comb,comb] => bool"   (infixl 50)
 
 translations
-  "x =1=> y" == "(x,y) : parcontract"
-  "x ===> y" == "(x,y) : parcontract^*"
+  "x =1=> y" == "(x,y) \<in> parcontract"
+  "x ===> y" == "(x,y) \<in> parcontract^*"
 
 inductive parcontract
-  intrs
-    refl  "x =1=> x"
-    K     "K##x##y =1=> x"
-    S     "S##x##y##z =1=> (x##z)##(y##z)"
-    Ap    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
+  intros
+    refl:  "x =1=> x"
+    K:     "K##x##y =1=> x"
+    S:     "S##x##y##z =1=> (x##z)##(y##z)"
+    Ap:    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
 
+text {*
+  Misc definitions.
+*}
 
-(*Misc definitions*)
 constdefs
   I :: comb
   "I == S##K##K"
 
-  (*confluence; Lambda/Commutation treats this more abstractly*)
   diamond   :: "('a * 'a)set => bool"	
-  "diamond(r) == ALL x y. (x,y):r --> 
-                  (ALL y'. (x,y'):r --> 
-                    (EX z. (y,z):r & (y',z) : r))"
+    --{*confluence; Lambda/Commutation treats this more abstractly*}
+  "diamond(r) == \<forall>x y. (x,y) \<in> r --> 
+                  (\<forall>y'. (x,y') \<in> r --> 
+                    (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
+
+
+subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
+
+text{*So does the Transitive closure, with a similar proof*}
+
+text{*Strip lemma.  
+   The induction hypothesis covers all but the last diamond of the strip.*}
+lemma diamond_strip_lemmaE [rule_format]: 
+    "[| diamond(r);  (x,y) \<in> r^* |] ==>   
+          \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
+apply (unfold diamond_def)
+apply (erule rtrancl_induct, blast, clarify)
+apply (drule spec, drule mp, assumption)
+apply (blast intro: rtrancl_trans [OF _ r_into_rtrancl])
+done
+
+lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)"
+apply (simp (no_asm_simp) add: diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule rtrancl_induct, blast)
+apply (best intro: rtrancl_trans [OF _ r_into_rtrancl] 
+            elim: diamond_strip_lemmaE [THEN exE])
+done
+
+
+subsection {* Non-contraction results *}
+
+text {* Derive a case for each combinator constructor. *}
+
+inductive_cases
+      K_contractE [elim!]: "K -1-> r"
+  and S_contractE [elim!]: "S -1-> r"
+  and Ap_contractE [elim!]: "p##q -1-> r"
+
+declare contract.K [intro!] contract.S [intro!]
+declare contract.Ap1 [intro] contract.Ap2 [intro]
+
+lemma I_contract_E [elim!]: "I -1-> z ==> P"
+by (unfold I_def, blast)
+
+lemma K1_contractD [elim!]: "K##x -1-> z ==> (\<exists>x'. z = K##x' & x -1-> x')"
+by blast
+
+lemma Ap_reduce1 [intro]: "x ---> y ==> x##z ---> y##z"
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_trans)+
+done
+
+lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y"
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_trans)+
+done
+
+(** Counterexample to the diamond property for -1-> **)
+
+lemma KIII_contract1: "K##I##(I##I) -1-> I"
+by (rule contract.K)
+
+lemma KIII_contract2: "K##I##(I##I) -1-> K##I##((K##I)##(K##I))"
+by (unfold I_def, blast)
+
+lemma KIII_contract3: "K##I##((K##I)##(K##I)) -1-> I"
+by blast
+
+lemma not_diamond_contract: "~ diamond(contract)"
+apply (unfold diamond_def) 
+apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3)
+done
+
+
+subsection {* Results about Parallel Contraction *}
+
+text {* Derive a case for each combinator constructor. *}
+
+inductive_cases
+      K_parcontractE [elim!]: "K =1=> r"
+  and S_parcontractE [elim!]: "S =1=> r"
+  and Ap_parcontractE [elim!]: "p##q =1=> r"
+
+declare parcontract.intros [intro]
+
+(*** Basic properties of parallel contraction ***)
+
+subsection {* Basic properties of parallel contraction *}
+
+lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')"
+by blast
+
+lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')"
+by blast
+
+lemma S2_parcontractD [dest!]:
+     "S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')"
+by blast
+
+text{*The rules above are not essential but make proofs much faster*}
+
+text{*Church-Rosser property for parallel contraction*}
+lemma diamond_parcontract: "diamond parcontract"
+apply (unfold diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule parcontract.induct, fast+)
+done
+
+text {*
+  \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
+*}
+
+lemma contract_subset_parcontract: "contract <= parcontract"
+apply (rule subsetI)
+apply (simp only: split_tupled_all)
+apply (erule contract.induct, blast+)
+done
+
+text{*Reductions: simply throw together reflexivity, transitivity and
+  the one-step reductions*}
+
+declare r_into_rtrancl [intro]  rtrancl_trans [intro]
+
+(*Example only: not used*)
+lemma reduce_I: "I##x ---> x"
+by (unfold I_def, blast)
+
+lemma parcontract_subset_reduce: "parcontract <= contract^*"
+apply (rule subsetI)
+apply (simp only: split_tupled_all)
+apply (erule parcontract.induct , blast+)
+done
+
+lemma reduce_eq_parreduce: "contract^* = parcontract^*"
+by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono] 
+         parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+
+
+lemma diamond_reduce: "diamond(contract^*)"
+by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract)
 
 end
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,233 +0,0 @@
-(*  Title:      HOL/Induct/Exp
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
-*)
-
-AddSIs [eval.N, eval.X];
-AddIs  [eval.Op, eval.valOf];
-
-val eval_elim_cases = 
-    map eval.mk_cases 
-       ["(N(n),sigma) -|-> (n',s')", 
-	"(X(x),sigma) -|-> (n,s')",
-	"(Op f a1 a2,sigma)  -|-> (n,s')",
-	"(VALOF c RESULTIS e, s) -|-> (n, s1)"];
-
-AddSEs eval_elim_cases;
-
-
-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];
-
-
-(** Make the induction rule look nicer -- though eta_contract makes the new
-    version look worse than it is...**)
-
-Goal "{((e,s),(n,s')). P e s n s'} = \
-\         Collect (split (%v. split (split P v)))";
-by (rtac Collect_cong 1);
-by (split_all_tac 1);
-by (Simp_tac 1);
-val split_lemma = result();
-
-(*New induction rule.  Note the form of the VALOF induction hypothesis*)
-val major::prems = goal thy
-  "[| (e,s) -|-> (n,s');                                         \
-\     !!n s. P (N n) s n s;                                      \
-\     !!s x. P (X x) s (s x) s;                                  \
-\     !!e0 e1 f n0 n1 s s0 s1.                                   \
-\        [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                   \
-\           (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                  \
-\        |] ==> P (Op f e0 e1) s (f n0 n1) s1;                   \
-\     !!c e n s s0 s1.                                           \
-\        [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
-\           (c,s) -[eval]-> s0;                                  \
-\           (e,s0) -|-> (n,s1); P e s0 n s1 |]                   \
-\        ==> P (VALOF c RESULTIS e) s n s1                       \
-\  |] ==> P e s n s'";
-by (rtac (major RS eval.induct) 1);
-by (blast_tac (claset() addIs prems) 1);
-by (blast_tac (claset() addIs prems) 1);
-by (blast_tac (claset() addIs prems) 1);
-by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
-by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
-qed "eval_induct";
-
-
-(*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
-  using eval restricted to its functional part.  Note that the execution
-  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
-  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,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 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 Blast_tac);
-qed "com_Unique";
-
-
-(*Expression evaluation is functional, or deterministic*)
-Goalw [single_valued_def] "single_valued 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);
-by (ALLGOALS Blast_tac);
-qed "single_valued_eval";
-
-
-Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-val lemma = result();
-bind_thm ("eval_N_E", refl RSN (2, lemma RS mp));
-
-AddSEs [eval_N_E];
-
-
-(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
-Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
-by (etac exec.induct 1);
-by Auto_tac;
-bind_thm ("while_true_E", refl RSN (2, result() RS mp));
-
-
-(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  WHILE e DO c **)
-
-Goal "(c',s) -[eval]-> t ==> \
-\              (c' = WHILE e DO c) --> \
-\              (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac); 
-bind_thm ("while_if1", refl RSN (2, result() RS mp));
-
-
-Goal "(c',s) -[eval]-> t ==> \
-\              (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
-\              (WHILE e DO c, s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac); 
-bind_thm ("while_if2", refl RSN (2, result() RS mp));
-
-
-Goal "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =  \
-\         ((WHILE e DO c, s) -[eval]-> t)";
-by (blast_tac (claset() addIs [while_if1, while_if2]) 1);
-qed "while_if";
-
-
-
-(** Equivalence of  (IF e THEN c1 ELSE c2);;c
-               and  IF e THEN (c1;;c) ELSE (c2;;c)   **)
-
-Goal "(c',s) -[eval]-> t ==> \
-\              (c' = (IF e THEN c1 ELSE c2);;c) --> \
-\              (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1); 
-bind_thm ("if_semi1", refl RSN (2, result() RS mp));
-
-
-Goal "(c',s) -[eval]-> t ==> \
-\              (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
-\              ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac); 
-bind_thm ("if_semi2", refl RSN (2, result() RS mp));
-
-
-Goal "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =  \
-\         ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)";
-by (blast_tac (claset() addIs [if_semi1, if_semi2]) 1);
-qed "if_semi";
-
-
-
-(** Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
-               and  VALOF c1;;c2 RESULTIS e
- **)
-
-Goal "(e',s) -|-> (v,s') ==> \
-\              (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
-\              (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1); 
-bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
-
-
-Goal "(e',s) -|-> (v,s') ==> \
-\              (e' = VALOF c1;;c2 RESULTIS e) --> \
-\              (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1); 
-bind_thm ("valof_valof2", refl RSN (2, result() RS mp));
-
-
-Goal "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =  \
-\         ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))";
-by (blast_tac (claset() addIs [valof_valof1, valof_valof2]) 1);
-qed "valof_valof";
-
-
-(** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
-
-Goal "(e',s) -|-> (v,s') ==> \
-\              (e' = VALOF SKIP RESULTIS e) --> \
-\              (e, s) -|-> (v,s')";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1); 
-bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
-
-Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
-by (Blast_tac 1);
-qed "valof_skip2";
-
-Goal "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))";
-by (blast_tac (claset() addIs [valof_skip1, valof_skip2]) 1);
-qed "valof_skip";
-
-
-(** 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'(x:=v)))";
-by (etac eval_induct 1);
-   by (ALLGOALS Asm_simp_tac);
-by (thin_tac "?PP-->?QQ" 1);
-by (Clarify_tac 1);
-by (Simp_tac 1);
-by (Blast_tac 1); 
-bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
-
-
-Goal "(e,s) -|-> (v,s') ==> \
-\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))";
-by (Blast_tac 1);
-qed "valof_assign2";
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/Exp.thy
--- a/src/HOL/Induct/Exp.thy	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      HOL/Induct/Exp
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
-*)
-
-Exp = Com +
-
-(** Evaluation of arithmetic expressions **)
-consts  eval    :: "((exp*state) * (nat*state)) set"
-       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
-translations
-    "esig -|-> (n,s)" <= "(esig,n,s) : eval"
-    "esig -|-> ns"    == "(esig,ns ) : eval"
-  
-inductive eval
-  intrs 
-    N      "(N(n),s) -|-> (n,s)"
-
-    X      "(X(x),s) -|-> (s(x),s)"
-
-    Op     "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
-            ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
-
-    valOf  "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
-            ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
-
-  monos exec_mono
-
-end
-
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,337 +0,0 @@
-(*  Title:      HOL/ex/LFilter
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-The "filter" functional for coinductive lists
-  --defined by a combination of induction and coinduction
-*)
-
-(*** findRel: basic laws ****)
-
-val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p";
-
-AddSEs [findRel_LConsE];
-
-
-Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
-by (etac findRel.induct 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "findRel_functional";
-
-Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
-by (etac findRel.induct 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "findRel_imp_LCons";
-
-Goal "(LNil,l): findRel p ==> R";
-by (blast_tac (claset() addEs [findRel.elim]) 1);
-qed "findRel_LNil";
-
-AddSEs [findRel_LNil];
-
-
-(*** Properties of Domain (findRel p) ***)
-
-Goal "LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
-by (case_tac "p x" 1);
-by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
-qed "LCons_Domain_findRel";
-
-Addsimps [LCons_Domain_findRel];
-
-val major::prems = 
-Goal "[| l: Domain (findRel p);                                   \
-\            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
-\         |] ==> Q";
-by (rtac (major RS DomainE) 1);
-by (ftac findRel_imp_LCons 1);
-by (REPEAT (eresolve_tac [exE,conjE] 1));
-by (hyp_subst_tac 1);
-by (REPEAT (ares_tac prems 1));
-qed "Domain_findRelE";
-
-val prems = goal thy
-    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
-by (Clarify_tac 1);
-by (etac findRel.induct 1);
-by (blast_tac (claset() addIs findRel.intrs @ prems) 1);
-by (blast_tac (claset() addIs findRel.intrs) 1);
-qed "Domain_findRel_mono";
-
-
-(*** find: basic equations ***)
-
-Goalw [find_def] "find p LNil = LNil";
-by (Blast_tac 1);
-qed "find_LNil";
-Addsimps [find_LNil];
-
-Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
-by (blast_tac (claset() addDs [findRel_functional]) 1);
-qed "findRel_imp_find";
-Addsimps [findRel_imp_find];
-
-Goal "p x ==> find p (LCons x l) = LCons x l";
-by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
-qed "find_LCons_found";
-Addsimps [find_LCons_found];
-
-Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
-by (Blast_tac 1);
-qed "diverge_find_LNil";
-Addsimps [diverge_find_LNil];
-
-Goal "~ (p x) ==> find p (LCons x l) = find p l";
-by (case_tac "LCons x l : Domain(findRel p)" 1);
-by (Asm_full_simp_tac 2);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
-qed "find_LCons_seek";
-Addsimps [find_LCons_seek];
-
-Goal "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (Asm_simp_tac 1);
-qed "find_LCons";
-
-
-
-(*** lfilter: basic equations ***)
-
-Goal "lfilter p LNil = LNil";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lfilter_LNil";
-Addsimps [lfilter_LNil];
-
-Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (Asm_simp_tac 1);
-qed "diverge_lfilter_LNil";
-
-Addsimps [diverge_lfilter_LNil];
-
-
-Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (Asm_simp_tac 1);
-qed "lfilter_LCons_found";
-(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
-  subsumes both*)
-
-
-Goal "(l, LCons x l') : findRel p \
-\              ==> lfilter p l = LCons x (lfilter p l')";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (Asm_simp_tac 1);
-qed "findRel_imp_lfilter";
-
-Addsimps [findRel_imp_lfilter];
-
-
-Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (case_tac "LCons x l : Domain(findRel p)" 1);
-by (Asm_full_simp_tac 2);
-by (etac Domain_findRelE 1);
-by (safe_tac (claset() delrules [conjI]));
-by (Asm_full_simp_tac 1);
-qed "lfilter_LCons_seek";
-
-
-Goal "lfilter p (LCons x l) = \
-\         (if p x then LCons x (lfilter p l) else lfilter p l)";
-by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1);
-qed "lfilter_LCons";
-
-AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-Addsimps [lfilter_LCons];
-
-
-Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)";
-by (rtac notI 1);
-by (etac Domain_findRelE 1);
-by (etac rev_mp 1);
-by (Asm_simp_tac 1);
-qed "lfilter_eq_LNil";
-
-
-Goal "lfilter p l = LCons x l' -->     \
-\              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
-by (stac (lfilter_def RS def_llist_corec) 1);
-by (case_tac "l : Domain(findRel p)" 1);
-by (etac Domain_findRelE 1);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "lfilter_eq_LCons";
-
-
-Goal "lfilter p l = LNil  |  \
-\         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
-by (case_tac "l : Domain(findRel p)" 1);
-by (Asm_simp_tac 2);
-by (blast_tac (claset() addSEs [Domain_findRelE] 
-                        addIs  [findRel_imp_lfilter]) 1);
-qed "lfilter_cases";
-
-
-(*** lfilter: simple facts by coinduction ***)
-
-Goal "lfilter (%x. True) l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lfilter_K_True";
-
-Goal "lfilter p (lfilter p l) = lfilter p l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-by Safe_tac;
-(*Cases: p x is true or false*)
-by (rtac (lfilter_cases RS disjE) 1);
-by (etac ssubst 1);
-by Auto_tac;
-qed "lfilter_idem";
-
-
-(*** Numerous lemmas required to prove lfilter_conj:
-     lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
- ***)
-
-Goal "(l,l') : findRel q \
-\           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
-by (etac findRel.induct 1);
-by (blast_tac (claset() addIs findRel.intrs) 1);
-by (blast_tac (claset() addIs findRel.intrs) 1);
-qed_spec_mp "findRel_conj_lemma";
-
-val findRel_conj = refl RSN (2, findRel_conj_lemma);
-
-Goal "(l,l'') : findRel (%x. p x & q x) \
-\              ==> (l, LCons x l') : findRel q --> ~ p x     \
-\                  --> l' : Domain (findRel (%x. p x & q x))";
-by (etac findRel.induct 1);
-by Auto_tac;
-qed_spec_mp "findRel_not_conj_Domain";
-
-
-Goal "(l,lxx) : findRel q ==> \
-\            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
-\            --> (l,lz) : findRel (%x. p x & q x)";
-by (etac findRel.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
-qed_spec_mp "findRel_conj2";
-
-
-Goal "(lx,ly) : findRel p \
-\              ==> ALL l. lx = lfilter q l \
-\                  --> l : Domain (findRel(%x. p x & q x))";
-by (etac findRel.induct 1);
-by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
-                        addIs  [findRel_conj]) 1);
-by Auto_tac;
-by (dtac (sym RS lfilter_eq_LCons) 1);
-by Auto_tac;
-by (dtac spec 1);
-by (dtac (refl RS rev_mp) 1);
-by (blast_tac (claset() addIs [findRel_conj2]) 1);
-qed_spec_mp "findRel_lfilter_Domain_conj";
-
-
-Goal "(l,l'') : findRel(%x. p x & q x) \
-\              ==> l'' = LCons y l' --> \
-\                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
-by (etac findRel.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
-qed_spec_mp "findRel_conj_lfilter";
-
-
-
-Goal "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)  \
-\         : llistD_Fun (range                                   \
-\                       (%u. (lfilter p (lfilter q u),          \
-\                             lfilter (%x. p x & q x) u)))";
-by (case_tac "l : Domain(findRel q)" 1);
-by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
-by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
-(*There are no qs in l: both lists are LNil*)
-by (Asm_simp_tac 2);
-by (etac Domain_findRelE 1);
-(*case q x*)
-by (case_tac "p x" 1);
-by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
-(*case q x and ~(p x) *)
-by (Asm_simp_tac 1);
-by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
-(*subcase: there is no p&q in l' and therefore none in l*)
-by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
-by (blast_tac (claset() addIs [findRel_not_conj_Domain]) 3);
-by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
-by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
-(*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
-by (Asm_simp_tac 2);
-(*subcase: there is a p&q in l' and therefore also one in l*)
-by (etac Domain_findRelE 1);
-by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
-by (blast_tac (claset() addIs [findRel_conj2]) 2);
-by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
-by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
-by (Asm_simp_tac 1);
-val lemma = result();
-
-
-Goal "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
-qed "lfilter_conj";
-
-
-(*** Numerous lemmas required to prove ??:
-     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
- ***)
-
-Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
-by (etac findRel.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "findRel_lmap_Domain";
-
-
-Goal "lmap f l = LCons x l' -->     \
-\              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
-by (stac (lmap_def RS def_llist_corec) 1);
-by (res_inst_tac [("l", "l")] llistE 1);
-by Auto_tac;
-qed_spec_mp "lmap_eq_LCons";
-
-
-Goal "(lx,ly) : findRel p ==>  \
-\    ALL l. lmap f l = lx --> ly = LCons x l' --> \
-\    (EX y l''. x = f y & l' = lmap f l'' &       \
-\    (l, LCons y l'') : findRel(%x. p(f x)))";
-by (etac findRel.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (safe_tac (claset() addSDs [lmap_eq_LCons]));
-by (blast_tac (claset() addIs findRel.intrs) 1);
-by (blast_tac (claset() addIs findRel.intrs) 1);
-qed_spec_mp "lmap_LCons_findRel_lemma";
-
-val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
-
-Goal "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-by Safe_tac;
-by (case_tac "lmap f l : Domain (findRel p)" 1);
-by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
-by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
-by (Asm_simp_tac 2);
-by (etac Domain_findRelE 1);
-by (ftac lmap_LCons_findRel 1);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
-qed "lfilter_lmap";
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/LFilter.thy
--- a/src/HOL/Induct/LFilter.thy	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/LFilter.thy	Tue Apr 02 14:28:28 2002 +0200
@@ -2,28 +2,271 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
-
-The "filter" functional for coinductive lists
-  --defined by a combination of induction and coinduction
 *)
 
-LFilter = LList +
+header {*The "filter" functional for coinductive lists
+  --defined by a combination of induction and coinduction*}
+
+theory LFilter = LList:
 
 consts
   findRel	:: "('a => bool) => ('a llist * 'a llist)set"
 
 inductive "findRel p"
-  intrs
-    found  "p x ==> (LCons x l, LCons x l) : findRel p"
-    seek   "[| ~p x;  (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
+  intros
+    found:  "p x ==> (LCons x l, LCons x l) \<in> findRel p"
+    seek:   "[| ~p x;  (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
+
+declare findRel.intros [intro]
 
 constdefs
-  find		:: ['a => bool, 'a llist] => 'a llist
+  find    :: "['a => bool, 'a llist] => 'a llist"
     "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
 
-  lfilter	:: ['a => bool, 'a llist] => 'a llist
+  lfilter :: "['a => bool, 'a llist] => 'a llist"
     "lfilter p l == llist_corec l (%l. case find p l of
                                             LNil => None
                                           | LCons y z => Some(y,z))"
 
+
+subsection {* findRel: basic laws *}
+
+inductive_cases
+  findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p"
+
+
+lemma findRel_functional [rule_format]:
+     "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"
+by (erule findRel.induct, auto)
+
+lemma findRel_imp_LCons [rule_format]:
+     "(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x"
+by (erule findRel.induct, auto)
+
+lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R"
+by (blast elim: findRel.cases)
+
+
+subsection {* Properties of Domain (findRel p) *}
+
+lemma LCons_Domain_findRel [simp]:
+     "LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))"
+by auto
+
+lemma Domain_findRel_iff:
+     "(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p &  p x)" 
+by (blast dest: findRel_imp_LCons) 
+
+lemma Domain_findRel_mono:
+    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"
+apply clarify
+apply (erule findRel.induct, blast+)
+done
+
+
+subsection {* find: basic equations *}
+
+lemma find_LNil [simp]: "find p LNil = LNil"
+by (unfold find_def, blast)
+
+lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'"
+apply (unfold find_def)
+apply (blast dest: findRel_functional)
+done
+
+lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l"
+by (blast intro: findRel_imp_find)
+
+lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil"
+by (unfold find_def, blast)
+
+lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l"
+apply (case_tac "LCons x l \<in> Domain (findRel p) ")
+ apply auto 
+apply (blast intro: findRel_imp_find)
+done
+
+lemma find_LCons [simp]:
+     "find p (LCons x l) = (if p x then LCons x l else find p l)"
+by (simp add: find_LCons_seek find_LCons_found)
+
+
+
+subsection {* lfilter: basic equations *}
+
+lemma lfilter_LNil [simp]: "lfilter p LNil = LNil"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma diverge_lfilter_LNil [simp]:
+     "l ~: Domain(findRel p) ==> lfilter p l = LNil"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lfilter_LCons_found:
+     "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma findRel_imp_lfilter [simp]:
+     "(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"
+apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+apply (case_tac "LCons x l \<in> Domain (findRel p) ")
+ apply (simp add: Domain_findRel_iff, auto) 
+done
+
+lemma lfilter_LCons [simp]:
+     "lfilter p (LCons x l) =  
+          (if p x then LCons x (lfilter p l) else lfilter p l)"
+by (simp add: lfilter_LCons_found lfilter_LCons_seek)
+
+declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!]
+
+
+lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" 
+apply (auto iff: Domain_findRel_iff)
+apply (rotate_tac 1, simp) 
+done
+
+lemma lfilter_eq_LCons [rule_format]:
+     "lfilter p l = LCons x l' -->      
+               (\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)"
+apply (subst lfilter_def [THEN def_llist_corec])
+apply (case_tac "l \<in> Domain (findRel p) ")
+ apply (auto iff: Domain_findRel_iff)
+done
+
+
+lemma lfilter_cases: "lfilter p l = LNil  |   
+          (\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)"
+apply (case_tac "l \<in> Domain (findRel p) ")
+apply (auto iff: Domain_findRel_iff)
+done
+
+
+subsection {* lfilter: simple facts by coinduction *}
+
+lemma lfilter_K_True: "lfilter (%x. True) l = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+apply safe
+txt{*Cases: p x is true or false*}
+apply (rule lfilter_cases [THEN disjE])
+ apply (erule ssubst, auto)
+done
+
+
+subsection {* Numerous lemmas required to prove @{text lfilter_conj} *}
+
+lemma findRel_conj_lemma [rule_format]:
+     "(l,l') \<in> findRel q  
+      ==> l' = LCons x l'' --> p x --> (l,l') \<in> findRel (%x. p x & q x)"
+by (erule findRel.induct, auto)
+
+lemmas findRel_conj = findRel_conj_lemma [OF _ refl]
+
+lemma findRel_not_conj_Domain [rule_format]:
+     "(l,l'') \<in> findRel (%x. p x & q x)  
+      ==> (l, LCons x l') \<in> findRel q --> ~ p x --> 
+          l' \<in> Domain (findRel (%x. p x & q x))"
+by (erule findRel.induct, auto)
+
+lemma findRel_conj2 [rule_format]:
+     "(l,lxx) \<in> findRel q 
+      ==> lxx = LCons x lx --> (lx,lz) \<in> findRel(%x. p x & q x) --> ~ p x  
+          --> (l,lz) \<in> findRel (%x. p x & q x)"
+by (erule findRel.induct, auto)
+
+lemma findRel_lfilter_Domain_conj [rule_format]:
+     "(lx,ly) \<in> findRel p  
+      ==> \<forall>l. lx = lfilter q l --> l \<in> Domain (findRel(%x. p x & q x))"
+apply (erule findRel.induct)
+ apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto)
+apply (drule sym [THEN lfilter_eq_LCons], auto)
+apply (drule spec)
+apply (drule refl [THEN rev_mp])
+apply (blast intro: findRel_conj2)
+done
+
+
+lemma findRel_conj_lfilter [rule_format]:
+     "(l,l'') \<in> findRel(%x. p x & q x)  
+      ==> l'' = LCons y l' --> 
+          (lfilter q l, LCons y (lfilter q l')) \<in> findRel p"
+by (erule findRel.induct, auto)
+
+lemma lfilter_conj_lemma:
+     "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)   
+      \<in> llistD_Fun (range (%u. (lfilter p (lfilter q u),           
+                                lfilter (%x. p x & q x) u)))"
+apply (case_tac "l \<in> Domain (findRel q)")
+ apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
+  prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono])
+ txt{*There are no qs in l: both lists are LNil*}
+ apply (simp_all add: Domain_findRel_iff, clarify) 
+txt{*case q x*}
+apply (case_tac "p x")
+ apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter])
+ txt{*case q x and ~(p x) *}
+apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))")
+ txt{*subcase: there is no p&q in l' and therefore none in l*}
+ apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
+  prefer 3 apply (blast intro: findRel_not_conj_Domain)
+ apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ")
+  prefer 3 apply (blast intro: findRel_lfilter_Domain_conj)
+ txt{*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*}
+ apply (simp_all add: Domain_findRel_iff, clarify) 
+txt{*subcase: there is a p&q in l' and therefore also one in l*}
+apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ")
+ prefer 2 apply (blast intro: findRel_conj2)
+apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p")
+ apply simp 
+apply (blast intro: findRel_conj_lfilter)
+done
+
+
+lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono])
+done
+
+
+subsection {* Numerous lemmas required to prove ??:
+     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
+ *}
+
+lemma findRel_lmap_Domain:
+     "(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)"
+by (erule findRel.induct, auto)
+
+lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' -->      
+               (\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')"
+apply (subst lmap_def [THEN def_llist_corec])
+apply (rule_tac l = "l" in llistE, auto)
+done
+
+
+lemma lmap_LCons_findRel_lemma [rule_format]:
+     "(lx,ly) \<in> findRel p
+      ==> \<forall>l. lmap f l = lx --> ly = LCons x l' -->  
+          (\<exists>y l''. x = f y & l' = lmap f l'' &        
+          (l, LCons y l'') \<in> findRel(%x. p(f x)))"
+apply (erule findRel.induct, simp_all)
+apply (blast dest!: lmap_eq_LCons)+
+done
+
+lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl]
+
+lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+apply safe
+apply (case_tac "lmap f l \<in> Domain (findRel p)")
+ apply (simp add: Domain_findRel_iff, clarify)
+ apply (frule lmap_LCons_findRel, force) 
+apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp)
+apply (blast intro: findRel_lmap_Domain)
+done
+
 end
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,876 +0,0 @@
-(*  Title:      HOL/Induct/LList
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
-*)
-
-bind_thm ("UN1_I", UNIV_I RS UN_I);
-
-(** Simplification **)
-
-Addsplits [option.split];
-
-(*This justifies using llist in other recursive type definitions*)
-Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
-by (rtac gfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "llist_mono";
-
-
-Goal "llist(A) = usum {Numb(0)} (uprod A (llist A))";
-let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (claset() addSIs (map rew llist.intrs)
-                       addEs [rew llist.elim]) 1)
-end;
-qed "llist_unfold";
-
-
-(*** Type checking by coinduction, using list_Fun 
-     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
-***)
-
-Goalw [list_Fun_def]
-    "[| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
-by (etac llist.coinduct 1);
-by (etac (subsetD RS CollectD) 1);
-by (assume_tac 1);
-qed "llist_coinduct";
-
-Goalw [list_Fun_def, NIL_def] "NIL: list_Fun A X";
-by (Fast_tac 1);
-qed "list_Fun_NIL_I";
-AddIffs [list_Fun_NIL_I];
-
-Goalw [list_Fun_def,CONS_def]
-    "[| M: A;  N: X |] ==> CONS M N : list_Fun A X";
-by (Fast_tac 1);
-qed "list_Fun_CONS_I";
-Addsimps [list_Fun_CONS_I];
-AddSIs   [list_Fun_CONS_I];
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw (llist.defs @ [list_Fun_def])
-    "M: llist(A) ==> M : list_Fun A (X Un llist(A))";
-by (etac (llist.mono RS gfp_fun_UnI2) 1);
-qed "list_Fun_llist_I";
-
-(*** LList_corec satisfies the desired recurion equation ***)
-
-(*A continuity result?*)
-Goalw [CONS_def] "CONS M (UN x. f(x)) = (UN x. CONS M (f x))";
-by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
-qed "CONS_UN1";
-
-Goalw [CONS_def] "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
-by (REPEAT (ares_tac [In1_mono,Scons_mono] 1));
-qed "CONS_mono";
-
-Addsimps [LList_corec_fun_def RS def_nat_rec_0,
-          LList_corec_fun_def RS def_nat_rec_Suc];
-
-(** The directions of the equality are proved separately **)
-
-Goalw [LList_corec_def]
-    "LList_corec a f <= \
-\    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
-by (rtac UN_least 1);
-by (case_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 
-			 UNIV_I RS UN_upper] 1));
-qed "LList_corec_subset1";
-
-Goalw [LList_corec_def]
-    "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <= \
-\    LList_corec a f";
-by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
-by Safe_tac;
-by (ALLGOALS (res_inst_tac [("a","Suc(?k)")] UN_I));
-by (ALLGOALS Asm_simp_tac);
-qed "LList_corec_subset2";
-
-(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
-Goal "LList_corec a f =  \
-\     (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
-by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
-                         LList_corec_subset2] 1));
-qed "LList_corec";
-
-(*definitional version of same*)
-val [rew] = 
-Goal "[| !!x. h(x) == LList_corec x f |]     \
-\     ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))";
-by (rewtac rew);
-by (rtac LList_corec 1);
-qed "def_LList_corec";
-
-(*A typical use of co-induction to show membership in the gfp. 
-  Bisimulation is  range(%x. LList_corec x f) *)
-Goal "LList_corec a f : llist UNIV";
-by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac LList_corec 1);
-by (Simp_tac 1);
-qed "LList_corec_type";
-
-
-(**** llist equality as a gfp; the bisimulation principle ****)
-
-(*This theorem is actually used, unlike the many similar ones in ZF*)
-Goal "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))";
-let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (claset() addSIs (map rew LListD.intrs)
-                      addEs [rew LListD.elim]) 1)
-end;
-qed "LListD_unfold";
-
-Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
-by (induct_thm_tac nat_less_induct "k" 1);
-by (safe_tac (claset() delrules [equalityI]));
-by (etac LListD.elim 1);
-by (safe_tac (claset() delrules [equalityI]));
-by (case_tac "n" 1);
-by (Asm_simp_tac 1);
-by (rename_tac "n'" 1);
-by (case_tac "n'" 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
-qed "LListD_implies_ntrunc_equality";
-
-(*The domain of the LListD relation*)
-Goalw (llist.defs @ [NIL_def, CONS_def])
-    "Domain (LListD(diag A)) <= llist(A)";
-by (rtac gfp_upperbound 1);
-(*avoids unfolding LListD on the rhs*)
-by (res_inst_tac [("P", "%x. Domain x <= ?B")] (LListD_unfold RS ssubst) 1);
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "Domain_LListD";
-
-(*This inclusion justifies the use of coinduction to show M=N*)
-Goal "LListD(diag A) <= diag(llist(A))";
-by (rtac subsetI 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by Safe_tac;
-by (rtac diag_eqI 1);
-by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
-          ntrunc_equality) 1);
-by (assume_tac 1);
-by (etac (DomainI RS (Domain_LListD RS subsetD)) 1);
-qed "LListD_subset_diag";
-
-
-(** Coinduction, using LListD_Fun
-    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
- **)
-
-Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
-by (REPEAT (ares_tac basic_monos 1));
-qed "LListD_Fun_mono";
-
-Goalw [LListD_Fun_def]
-    "[| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
-by (etac LListD.coinduct 1);
-by (etac (subsetD RS CollectD) 1);
-by (assume_tac 1);
-qed "LListD_coinduct";
-
-Goalw [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
-by (Fast_tac 1);
-qed "LListD_Fun_NIL_I";
-
-Goalw [LListD_Fun_def,CONS_def]
- "[| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
-by (Fast_tac 1);
-qed "LListD_Fun_CONS_I";
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw (LListD.defs @ [LListD_Fun_def])
-    "M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
-by (etac (LListD.mono RS gfp_fun_UnI2) 1);
-qed "LListD_Fun_LListD_I";
-
-
-(*This converse inclusion helps to strengthen LList_equalityI*)
-Goal "diag(llist(A)) <= LListD(diag A)";
-by (rtac subsetI 1);
-by (etac LListD_coinduct 1);
-by (rtac subsetI 1);
-by (etac diagE 1);
-by (etac ssubst 1);
-by (eresolve_tac [llist.elim] 1);
-by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I,
-				       LListD_Fun_CONS_I])));
-qed "diag_subset_LListD";
-
-Goal "LListD(diag A) = diag(llist(A))";
-by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
-                         diag_subset_LListD] 1));
-qed "LListD_eq_diag";
-
-Goal "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
-by (rtac (LListD_eq_diag RS subst) 1);
-by (rtac LListD_Fun_LListD_I 1);
-by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
-qed "LListD_Fun_diag_I";
-
-
-(** To show two LLists are equal, exhibit a bisimulation! 
-      [also admits true equality]
-   Replace "A" by some particular set, like {x.True}??? *)
-Goal "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
-\         |] ==>  M=N";
-by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
-by (etac LListD_coinduct 1);
-by (asm_simp_tac (simpset() addsimps [LListD_eq_diag]) 1);
-by Safe_tac;
-qed "LList_equalityI";
-
-
-(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
-
-(*We must remove Pair_eq because it may turn an instance of reflexivity
-  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
-  (or strengthen the Solver?) 
-*)
-Delsimps [Pair_eq];
-
-(*abstract proof using a bisimulation*)
-val [prem1,prem2] = 
-Goal
- "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
-\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
-\ ==> h1=h2";
-by (rtac ext 1);
-(*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "UNIV"),
-                  ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac prem1 1);
-by (stac prem2 1);
-by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
-				  UNIV_I RS LListD_Fun_CONS_I]) 1);
-qed "LList_corec_unique";
-
-val [prem] = 
-Goal 
- "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] \
-\ ==> h = (%x. LList_corec x f)";
-by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
-qed "equals_LList_corec";
-
-
-(** Obsolete LList_corec_unique proof: complete induction, not coinduction **)
-
-Goalw [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
-by (rtac ntrunc_one_In1 1);
-qed "ntrunc_one_CONS";
-
-Goalw [CONS_def]
-    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
-by (Simp_tac 1);
-qed "ntrunc_CONS";
-
-Addsimps [ntrunc_one_CONS, ntrunc_CONS];
-
-
-val [prem1,prem2] = 
-Goal 
- "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
-\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
-\ ==> h1=h2";
-by (rtac (ntrunc_equality RS ext) 1);
-by (rename_tac "x k" 1);
-by (res_inst_tac [("x", "x")] spec 1);
-by (induct_thm_tac nat_less_induct "k" 1);
-by (rename_tac "n" 1);
-by (rtac allI 1);
-by (rename_tac "y" 1);
-by (stac prem1 1);
-by (stac prem2 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (case_tac "n" 1);
-by (rename_tac "m" 2);
-by (case_tac "m" 2);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
-result();
-
-
-(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
-
-Goal "mono(CONS(M))";
-by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1));
-qed "Lconst_fun_mono";
-
-(* Lconst(M) = CONS M (Lconst M) *)
-bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_unfold)));
-
-(*A typical use of co-induction to show membership in the gfp.
-  The containing set is simply the singleton {Lconst(M)}. *)
-Goal "M:A ==> Lconst(M): llist(A)";
-by (rtac (singletonI RS llist_coinduct) 1);
-by Safe_tac;
-by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
-by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
-qed "Lconst_type";
-
-Goal "Lconst(M) = LList_corec M (%x. Some(x,x))";
-by (rtac (equals_LList_corec RS fun_cong) 1);
-by (Simp_tac 1);
-by (rtac Lconst 1);
-qed "Lconst_eq_LList_corec";
-
-(*Thus we could have used gfp in the definition of Lconst*)
-Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))";
-by (rtac (equals_LList_corec RS fun_cong) 1);
-by (Simp_tac 1);
-by (rtac (Lconst_fun_mono RS gfp_unfold) 1);
-qed "gfp_Lconst_eq_LList_corec";
-
-
-(*** Isomorphisms ***)
-
-Goal "inj Rep_LList";
-by (rtac inj_inverseI 1);
-by (rtac Rep_LList_inverse 1);
-qed "inj_Rep_LList";
-
-
-Goalw [LList_def] "x : llist (range Leaf) ==> x : LList";
-by (Asm_simp_tac 1);
-qed "LListI";
-
-Goalw [LList_def] "x : LList ==> x : llist (range Leaf)";
-by (Asm_simp_tac 1);
-qed "LListD";
-
-
-(** Distinctness of constructors **)
-
-Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil";
-by (stac (thm "Abs_LList_inject") 1);
-by (REPEAT (resolve_tac (llist.intrs @ [CONS_not_NIL, rangeI, 
-                                        LListI, Rep_LList RS LListD]) 1));
-qed "LCons_not_LNil";
-
-bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
-
-AddIffs [LCons_not_LNil, LNil_not_LCons];
-
-
-(** llist constructors **)
-
-Goalw [LNil_def] "Rep_LList LNil = NIL";
-by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1);
-qed "Rep_LList_LNil";
-
-Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)";
-by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse,
-                         rangeI, Rep_LList RS LListD] 1));
-qed "Rep_LList_LCons";
-
-(** Injectiveness of CONS and LCons **)
-
-Goalw [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
-by (fast_tac (claset() addSEs [Scons_inject]) 1);
-qed "CONS_CONS_eq2";
-
-bind_thm ("CONS_inject", CONS_CONS_eq RS iffD1 RS conjE);
-
-
-(*For reasoning about abstract llist constructors*)
-
-AddIs [Rep_LList RS LListD, LListI];
-AddIs llist.intrs;
-
-Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
-by (stac (thm "Abs_LList_inject") 1);
-by (auto_tac (claset(), simpset() addsimps [thm "Rep_LList_inject"])); 
-qed "LCons_LCons_eq";
-
-AddIffs [LCons_LCons_eq];
-
-Goal "CONS M N: llist(A) ==> M: A & N: llist(A)";
-by (etac llist.elim 1);
-by (etac CONS_neq_NIL 1);
-by (Fast_tac 1);
-qed "CONS_D2";
-
-
-(****** Reasoning about llist(A) ******)
-
-Addsimps [List_case_NIL, List_case_CONS];
-
-(*A special case of list_equality for functions over lazy lists*)
-val [Mlist,gMlist,NILcase,CONScase] = 
-Goal
- "[| M: llist(A); g(NIL): llist(A);                             \
-\    f(NIL)=g(NIL);                                             \
-\    !!x l. [| x:A;  l: llist(A) |] ==>                         \
-\           (f(CONS x l),g(CONS x l)) :                         \
-\               LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un  \
-\                                   diag(llist(A)))             \
-\ |] ==> f(M) = g(M)";
-by (rtac LList_equalityI 1);
-by (rtac (Mlist RS imageI) 1);
-by (rtac image_subsetI 1);
-by (etac llist.elim 1);
-by (etac ssubst 1);
-by (stac NILcase 1);
-by (rtac (gMlist RS LListD_Fun_diag_I) 1);
-by (etac ssubst 1);
-by (REPEAT (ares_tac [CONScase] 1));
-qed "LList_fun_equalityI";
-
-
-(*** The functional "Lmap" ***)
-
-Goal "Lmap f NIL = NIL";
-by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lmap_NIL";
-
-Goal "Lmap f (CONS M N) = CONS (f M) (Lmap f N)";
-by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lmap_CONS";
-
-Addsimps [Lmap_NIL, Lmap_CONS];
-
-(*Another type-checking proof by coinduction*)
-val [major,minor] = 
-Goal "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
-by (rtac (major RS imageI RS llist_coinduct) 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
-                      minor, imageI, UnI1] 1));
-qed "Lmap_type";
-
-(*This type checking rule synthesises a sufficiently large set for f*)
-Goal "M: llist(A) ==> Lmap f M: llist(f`A)";
-by (etac Lmap_type 1);
-by (etac imageI 1);
-qed "Lmap_type2";
-
-(** Two easy results about Lmap **)
-
-Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
-by (dtac imageI 1);
-by (etac LList_equalityI 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
-                      rangeI RS LListD_Fun_CONS_I] 1));
-qed "Lmap_compose";
-
-Goal "M: llist(A) ==> Lmap (%x. x) M = M";
-by (dtac imageI 1);
-by (etac LList_equalityI 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
-                      rangeI RS LListD_Fun_CONS_I] 1));
-qed "Lmap_ident";
-
-
-(*** Lappend -- its two arguments cause some complications! ***)
-
-Goalw [Lappend_def] "Lappend NIL NIL = NIL";
-by (rtac (LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lappend_NIL_NIL";
-
-Goalw [Lappend_def]
-    "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')";
-by (rtac (LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lappend_NIL_CONS";
-
-Goalw [Lappend_def]
-    "Lappend (CONS M M') N = CONS M (Lappend M' N)";
-by (rtac (LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lappend_CONS";
-
-Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
-          Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
-
-
-Goal "M: llist(A) ==> Lappend NIL M = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Lappend_NIL";
-
-Goal "M: llist(A) ==> Lappend M NIL = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Lappend_NIL2";
-
-Addsimps [Lappend_NIL, Lappend_NIL2];
-
-
-(** Alternative type-checking proofs for Lappend **)
-
-(*weak co-induction: bisimulation and case analysis on both variables*)
-Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
-by (res_inst_tac
-    [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
-by (Fast_tac 1);
-by Safe_tac;
-by (eres_inst_tac [("aa", "u")] llist.elim 1);
-by (eres_inst_tac [("aa", "v")] llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "Lappend_type";
-
-(*strong co-induction: bisimulation and case analysis on one variable*)
-Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
-by (res_inst_tac [("X", "(%u. Lappend u N)`llist(A)")] llist_coinduct 1);
-by (etac imageI 1);
-by (rtac image_subsetI 1);
-by (eres_inst_tac [("aa", "x")] llist.elim 1);
-by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
-by (Asm_simp_tac 1);
-qed "Lappend_type";
-
-(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
-
-(** llist_case: case analysis for 'a llist **)
-
-Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse,
-           Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
-
-Goalw [llist_case_def,LNil_def]  "llist_case c d LNil = c";
-by (Simp_tac 1);
-qed "llist_case_LNil";
-
-Goalw [llist_case_def,LCons_def]
-    "llist_case c d (LCons M N) = d M N";
-by (Simp_tac 1);
-qed "llist_case_LCons";
-
-(*Elimination is case analysis, not induction.*)
-val [prem1,prem2] = 
-Goalw [NIL_def,CONS_def]
-     "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P";
-by (rtac (Rep_LList RS LListD RS llist.elim) 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [Rep_LList_LNil RS sym, thm "Rep_LList_inject"]) 1);
-by (etac prem1 1); 
-by (etac (LListI RS thm "Rep_LList_cases") 1); 
-by (Clarify_tac 1);  
-by (asm_full_simp_tac
-    (simpset() addsimps [Rep_LList_LCons RS sym, thm "Rep_LList_inject"]) 1); 
-by (etac prem2 1); 
-qed "llistE";
-
-(** llist_corec: corecursion for 'a llist **)
-
-(*Lemma for the proof of llist_corec*)
-Goal "LList_corec a \
-\          (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) : \
-\       llist(range Leaf)";
-by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac LList_corec 1);
-by (Force_tac 1);
-qed "LList_corec_type2";
-
-Goalw [llist_corec_def,LNil_def,LCons_def]
-    "llist_corec a f =  \
-\    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
-by (stac LList_corec 1);
-by (case_tac "f a" 1);
-by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
-by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
-qed "llist_corec";
-
-(*definitional version of same*)
-val [rew] = 
-Goal "[| !!x. h(x) == llist_corec x f |] ==>     \
-\     h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))";
-by (rewtac rew);
-by (rtac llist_corec 1);
-qed "def_llist_corec";
-
-(**** Proofs about type 'a llist functions ****)
-
-(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
-
-Goalw [LListD_Fun_def]
-    "r <= (llist A) <*> (llist A) ==> \
-\           LListD_Fun (diag A) r <= (llist A) <*> (llist A)";
-by (stac llist_unfold 1);
-by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
-by (Fast_tac 1);
-qed "LListD_Fun_subset_Times_llist";
-
-Goal "prod_fun Rep_LList Rep_LList ` r <= \
-\    (llist(range Leaf)) <*> (llist(range Leaf))";
-by (fast_tac (claset() delrules [image_subsetI]
-		       addIs [Rep_LList RS LListD]) 1);
-qed "subset_Times_llist";
-
-Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
-\    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r";
-by Safe_tac;
-by (etac (subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
-qed "prod_fun_lemma";
-
-Goal "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) = \
-\    diag(llist(range Leaf))";
-by (rtac equalityI 1);
-by (Blast_tac 1);
-by (fast_tac (claset() delSWrapper "split_all_tac"
-		       addSEs [LListI RS Abs_LList_inverse RS subst]) 1);
-qed "prod_fun_range_eq_diag";
-
-(*Used with lfilter*)
-Goalw [llistD_Fun_def, prod_fun_def]
-    "A<=B ==> llistD_Fun A <= llistD_Fun B";
-by Auto_tac;
-by (rtac image_eqI 1);
-by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2);
-by (Force_tac 1);
-qed "llistD_Fun_mono";
-
-(** To show two llists are equal, exhibit a bisimulation! 
-      [also admits true equality] **)
-Goalw [llistD_Fun_def]
-    "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
-by (rtac (thm "Rep_LList_inject" RS iffD1) 1);
-by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList `r"),
-                  ("A", "range(Leaf)")] 
-        LList_equalityI 1);
-by (etac prod_fun_imageI 1);
-by (etac (image_mono RS subset_trans) 1);
-by (rtac (image_compose RS subst) 1);
-by (rtac (prod_fun_compose RS subst) 1);
-by (stac image_Un 1);
-by (stac prod_fun_range_eq_diag 1);
-by (rtac (LListD_Fun_subset_Times_llist RS prod_fun_lemma) 1);
-by (rtac (subset_Times_llist RS Un_least) 1);
-by (rtac diag_subset_Times 1);
-qed "llist_equalityI";
-
-(** Rules to prove the 2nd premise of llist_equalityI **)
-Goalw [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
-by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
-qed "llistD_Fun_LNil_I";
-
-Goalw [llistD_Fun_def,LCons_def]
-    "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
-by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
-by (etac prod_fun_imageI 1);
-qed "llistD_Fun_LCons_I";
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw [llistD_Fun_def] "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
-by (rtac (Rep_LList_inverse RS subst) 1);
-by (rtac prod_fun_imageI 1);
-by (stac image_Un 1);
-by (stac prod_fun_range_eq_diag 1);
-by (rtac (Rep_LList RS LListD RS LListD_Fun_diag_I) 1);
-qed "llistD_Fun_range_I";
-
-(*A special case of list_equality for functions over lazy lists*)
-val [prem1,prem2] =
-Goal "[| f(LNil)=g(LNil);                                                \
-\        !!x l. (f(LCons x l),g(LCons x l)) :                            \
-\               llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
-\     |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
-by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
-by (rtac rangeI 1);
-by (rtac subsetI 1);
-by (etac rangeE 1);
-by (etac ssubst 1);
-by (res_inst_tac [("l", "u")] llistE 1);
-by (etac ssubst 1);
-by (stac prem1 1);
-by (rtac llistD_Fun_range_I 1);
-by (etac ssubst 1);
-by (rtac prem2 1);
-qed "llist_fun_equalityI";
-
-(*simpset for llist bisimulations*)
-Addsimps [llist_case_LNil, llist_case_LCons, 
-          llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-
-
-(*** The functional "lmap" ***)
-
-Goal "lmap f LNil = LNil";
-by (rtac (lmap_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lmap_LNil";
-
-Goal "lmap f (LCons M N) = LCons (f M) (lmap f N)";
-by (rtac (lmap_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lmap_LCons";
-
-Addsimps [lmap_LNil, lmap_LCons];
-
-
-(** Two easy results about lmap **)
-
-Goal "lmap (f o g) l = lmap f (lmap g l)";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lmap_compose";
-
-Goal "lmap (%x. x) l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lmap_ident";
-
-
-(*** iterates -- llist_fun_equalityI cannot be used! ***)
-
-Goal "iterates f x = LCons x (iterates f (f x))";
-by (rtac (iterates_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "iterates";
-
-Goal "lmap f (iterates f x) = iterates f (f x)";
-by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
-    llist_equalityI 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
-by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
-by (Simp_tac 1);
-qed "lmap_iterates";
-
-Goal "iterates f x = LCons x (lmap f (iterates f x))";
-by (stac lmap_iterates 1);
-by (rtac iterates 1);
-qed "iterates_lmap";
-
-(*** A rather complex proof about iterates -- cf Andy Pitts ***)
-
-(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
-
-Goal "nat_rec (LCons b l) (%m. lmap(f)) n =      \
-\    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "fun_power_lmap";
-
-goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "fun_power_Suc";
-
-val Pair_cong = read_instantiate_sg (sign_of (theory "Product_Type"))
- [("f","Pair")] (standard(refl RS cong RS cong));
-
-(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
-  for all u and all n::nat.*)
-val [prem] = Goal "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
-by (rtac ext 1);
-by (res_inst_tac [("r", 
-   "UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
-\                    nat_rec (iterates f u) (%m y. lmap f y) n))")] 
-    llist_equalityI 1);
-by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
-by (Clarify_tac 1);
-by (stac iterates 1);
-by (stac prem 1);
-by (stac fun_power_lmap 1);
-by (stac fun_power_lmap 1);
-by (rtac llistD_Fun_LCons_I 1);
-by (rtac (lmap_iterates RS subst) 1);
-by (stac fun_power_Suc 1);
-by (stac fun_power_Suc 1);
-by (rtac (UN1_I RS UnI1) 1);
-by (rtac rangeI 1);
-qed "iterates_equality";
-
-
-(*** lappend -- its two arguments cause some complications! ***)
-
-Goalw [lappend_def] "lappend LNil LNil = LNil";
-by (rtac (llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lappend_LNil_LNil";
-
-Goalw [lappend_def]
-    "lappend LNil (LCons l l') = LCons l (lappend LNil l')";
-by (rtac (llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lappend_LNil_LCons";
-
-Goalw [lappend_def]
-    "lappend (LCons l l') N = LCons l (lappend l' N)";
-by (rtac (llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lappend_LCons";
-
-Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons];
-
-Goal "lappend LNil l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lappend_LNil";
-
-Goal "lappend l LNil = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lappend_LNil2";
-
-Addsimps [lappend_LNil, lappend_LNil2];
-
-(*The infinite first argument blocks the second*)
-Goal "lappend (iterates f x) N = iterates f x";
-by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
-    llist_equalityI 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac iterates 1);
-by (Simp_tac 1);
-qed "lappend_iterates";
-
-(** Two proofs that lmap distributes over lappend **)
-
-(*Long proof requiring case analysis on both both arguments*)
-Goal "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
-by (res_inst_tac 
-    [("r",  
-      "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] 
-    llist_equalityI 1);
-by (rtac UN1_I 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (res_inst_tac [("l", "l")] llistE 1);
-by (res_inst_tac [("l", "n")] llistE 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI]));
-qed "lmap_lappend_distrib";
-
-(*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
-Goal "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-qed "lmap_lappend_distrib";
-
-(*Without strong coinduction, three case analyses might be needed*)
-Goal "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)";
-by (res_inst_tac [("l","l1")] llist_fun_equalityI 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-qed "lappend_assoc";
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/LList.thy	Tue Apr 02 14:28:28 2002 +0200
@@ -1,13 +1,11 @@
-(*  Title:      HOL/LList.thy
+(*  Title:      HOL/Induct/LList.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Definition of type 'a llist by a greatest fixed point
-
 Shares NIL, CONS, List_case with List.thy
 
-Still needs filter and flatten functions -- hard because they need
+Still needs flatten function -- hard because it need
 bounds on the amount of lookahead required.
 
 Could try (but would it work for the gfp analogue of term?)
@@ -23,49 +21,53 @@
        (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
 *)
 
-LList = Main + SList +
+header {*Definition of type 'a llist by a greatest fixed point*}
+
+theory LList = Main + SList:
 
 consts
 
-  llist      :: 'a item set => 'a item set
-  LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
+  llist  :: "'a item set => 'a item set"
+  LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
 
 
 coinductive "llist(A)"
-  intrs
-    NIL_I  "NIL: llist(A)"
-    CONS_I "[| a: A;  M: llist(A) |] ==> CONS a M : llist(A)"
+  intros
+    NIL_I:  "NIL \<in> llist(A)"
+    CONS_I:         "[| a \<in> A;  M \<in> llist(A) |] ==> CONS a M \<in> llist(A)"
 
 coinductive "LListD(r)"
-  intrs
-    NIL_I  "(NIL, NIL) : LListD(r)"
-    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
-            |] ==> (CONS a M, CONS b N) : LListD(r)"
+  intros
+    NIL_I:  "(NIL, NIL) \<in> LListD(r)"
+    CONS_I:         "[| (a,b) \<in> r;  (M,N) \<in> LListD(r) |] 
+                     ==> (CONS a M, CONS b N) \<in> LListD(r)"
 
 
 typedef (LList)
-  'a llist = "llist(range Leaf) :: 'a item set" (llist.NIL_I)
+  'a llist = "llist(range Leaf) :: 'a item set"
+  by (blast intro: llist.NIL_I)
 
 constdefs
-  (*Now used exclusively for abbreviating the coinduction rule*)
-  list_Fun   :: ['a item set, 'a item set] => 'a item set
-     "list_Fun A X == {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+  list_Fun   :: "['a item set, 'a item set] => 'a item set"
+    --{*Now used exclusively for abbreviating the coinduction rule*}
+     "list_Fun A X == {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
 
   LListD_Fun :: 
       "[('a item * 'a item)set, ('a item * 'a item)set] => 
        ('a item * 'a item)set"
     "LListD_Fun r X ==   
        {z. z = (NIL, NIL) |   
-           (? M N a b. z = (CONS a M, CONS b N) & (a, b) : r & (M, N) : X)}"
+           (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
 
-  (*the abstract constructors*)
-  LNil       :: 'a llist
+  LNil :: "'a llist"
+     --{*abstract constructor*}
     "LNil == Abs_LList NIL"
 
-  LCons      :: ['a, 'a llist] => 'a llist
+  LCons :: "['a, 'a llist] => 'a llist"
+     --{*abstract constructor*}
     "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
 
-  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
+  llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
     "llist_case c d l == 
        List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
 
@@ -77,7 +79,7 @@
              k"
 
   LList_corec     :: "['a, 'a => ('b item * 'a) option] => 'b item"
-    "LList_corec a f == UN k. LList_corec_fun k f a"
+    "LList_corec a f == \<Union>k. LList_corec_fun k f a"
 
   llist_corec     :: "['a, 'a => ('b * 'a) option] => 'b llist"
     "llist_corec a f == 
@@ -93,41 +95,810 @@
 
 
 
-(*The case syntax for type 'a llist*)
+text{*The case syntax for type 'a llist*}
 translations
   "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
 
 
-(** Sample function definitions.  Item-based ones start with L ***)
+subsubsection{* Sample function definitions.  Item-based ones start with L *}
 
 constdefs
-  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
+  Lmap       :: "('a item => 'b item) => ('a item => 'b item)"
     "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
 
-  lmap       :: ('a=>'b) => ('a llist => 'b llist)
+  lmap       :: "('a=>'b) => ('a llist => 'b llist)"
     "lmap f l == llist_corec l (%z. case z of LNil => None 
                                            | LCons y z => Some(f(y), z))"
 
-  iterates   :: ['a => 'a, 'a] => 'a llist
+  iterates   :: "['a => 'a, 'a] => 'a llist"
     "iterates f a == llist_corec a (%x. Some((x, f(x))))"     
 
-  Lconst     :: 'a item => 'a item
-    "Lconst(M) == lfp(%N. CONS M N)"     
+  Lconst     :: "'a item => 'a item"
+    "Lconst(M) == lfp(%N. CONS M N)"
 
-(*Append generates its result by applying f, where
-    f((NIL,NIL))          = None
-    f((NIL, CONS N1 N2))  = Some((N1, (NIL,N2))
-    f((CONS M1 M2, N))    = Some((M1, (M2,N))
-*)
-
-  Lappend    :: ['a item, 'a item] => 'a item
+  Lappend    :: "['a item, 'a item] => 'a item"
    "Lappend M N == LList_corec (M,N)                                         
      (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2))))) 
                       (%M1 M2 N. Some((M1, (M2,N))))))"
 
-  lappend    :: ['a llist, 'a llist] => 'a llist
+  lappend    :: "['a llist, 'a llist] => 'a llist"
     "lappend l n == llist_corec (l,n)                                         
        (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2))))) 
                          (%l1 l2 n. Some((l1, (l2,n))))))"
 
+
+text{*Append generates its result by applying f, where
+    f((NIL,NIL))          = None
+    f((NIL, CONS N1 N2))  = Some((N1, (NIL,N2))
+    f((CONS M1 M2, N))    = Some((M1, (M2,N))
+*}
+
+text{*
+SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
+*}
+
+lemmas UN1_I = UNIV_I [THEN UN_I, standard]
+
+subsubsection{* Simplification *}
+
+declare option.split [split]
+
+text{*This justifies using llist in other recursive type definitions*}
+lemma llist_mono: "A<=B ==> llist(A) <= llist(B)"
+apply (unfold llist.defs )
+apply (rule gfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+
+lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))"
+  by (fast intro!: llist.intros [unfolded NIL_def CONS_def]
+           elim: llist.cases [unfolded NIL_def CONS_def])
+
+
+subsection{* Type checking by coinduction, using list_Fun 
+     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+*}
+
+lemma llist_coinduct: 
+    "[| M \<in> X;  X <= list_Fun A (X Un llist(A)) |] ==>  M \<in> llist(A)"
+apply (unfold list_Fun_def)
+apply (erule llist.coinduct)
+apply (erule subsetD [THEN CollectD], assumption)
+done
+
+lemma list_Fun_NIL_I [iff]: "NIL \<in> list_Fun A X"
+by (unfold list_Fun_def NIL_def, fast)
+
+lemma list_Fun_CONS_I [intro!,simp]: 
+    "[| M \<in> A;  N \<in> X |] ==> CONS M N \<in> list_Fun A X"
+apply (unfold list_Fun_def CONS_def, fast)
+done
+
+
+text{*Utilise the "strong" part, i.e. gfp(f)*}
+lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))"
+apply (unfold llist.defs list_Fun_def)
+apply (rule gfp_fun_UnI2) 
+apply (rule monoI, blast) 
+apply assumption
+done
+
+subsection{* LList_corec satisfies the desired recurion equation *}
+
+text{*A continuity result?*}
+lemma CONS_UN1: "CONS M (\<Union>x. f(x)) = (\<Union>x. CONS M (f x))"
+apply (unfold CONS_def)
+apply (simp add: In1_UN1 Scons_UN1_y)
+done
+
+lemma CONS_mono: "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'"
+apply (unfold CONS_def)
+apply (assumption | rule In1_mono Scons_mono)+
+done
+
+declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
+        LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
+
+subsubsection{* The directions of the equality are proved separately *}
+
+lemma LList_corec_subset1: 
+    "LList_corec a f <=  
+     (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
+apply (unfold LList_corec_def)
+apply (rule UN_least)
+apply (case_tac "k")
+apply (simp_all (no_asm_simp))
+apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
+done
+
+lemma LList_corec_subset2: 
+    "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <=  
+     LList_corec a f"
+apply (unfold LList_corec_def)
+apply (simp add: CONS_UN1, safe) 
+apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+ 
+done
+
+text{*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*}
+lemma LList_corec:
+     "LList_corec a f =   
+      (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
+by (rule equalityI LList_corec_subset1 LList_corec_subset2)+
+
+text{*definitional version of same*}
+lemma def_LList_corec: 
+     "[| !!x. h(x) == LList_corec x f |]      
+      ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
+by (simp add: LList_corec)
+
+text{*A typical use of co-induction to show membership in the gfp. 
+  Bisimulation is  range(%x. LList_corec x f) *}
+lemma LList_corec_type: "LList_corec a f \<in> llist UNIV"
+apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
+apply (rule rangeI, safe)
+apply (subst LList_corec, simp)
+done
+
+
+subsection{* llist equality as a gfp; the bisimulation principle *}
+
+text{*This theorem is actually used, unlike the many similar ones in ZF*}
+lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
+  by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
+           elim: LListD.cases [unfolded NIL_def CONS_def])
+
+lemma LListD_implies_ntrunc_equality [rule_format]:
+     "\<forall>M N. (M,N) \<in> LListD(diag A) --> ntrunc k M = ntrunc k N"
+apply (induct_tac "k" rule: nat_less_induct)
+apply (safe del: equalityI)
+apply (erule LListD.cases)
+apply (safe del: equalityI)
+apply (case_tac "n", simp)
+apply (rename_tac "n'")
+apply (case_tac "n'")
+apply (simp_all add: CONS_def less_Suc_eq)
+done
+
+text{*The domain of the LListD relation*}
+lemma Domain_LListD: 
+    "Domain (LListD(diag A)) <= llist(A)"
+apply (unfold llist.defs NIL_def CONS_def)
+apply (rule gfp_upperbound)
+txt{*avoids unfolding LListD on the rhs*}
+apply (rule_tac P = "%x. Domain x <= ?B" in LListD_unfold [THEN ssubst], simp)
+apply blast 
+done
+
+text{*This inclusion justifies the use of coinduction to show M=N*}
+lemma LListD_subset_diag: "LListD(diag A) <= diag(llist(A))"
+apply (rule subsetI)
+apply (rule_tac p = "x" in PairE, safe)
+apply (rule diag_eqI)
+apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption)
+apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
+done
+
+
+subsubsection{* Coinduction, using LListD_Fun
+    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+ *}
+
+lemma LListD_Fun_mono: "A<=B ==> LListD_Fun r A <= LListD_Fun r B"
+apply (unfold LListD_Fun_def)
+apply (assumption | rule basic_monos)+
+done
+
+lemma LListD_coinduct: 
+    "[| M \<in> X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M \<in> LListD(r)"
+apply (unfold LListD_Fun_def)
+apply (erule LListD.coinduct)
+apply (erule subsetD [THEN CollectD], assumption)
+done
+
+lemma LListD_Fun_NIL_I: "(NIL,NIL) \<in> LListD_Fun r s"
+by (unfold LListD_Fun_def NIL_def, fast)
+
+lemma LListD_Fun_CONS_I: 
+     "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (diag A) s"
+apply (unfold LListD_Fun_def CONS_def, blast)
+done
+
+text{*Utilise the "strong" part, i.e. gfp(f)*}
+lemma LListD_Fun_LListD_I:
+     "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))"
+apply (unfold LListD.defs LListD_Fun_def)
+apply (rule gfp_fun_UnI2) 
+apply (rule monoI, blast) 
+apply assumption
+done
+
+
+text{*This converse inclusion helps to strengthen LList_equalityI*}
+lemma diag_subset_LListD: "diag(llist(A)) <= LListD(diag A)"
+apply (rule subsetI)
+apply (erule LListD_coinduct)
+apply (rule subsetI)
+apply (erule diagE)
+apply (erule ssubst)
+apply (erule llist.cases)
+apply (simp_all add: diagI LListD_Fun_NIL_I LListD_Fun_CONS_I)
+done
+
+lemma LListD_eq_diag: "LListD(diag A) = diag(llist(A))"
+apply (rule equalityI LListD_subset_diag diag_subset_LListD)+
+done
+
+lemma LListD_Fun_diag_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (diag A) (X Un diag(llist(A)))"
+apply (rule LListD_eq_diag [THEN subst])
+apply (rule LListD_Fun_LListD_I)
+apply (simp add: LListD_eq_diag diagI)
+done
+
+
+subsubsection{* To show two LLists are equal, exhibit a bisimulation! 
+      [also admits true equality]
+   Replace "A" by some particular set, like {x.True}??? *}
+lemma LList_equalityI:
+     "[| (M,N) \<in> r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) |] 
+      ==>  M=N"
+apply (rule LListD_subset_diag [THEN subsetD, THEN diagE])
+apply (erule LListD_coinduct)
+apply (simp add: LListD_eq_diag, safe)
+done
+
+
+subsection{* Finality of llist(A): Uniqueness of functions defined by corecursion *}
+
+text{*We must remove Pair_eq because it may turn an instance of reflexivity
+  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
+  (or strengthen the Solver?) 
+*}
+declare Pair_eq [simp del]
+
+text{*abstract proof using a bisimulation*}
+lemma LList_corec_unique:
+ "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));   
+     !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |] 
+  ==> h1=h2"
+apply (rule ext)
+txt{*next step avoids an unknown (and flexflex pair) in simplification*}
+apply (rule_tac A = "UNIV" and r = "range(%u. (h1 u, h2 u))" 
+       in LList_equalityI)
+apply (rule rangeI, safe)
+apply (simp add: LListD_Fun_NIL_I UNIV_I [THEN LListD_Fun_CONS_I])
+done
+
+lemma equals_LList_corec:
+ "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |]  
+  ==> h = (%x. LList_corec x f)"
+by (simp add: LList_corec_unique LList_corec) 
+
+
+subsubsection{*Obsolete proof of @{text LList_corec_unique}: 
+               complete induction, not coinduction *}
+
+lemma ntrunc_one_CONS [simp]: "ntrunc (Suc 0) (CONS M N) = {}"
+by (simp add: CONS_def ntrunc_one_In1)
+
+lemma ntrunc_CONS [simp]: 
+    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"
+by (simp add: CONS_def)
+
+
+lemma
+ assumes prem1:
+          "!!x. h1 x = (case f x of None => NIL | Some(z,w) => CONS z (h1 w))"
+     and prem2:
+          "!!x. h2 x = (case f x of None => NIL | Some(z,w) => CONS z (h2 w))"
+ shows "h1=h2"
+apply (rule ntrunc_equality [THEN ext])
+apply (rule_tac x = "x" in spec)
+apply (induct_tac "k" rule: nat_less_induct)
+apply (rename_tac "n")
+apply (rule allI)
+apply (subst prem1)
+apply (subst prem2, simp)
+apply (intro strip) 
+apply (case_tac "n") 
+apply (rename_tac [2] "m")
+apply (case_tac [2] "m")
+apply simp_all
+done
+
+
+subsection{*Lconst: defined directly by lfp *}
+
+text{*But it could be defined by corecursion.*}
+
+lemma Lconst_fun_mono: "mono(CONS(M))"
+apply (rule monoI subset_refl CONS_mono)+
+apply assumption 
+done
+
+text{* Lconst(M) = CONS M (Lconst M) *}
+lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]]
+
+text{*A typical use of co-induction to show membership in the gfp.
+  The containing set is simply the singleton {Lconst(M)}. *}
+lemma Lconst_type: "M\<in>A ==> Lconst(M): llist(A)"
+apply (rule singletonI [THEN llist_coinduct], safe)
+apply (rule_tac P = "%u. u \<in> ?A" in Lconst [THEN ssubst])
+apply (assumption | rule list_Fun_CONS_I singletonI UnI1)+
+done
+
+lemma Lconst_eq_LList_corec: "Lconst(M) = LList_corec M (%x. Some(x,x))"
+apply (rule equals_LList_corec [THEN fun_cong], simp)
+apply (rule Lconst)
+done
+
+text{*Thus we could have used gfp in the definition of Lconst*}
+lemma gfp_Lconst_eq_LList_corec: "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))"
+apply (rule equals_LList_corec [THEN fun_cong], simp)
+apply (rule Lconst_fun_mono [THEN gfp_unfold])
+done
+
+
+subsection{* Isomorphisms *}
+
+lemma inj_Rep_LList: "inj Rep_LList"
+apply (rule inj_inverseI)
+apply (rule Rep_LList_inverse)
+done
+
+
+lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList"
+by (unfold LList_def, simp)
+
+lemma LListD: "x \<in> LList ==> x \<in> llist (range Leaf)"
+by (unfold LList_def, simp)
+
+
+subsubsection{* Distinctness of constructors *}
+
+lemma LCons_not_LNil [iff]: "~ LCons x xs = LNil"
+apply (unfold LNil_def LCons_def)
+apply (subst Abs_LList_inject)
+apply (rule llist.intros CONS_not_NIL rangeI LListI Rep_LList [THEN LListD])+
+done
+
+lemmas LNil_not_LCons [iff] = LCons_not_LNil [THEN not_sym, standard]
+
+
+subsubsection{* llist constructors *}
+
+lemma Rep_LList_LNil: "Rep_LList LNil = NIL"
+apply (unfold LNil_def)
+apply (rule llist.NIL_I [THEN LListI, THEN Abs_LList_inverse])
+done
+
+lemma Rep_LList_LCons: "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)"
+apply (unfold LCons_def)
+apply (rule llist.CONS_I [THEN LListI, THEN Abs_LList_inverse] 
+            rangeI Rep_LList [THEN LListD])+
+done
+
+subsubsection{* Injectiveness of CONS and LCons *}
+
+lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')"
+apply (unfold CONS_def)
+apply (fast elim!: Scons_inject)
+done
+
+lemmas CONS_inject = CONS_CONS_eq [THEN iffD1, THEN conjE, standard]
+
+
+text{*For reasoning about abstract llist constructors*}
+
+declare Rep_LList [THEN LListD, intro] LListI [intro]
+declare llist.intros [intro]
+
+lemma LCons_LCons_eq [iff]: "(LCons x xs=LCons y ys) = (x=y & xs=ys)"
+apply (unfold LCons_def)
+apply (subst Abs_LList_inject)
+apply (auto simp add: Rep_LList_inject)
+done
+
+lemma LList_fun_equalityI: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
+apply (erule llist.cases)
+apply (erule CONS_neq_NIL, fast)
+done
+
+
+subsection{* Reasoning about llist(A) *}
+
+text{*A special case of list_equality for functions over lazy lists*}
+lemma LList_fun_equalityI:
+ "[| M \<in> llist(A); g(NIL): llist(A);                              
+     f(NIL)=g(NIL);                                              
+     !!x l. [| x\<in>A;  l \<in> llist(A) |] ==>                          
+            (f(CONS x l),g(CONS x l)) \<in>                          
+                LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un   
+                                    diag(llist(A)))              
+  |] ==> f(M) = g(M)"
+apply (rule LList_equalityI)
+apply (erule imageI)
+apply (rule image_subsetI)
+apply (erule_tac aa=x in llist.cases)
+apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) 
+done
+
+
+subsection{* The functional "Lmap" *}
+
+lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
+by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
+
+lemma Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
+by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
+
+
+
+text{*Another type-checking proof by coinduction*}
+lemma Lmap_type:
+     "[| M \<in> llist(A);  !!x. x\<in>A ==> f(x):B |] ==> Lmap f M \<in> llist(B)"
+apply (erule imageI [THEN llist_coinduct], safe)
+apply (erule llist.cases, simp_all)
+done
+
+text{*This type checking rule synthesises a sufficiently large set for f*}
+lemma Lmap_type2: "M \<in> llist(A) ==> Lmap f M \<in> llist(f`A)"
+apply (erule Lmap_type)
+apply (erule imageI)
+done
+
+subsubsection{* Two easy results about Lmap *}
+
+lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
+apply (unfold o_def)
+apply (drule imageI)
+apply (erule LList_equalityI, safe)
+apply (erule llist.cases, simp_all)
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply assumption  
+done
+
+lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M"
+apply (drule imageI)
+apply (erule LList_equalityI, safe)
+apply (erule llist.cases, simp_all)
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply assumption 
+done
+
+
+subsection{* Lappend -- its two arguments cause some complications! *}
+
+lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL"
+apply (unfold Lappend_def)
+apply (rule LList_corec [THEN trans], simp)
+done
+
+lemma Lappend_NIL_CONS [simp]: 
+    "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
+apply (unfold Lappend_def)
+apply (rule LList_corec [THEN trans], simp)
+done
+
+lemma Lappend_CONS [simp]: 
+    "Lappend (CONS M M') N = CONS M (Lappend M' N)"
+apply (unfold Lappend_def)
+apply (rule LList_corec [THEN trans], simp)
+done
+
+declare llist.intros [simp] LListD_Fun_CONS_I [simp] 
+        range_eqI [simp] image_eqI [simp]
+
+
+lemma Lappend_NIL [simp]: "M \<in> llist(A) ==> Lappend NIL M = M"
+by (erule LList_fun_equalityI, simp_all)
+
+lemma Lappend_NIL2: "M \<in> llist(A) ==> Lappend M NIL = M"
+by (erule LList_fun_equalityI, simp_all)
+
+
+subsubsection{* Alternative type-checking proofs for Lappend *}
+
+text{*weak co-induction: bisimulation and case analysis on both variables*}
+lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
+apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct)
+apply fast
+apply safe
+apply (erule_tac aa = "u" in llist.cases)
+apply (erule_tac aa = "v" in llist.cases, simp_all)
+apply blast
+done
+
+text{*strong co-induction: bisimulation and case analysis on one variable*}
+lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
+apply (rule_tac X = " (%u. Lappend u N) `llist (A) " in llist_coinduct)
+apply (erule imageI)
+apply (rule image_subsetI)
+apply (erule_tac aa = "x" in llist.cases)
+apply (simp add: list_Fun_llist_I, simp)
+done
+
+subsection{* Lazy lists as the type 'a llist -- strongly typed versions of above *}
+
+subsubsection{* llist_case: case analysis for 'a llist *}
+
+declare LListI [THEN Abs_LList_inverse, simp]
+declare Rep_LList_inverse [simp]
+declare Rep_LList [THEN LListD, simp]
+declare rangeI [simp] inj_Leaf [simp] 
+
+lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
+by (unfold llist_case_def LNil_def, simp)
+
+lemma llist_case_LCons [simp]: 
+    "llist_case c d (LCons M N) = d M N"
+apply (unfold llist_case_def LCons_def, simp)
+done
+
+text{*Elimination is case analysis, not induction.*}
+lemma llistE: "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P"
+apply (rule Rep_LList [THEN LListD, THEN llist.cases])
+ apply (simp add: Rep_LList_LNil [symmetric] Rep_LList_inject)
+ apply blast 
+apply (erule LListI [THEN Rep_LList_cases], clarify)
+apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast) 
+done
+
+subsubsection{* llist_corec: corecursion for 'a llist *}
+
+text{*Lemma for the proof of llist_corec*}
+lemma LList_corec_type2:
+     "LList_corec a  
+           (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) 
+       \<in> llist(range Leaf)"
+apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
+apply (rule rangeI, safe)
+apply (subst LList_corec, force)
+done
+
+lemma llist_corec: 
+    "llist_corec a f =   
+     (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
+apply (unfold llist_corec_def LNil_def LCons_def)
+apply (subst LList_corec)
+apply (case_tac "f a")
+apply (simp add: LList_corec_type2)
+apply (force simp add: LList_corec_type2)
+done
+
+text{*definitional version of same*}
+lemma def_llist_corec: 
+     "[| !!x. h(x) == llist_corec x f |] ==>      
+      h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
+by (simp add: llist_corec)
+
+subsection{* Proofs about type 'a llist functions *}
+
+subsection{* Deriving llist_equalityI -- llist equality is a bisimulation *}
+
+lemma LListD_Fun_subset_Times_llist: 
+    "r <= (llist A) <*> (llist A) ==>  
+            LListD_Fun (diag A) r <= (llist A) <*> (llist A)"
+apply (unfold LListD_Fun_def)
+apply (subst llist_unfold)
+apply (simp add: NIL_def CONS_def, fast)
+done
+
+lemma subset_Times_llist:
+     "prod_fun Rep_LList Rep_LList ` r <=  
+     (llist(range Leaf)) <*> (llist(range Leaf))"
+by (blast intro: Rep_LList [THEN LListD])
+
+lemma prod_fun_lemma:
+     "r <= (llist(range Leaf)) <*> (llist(range Leaf)) 
+      ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r"
+apply safe
+apply (erule subsetD [THEN SigmaE2], assumption)
+apply (simp add: LListI [THEN Abs_LList_inverse])
+done
+
+lemma prod_fun_range_eq_diag:
+     "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) =  
+      diag(llist(range Leaf))"
+apply (rule equalityI, blast) 
+apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
+done
+
+text{*Used with lfilter*}
+lemma llistD_Fun_mono: 
+    "A<=B ==> llistD_Fun A <= llistD_Fun B"
+apply (unfold llistD_Fun_def prod_fun_def, auto)
+apply (rule image_eqI)
+ prefer 2 apply (blast intro: rev_subsetD [OF _ LListD_Fun_mono], force)
+done
+
+subsubsection{* To show two llists are equal, exhibit a bisimulation! 
+      [also admits true equality] *}
+lemma llist_equalityI: 
+    "[| (l1,l2) \<in> r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"
+apply (unfold llistD_Fun_def)
+apply (rule Rep_LList_inject [THEN iffD1])
+apply (rule_tac r = "prod_fun Rep_LList Rep_LList `r" and A = "range (Leaf) " in LList_equalityI)
+apply (erule prod_fun_imageI)
+apply (erule image_mono [THEN subset_trans])
+apply (rule image_compose [THEN subst])
+apply (rule prod_fun_compose [THEN subst])
+apply (subst image_Un)
+apply (subst prod_fun_range_eq_diag)
+apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
+apply (rule subset_Times_llist [THEN Un_least])
+apply (rule diag_subset_Times)
+done
+
+subsubsection{* Rules to prove the 2nd premise of llist_equalityI *}
+lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \<in> llistD_Fun(r)"
+apply (unfold llistD_Fun_def LNil_def)
+apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI])
+done
+
+lemma llistD_Fun_LCons_I [simp]: 
+    "(l1,l2):r ==> (LCons x l1, LCons x l2) \<in> llistD_Fun(r)"
+apply (unfold llistD_Fun_def LCons_def)
+apply (rule rangeI [THEN LListD_Fun_CONS_I, THEN prod_fun_imageI])
+apply (erule prod_fun_imageI)
+done
+
+text{*Utilise the "strong" part, i.e. gfp(f)*}
+lemma llistD_Fun_range_I: "(l,l) \<in> llistD_Fun(r Un range(%x.(x,x)))"
+apply (unfold llistD_Fun_def)
+apply (rule Rep_LList_inverse [THEN subst])
+apply (rule prod_fun_imageI)
+apply (subst image_Un)
+apply (subst prod_fun_range_eq_diag)
+apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
+done
+
+text{*A special case of list_equality for functions over lazy lists*}
+lemma llist_fun_equalityI:
+     "[| f(LNil)=g(LNil);                                                 
+         !!x l. (f(LCons x l),g(LCons x l)) 
+                \<in> llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))    
+      |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"
+apply (rule_tac r = "range (%u. (f (u),g (u))) " in llist_equalityI)
+apply (rule rangeI, clarify) 
+apply (rule_tac l = "u" in llistE)
+apply (simp_all add: llistD_Fun_range_I) 
+done
+
+
+subsection{* The functional "lmap" *}
+
+lemma lmap_LNil [simp]: "lmap f LNil = LNil"
+by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
+by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
+
+
+subsubsection{* Two easy results about lmap *}
+
+lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+lemma lmap_ident [simp]: "lmap (%x. x) l = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+
+subsection{* iterates -- llist_fun_equalityI cannot be used! *}
+
+lemma iterates: "iterates f x = LCons x (iterates f (f x))"
+by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
+apply (rule_tac r = "range (%u. (lmap f (iterates f u),iterates f (f u))) " in llist_equalityI)
+apply (rule rangeI, safe)
+apply (rule_tac x1 = "f (u) " in iterates [THEN ssubst])
+apply (rule_tac x1 = "u" in iterates [THEN ssubst], simp)
+done
+
+lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
+apply (subst lmap_iterates)
+apply (rule iterates)
+done
+
+subsection{* A rather complex proof about iterates -- cf Andy Pitts *}
+
+subsubsection{* Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) *}
+
+lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n =       
+     LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"
+apply (induct_tac "n", simp_all)
+done
+
+lemma fun_power_Suc: "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)"
+by (induct_tac "n", simp_all)
+
+lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair]
+
+
+text{*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
+  for all u and all n::nat.*}
+lemma iterates_equality:
+     "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"
+apply (rule ext)
+apply (rule_tac 
+       r = "\<Union>u. range (%n. (nat_rec (h u) (%m y. lmap f y) n, 
+                             nat_rec (iterates f u) (%m y. lmap f y) n))" 
+       in llist_equalityI)
+apply (rule UN1_I range_eqI Pair_cong nat_rec_0 [symmetric])+
+apply clarify
+apply (subst iterates, atomize)
+apply (drule_tac x=u in spec) 
+apply (erule ssubst) 
+apply (subst fun_power_lmap)
+apply (subst fun_power_lmap)
+apply (rule llistD_Fun_LCons_I)
+apply (rule lmap_iterates [THEN subst])
+apply (subst fun_power_Suc)
+apply (subst fun_power_Suc, blast)
+done
+
+
+subsection{* lappend -- its two arguments cause some complications! *}
+
+lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
+apply (unfold lappend_def)
+apply (rule llist_corec [THEN trans], simp)
+done
+
+lemma lappend_LNil_LCons [simp]: 
+    "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
+apply (unfold lappend_def)
+apply (rule llist_corec [THEN trans], simp)
+done
+
+lemma lappend_LCons [simp]: 
+    "lappend (LCons l l') N = LCons l (lappend l' N)"
+apply (unfold lappend_def)
+apply (rule llist_corec [THEN trans], simp)
+done
+
+lemma lappend_LNil [simp]: "lappend LNil l = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+lemma lappend_LNil2 [simp]: "lappend l LNil = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+
+text{*The infinite first argument blocks the second*}
+lemma lappend_iterates [simp]: "lappend (iterates f x) N = iterates f x"
+apply (rule_tac r = "range (%u. (lappend (iterates f u) N,iterates f u))" 
+       in llist_equalityI)
+apply (rule rangeI, safe)
+apply (subst iterates, simp)
+done
+
+subsubsection{* Two proofs that lmap distributes over lappend *}
+
+text{*Long proof requiring case analysis on both both arguments*}
+lemma lmap_lappend_distrib:
+     "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
+apply (rule_tac r = "\<Union>n. range (%l. (lmap f (lappend l n),
+                                      lappend (lmap f l) (lmap f n)))" 
+       in llist_equalityI)
+apply (rule UN1_I)
+apply (rule rangeI, safe)
+apply (rule_tac l = "l" in llistE)
+apply (rule_tac l = "n" in llistE, simp_all)
+apply (blast intro: llistD_Fun_LCons_I) 
+done
+
+text{*Shorter proof of theorem above using llist_equalityI as strong coinduction*}
+lemma lmap_lappend_distrib:
+     "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp)
+apply simp
+done
+
+text{*Without strong coinduction, three case analyses might be needed*}
+lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
+apply (rule_tac l = "l1" in llist_fun_equalityI, simp)
+apply simp
+done
+
 end
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,209 +0,0 @@
-(*  Title:      HOL/ex/pl.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow & Lawrence C Paulson
-    Copyright   1994  TU Muenchen & University of Cambridge
-
-Soundness and completeness of propositional logic w.r.t. truth-tables.
-
-Prove: If H|=p then G|=p where G:Fin(H)
-*)
-
-(** Monotonicity **)
-Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
-by (rtac lfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "thms_mono";
-
-(*Rule is called I for Identity Combinator, not for Introduction*)
-Goal "H |- p->p";
-by (best_tac (claset() addIs [thms.K,thms.S,thms.MP]) 1);
-qed "thms_I";
-
-(** Weakening, left and right **)
-
-(* "[| G<=H;  G |- p |] ==> H |- p"
-   This order of premises is convenient with RS
-*)
-bind_thm ("weaken_left", (thms_mono RS subsetD));
-
-(* H |- p ==> insert(a,H) |- p *)
-val weaken_left_insert = subset_insertI RS weaken_left;
-
-val weaken_left_Un1  =    Un_upper1 RS weaken_left;
-val weaken_left_Un2  =    Un_upper2 RS weaken_left;
-
-Goal "H |- q ==> H |- p->q";
-by (fast_tac (claset() addIs [thms.K,thms.MP]) 1);
-qed "weaken_right";
-
-(*The deduction theorem*)
-Goal "insert p H |- q  ==>  H |- p->q";
-by (etac thms.induct 1);
-by (ALLGOALS 
-    (fast_tac (claset() addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
-			       thms.S RS thms.MP RS thms.MP, weaken_right])));
-qed "deduction";
-
-
-(* "[| insert p H |- q; H |- p |] ==> H |- q"
-    The cut rule - not used
-*)
-val cut = deduction RS thms.MP;
-
-(* H |- false ==> H |- p *)
-val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
-
-(* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
-bind_thm ("thms_notE", (thms.MP RS thms_falseE));
-
-
-(*Soundness of the rules wrt truth-table semantics*)
-Goalw [sat_def] "H |- p ==> H |= p";
-by (etac thms.induct 1);
-by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS Asm_simp_tac);
-qed "soundness";
-
-(*** Towards the completeness proof ***)
-
-Goal "H |- p->false ==> H |- p->q";
-by (rtac deduction 1);
-by (etac (weaken_left_insert RS thms_notE) 1);
-by (rtac thms.H 1);
-by (rtac insertI1 1);
-qed "false_imp";
-
-val [premp,premq] = goal PropLog.thy
-    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
-by (rtac deduction 1);
-by (rtac (premq RS weaken_left_insert RS thms.MP) 1);
-by (rtac (thms.H RS thms.MP) 1);
-by (rtac insertI1 1);
-by (rtac (premp RS weaken_left_insert) 1);
-qed "imp_false";
-
-(*This formulation is required for strong induction hypotheses*)
-Goal "hyps p tt |- (if tt[[p]] then p else p->false)";
-by (rtac (split_if RS iffD2) 1);
-by (induct_tac "p" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
-by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
-			      weaken_right, imp_false]
-                       addSEs [false_imp]) 1);
-qed "hyps_thms_if";
-
-(*Key lemma for completeness; yields a set of assumptions satisfying p*)
-val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
-by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
-    rtac hyps_thms_if 2);
-by (Simp_tac 1);
-qed "sat_thms_p";
-
-(*For proving certain theorems in our new propositional logic*)
-
-AddSIs [deduction];
-AddIs [thms.H, thms.H RS thms.MP];
-
-(*The excluded middle in the form of an elimination rule*)
-Goal "H |- (p->q) -> ((p->false)->q) -> q";
-by (rtac (deduction RS deduction) 1);
-by (rtac (thms.DN RS thms.MP) 1);
-by (ALLGOALS (best_tac (claset() addSIs prems)));
-qed "thms_excluded_middle";
-
-(*Hard to prove directly because it requires cuts*)
-val prems = goal PropLog.thy
-    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q";
-by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1);
-by (REPEAT (resolve_tac (prems@[deduction]) 1));
-qed "thms_excluded_middle_rule";
-
-(*** Completeness -- lemmas for reducing the set of assumptions ***)
-
-(*For the case hyps(p,t)-insert(#v,Y) |- p;
-  we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-Goal "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
-by (induct_tac "p" 1);
-by (ALLGOALS Simp_tac);
-by (Fast_tac 1);
-qed "hyps_Diff";
-
-(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
-  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
-Goal "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
-by (induct_tac "p" 1);
-by (ALLGOALS Simp_tac);
-by (Fast_tac 1);
-qed "hyps_insert";
-
-(** Two lemmas for use with weaken_left **)
-
-goal Set.thy "B-C <= insert a (B-insert a C)";
-by (Fast_tac 1);
-qed "insert_Diff_same";
-
-goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
-by (Fast_tac 1);
-qed "insert_Diff_subset2";
-
-Goal "finite(hyps p t)";
-by (induct_tac "p" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "hyps_finite";
-
-Goal "hyps p t <= (UN v. {#v, #v->false})";
-by (induct_tac "p" 1);
-by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed "hyps_subset";
-
-val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
-
-(*Induction on the finite set of assumptions hyps(p,t0).
-  We may repeatedly subtract assumptions until none are left!*)
-val [sat] = goal PropLog.thy
-    "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
-by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1);
-by (simp_tac (simpset() addsimps [sat RS sat_thms_p]) 1);
-by Safe_tac;
-(*Case hyps(p,t)-insert(#v,Y) |- p *)
-by (rtac thms_excluded_middle_rule 1);
-by (rtac (insert_Diff_same RS weaken_left) 1);
-by (etac spec 1);
-by (rtac (insert_Diff_subset2 RS weaken_left) 1);
-by (rtac (hyps_Diff RS Diff_weaken_left) 1);
-by (etac spec 1);
-(*Case hyps(p,t)-insert(#v -> false,Y) |- p *)
-by (rtac thms_excluded_middle_rule 1);
-by (rtac (insert_Diff_same RS weaken_left) 2);
-by (etac spec 2);
-by (rtac (insert_Diff_subset2 RS weaken_left) 1);
-by (rtac (hyps_insert RS Diff_weaken_left) 1);
-by (etac spec 1);
-qed "completeness_0_lemma";
-
-(*The base case for completeness*)
-val [sat] = goal PropLog.thy "{} |= p ==> {} |- p";
-by (rtac (Diff_cancel RS subst) 1);
-by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
-qed "completeness_0";
-
-(*A semantic analogue of the Deduction Theorem*)
-Goalw [sat_def] "insert p H |= q ==> H |= p->q";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "sat_imp";
-
-Goal "finite H ==> !p. H |= p --> H |- p";
-by (etac finite_induct 1);
-by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0]));
-by (rtac (weaken_left_insert RS thms.MP) 1);
-by (fast_tac ((claset_of Fun.thy) addSIs [sat_imp]) 1);
-by (Fast_tac 1);
-qed "completeness_lemma";
-
-val completeness = completeness_lemma RS spec RS mp;
-
-Goal "finite H ==> (H |- p) = (H |= p)";
-by (fast_tac (claset() addSEs [soundness, completeness]) 1);
-qed "syntax_iff_semantics";
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/PropLog.thy	Tue Apr 02 14:28:28 2002 +0200
@@ -1,45 +1,276 @@
-(*  Title:      HOL/ex/PropLog.thy
+(*  Title:      HOL/Induct/PropLog.thy
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1994  TU Muenchen
-
-Inductive definition of propositional logic.
+    Copyright   1994  TU Muenchen & University of Cambridge
 *)
 
-PropLog = Main +
+header {* Meta-theory of propositional logic *}
+
+theory PropLog = Main:
+
+text {*
+  Datatype definition of propositional logic formulae and inductive
+  definition of the propositional tautologies.
+
+  Inductive definition of propositional logic.  Soundness and
+  completeness w.r.t.\ truth-tables.
+
+  Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
+  Fin(H)"}
+*}
+
+subsection {* The datatype of propositions *}
 
 datatype
-    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
+    'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)
+
+subsection {* The proof system *}
+
 consts
-  thms :: 'a pl set => 'a pl set
-  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
-  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
-  eval  :: ['a set, 'a pl] => bool      ("_[[_]]" [100,0] 100)
-  hyps  :: ['a pl, 'a set] => 'a pl set
+  thms  :: "'a pl set => 'a pl set"
+  "|-"  :: "['a pl set, 'a pl] => bool"   (infixl 50)
 
 translations
-  "H |- p" == "p : thms(H)"
+  "H |- p" == "p \<in> thms(H)"
 
 inductive "thms(H)"
-  intrs
-  H   "p:H ==> H |- p"
-  K   "H |- p->q->p"
-  S   "H |- (p->q->r) -> (p->q) -> p->r"
-  DN  "H |- ((p->false) -> false) -> p"
-  MP  "[| H |- p->q; H |- p |] ==> H |- q"
+  intros
+  H [intro]:  "p\<in>H ==> H |- p"
+  K:          "H |- p->q->p"
+  S:          "H |- (p->q->r) -> (p->q) -> p->r"
+  DN:         "H |- ((p->false) -> false) -> p"
+  MP:         "[| H |- p->q; H |- p |] ==> H |- q"
+
+subsection {* The semantics *}
+
+subsubsection {* Semantics of propositional logic. *}
 
-defs
-  sat_def  "H |= p  ==  (!tt. (!q:H. tt[[q]]) --> tt[[p]])"
+consts
+  eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)
+
+primrec     "tt[[false]] = False"
+	    "tt[[#v]]    = (v \<in> tt)"
+  eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
 
-primrec
-         "tt[[false]] = False"
-         "tt[[#v]]    = (v:tt)"
-eval_imp "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
+text {*
+  A finite set of hypotheses from @{text t} and the @{text Var}s in
+  @{text p}.
+*}
+
+consts
+  hyps  :: "['a pl, 'a set] => 'a pl set"
 
 primrec
   "hyps false  tt = {}"
-  "hyps (#v)   tt = {if v:tt then #v else #v->false}"
+  "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
   "hyps (p->q) tt = hyps p tt Un hyps q tt"
 
+subsubsection {* Logical consequence *}
+
+text {*
+  For every valuation, if all elements of @{text H} are true then so
+  is @{text p}.
+*}
+
+constdefs
+  sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50)
+    "H |= p  ==  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
+
+
+subsection {* Proof theory of propositional logic *}
+
+lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
+apply (unfold thms.defs )
+apply (rule lfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+lemma thms_I: "H |- p->p"
+  -- {*Called @{text I} for Identity Combinator, not for Introduction. *}
+by (best intro: thms.K thms.S thms.MP)
+
+
+subsubsection {* Weakening, left and right *}
+
+lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
+  -- {* Order of premises is convenient with @{text THEN} *}
+  by (erule thms_mono [THEN subsetD])
+
+lemmas weaken_left_insert = subset_insertI [THEN weaken_left]
+
+lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
+lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
+
+lemma weaken_right: "H |- q ==> H |- p->q"
+by (fast intro: thms.K thms.MP)
+
+
+subsubsection {* The deduction theorem *}
+
+theorem deduction: "insert p H |- q  ==>  H |- p->q"
+apply (erule thms.induct)
+apply (fast intro: thms_I thms.H thms.K thms.S thms.DN 
+                   thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
+done
+
+
+subsubsection {* The cut rule *}
+
+lemmas cut = deduction [THEN thms.MP]
+
+lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
+
+lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
+
+
+subsubsection {* Soundness of the rules wrt truth-table semantics *}
+
+theorem soundness: "H |- p ==> H |= p"
+apply (unfold sat_def)
+apply (erule thms.induct, auto) 
+done
+
+subsection {* Completeness *}
+
+subsubsection {* Towards the completeness proof *}
+
+lemma false_imp: "H |- p->false ==> H |- p->q"
+apply (rule deduction)
+apply (erule weaken_left_insert [THEN thms_notE])
+apply blast
+done
+
+lemma imp_false:
+    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
+apply (rule deduction)
+apply (blast intro: weaken_left_insert thms.MP thms.H) 
+done
+
+lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
+  -- {* Typical example of strengthening the induction statement. *}
+apply simp 
+apply (induct_tac "p")
+apply (simp_all add: thms_I thms.H)
+apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
+                    imp_false false_imp)
+done
+
+lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
+  -- {* Key lemma for completeness; yields a set of assumptions 
+        satisfying @{text p} *}
+apply (unfold sat_def) 
+apply (drule spec, erule mp [THEN if_P, THEN subst], 
+       rule_tac [2] hyps_thms_if, simp)
+done
+
+text {*
+  For proving certain theorems in our new propositional logic.
+*}
+
+declare deduction [intro!]
+declare thms.H [THEN thms.MP, intro]
+
+text {*
+  The excluded middle in the form of an elimination rule.
+*}
+
+lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
+apply (rule deduction [THEN deduction])
+apply (rule thms.DN [THEN thms.MP], best) 
+done
+
+lemma thms_excluded_middle_rule:
+    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q"
+  -- {* Hard to prove directly because it requires cuts *}
+by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) 
+
+
+subsection{* Completeness -- lemmas for reducing the set of assumptions*}
+
+text {*
+  For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
+  "hyps p t - {#v} \<subseteq> hyps p (t-{v})"}.
+*}
+
+lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
+by (induct_tac "p", auto) 
+
+text {*
+  For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
+  @{prop "hyps p t-{#v->Fls} \<subseteq> hyps p (insert v t)"}.
+*}
+
+lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
+by (induct_tac "p", auto)
+
+text {* Two lemmas for use with @{text weaken_left} *}
+
+lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
+by fast
+
+lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
+by fast
+
+text {*
+  The set @{term "hyps p t"} is finite, and elements have the form
+  @{term "#v"} or @{term "#v->Fls"}.
+*}
+
+lemma hyps_finite: "finite(hyps p t)"
+by (induct_tac "p", auto)
+
+lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
+by (induct_tac "p", auto)
+
+lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
+
+subsubsection {* Completeness theorem *}
+
+text {*
+  Induction on the finite set of assumptions @{term "hyps p t0"}.  We
+  may repeatedly subtract assumptions until none are left!
+*}
+
+lemma completeness_0_lemma:
+    "{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p" 
+apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
+ apply (simp add: sat_thms_p, safe)
+(*Case hyps p t-insert(#v,Y) |- p *)
+ apply (rule thms_excluded_middle_rule)
+  apply (rule insert_Diff_same [THEN weaken_left])
+  apply (erule spec)
+ apply (rule insert_Diff_subset2 [THEN weaken_left])
+ apply (rule hyps_Diff [THEN Diff_weaken_left])
+ apply (erule spec)
+(*Case hyps p t-insert(#v -> false,Y) |- p *)
+apply (rule thms_excluded_middle_rule)
+ apply (rule_tac [2] insert_Diff_same [THEN weaken_left])
+ apply (erule_tac [2] spec)
+apply (rule insert_Diff_subset2 [THEN weaken_left])
+apply (rule hyps_insert [THEN Diff_weaken_left])
+apply (erule spec)
+done
+
+text{*The base case for completeness*}
+lemma completeness_0:  "{} |= p ==> {} |- p"
+apply (rule Diff_cancel [THEN subst])
+apply (erule completeness_0_lemma [THEN spec])
+done
+
+text{*A semantic analogue of the Deduction Theorem*}
+lemma sat_imp: "insert p H |= q ==> H |= p->q"
+by (unfold sat_def, auto)
+
+theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
+apply (erule finite_induct)
+apply (safe intro!: completeness_0)
+apply (drule sat_imp)
+apply (drule spec) 
+apply (blast intro: weaken_left_insert [THEN thms.MP])  
+done
+
+theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
+by (fast elim!: soundness completeness)
+
 end
 
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/ROOT.ML	Tue Apr 02 14:28:28 2002 +0200
@@ -9,4 +9,3 @@
 time_use_thy "PropLog";
 time_use_thy "SList";
 time_use_thy "LFilter";
-time_use_thy "Exp";
diff -r 96bf406fd3e5 -r d3e1d554cd6d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 02 14:28:28 2002 +0200
@@ -220,10 +220,9 @@
 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
 
 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
-  Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
-  Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
-  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
-  Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
+  Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
+  Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
+  Induct/PropLog.thy Induct/ROOT.ML \
   Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   Induct/Tree.thy Induct/document/root.tex