# HG changeset patch
# User paulson
# Date 863005882 -7200
# Node ID 3f0ab2c306f75b84996c9796711185c6f1883437
# Parent  1c0dfa7ebb72adf58dbc174212efbfc9f67c98f6
Moved induction examples to directory Induct

diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/IsaMakefile	Wed May 07 13:51:22 1997 +0200
@@ -41,6 +41,17 @@
 
 #### Tests and examples
 
+## Inductive definitions: simple examples
+
+INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
+
+INDUCT_FILES = Induct/ROOT.ML \
+	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
+
+Induct:	$(OUT)/HOL $(INDUCT_FILES)
+	@$(ISATOOL) usedir $(OUT)/HOL Induct
+
+
 ## IMP-semantics example
 
 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
@@ -185,8 +196,7 @@
 
 ## Miscellaneous examples
 
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
-	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
+EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
@@ -198,7 +208,8 @@
 ## Full test
 
 test:	$(OUT)/HOL \
-	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
+		TFL Induct IMP Hoare Lex Integ Auth Subst Lambda  \
+		W0 MiniML IOA AxClasses Quot ex
 	echo 'Test examples ran successfully' > test
 
 
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/Makefile
--- a/src/HOL/Makefile	Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/Makefile	Wed May 07 13:51:22 1997 +0200
@@ -88,6 +88,21 @@
 	else echo 'exit_use_dir"../TFL";quit();' | $(LOGIC); \
 	fi
 
+
+## Inductive definitions: simple examples
+
+INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
+
+INDUCT_FILES = Induct/ROOT.ML \
+	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
+
+Induct:	$(BIN)/HOL $(INDUCT_FILES)
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	then echo 'make_html := true; exit_use_dir"Induct";quit();' | $(LOGIC); \
+	else echo 'exit_use_dir"Induct";quit();' | $(LOGIC); \
+	fi
+
+
 ##IMP-semantics example
 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
@@ -201,8 +216,7 @@
 	fi
 
 ##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
-	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
+EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
@@ -214,7 +228,9 @@
 	fi
 
 #Full test.
-test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML ex
+test:	$(BIN)/HOL \
+		TFL Induct IMP Hoare Lex Integ Auth Subst Lambda  \
+		W0 MiniML IOA AxClasses Quot ex
 	echo 'Test examples ran successfully' > test
 
 .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/README.html
--- a/src/HOL/README.html	Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/README.html	Wed May 07 13:51:22 1997 +0200
@@ -31,11 +31,14 @@
 <DT>IMP
 <DD>mechanization of a large part of a semantics text by Glynn Winskel
 
+<DT>Induct
+<DD>examples of (co)inductive definitions
+
 <DT>Integ
 <DD>a theory of the integers including efficient integer calculations
 
 <DT>IOA
-<DD>extended example of Input/Output Automata (takes a long time to run!)
+<DD>extended example of Input/Output Automata
 
 <DT>Lambda
 <DD>a proof of the Church-Rosser theorem for lambda-calculus
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Acc.ML
--- a/src/HOL/ex/Acc.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(*  Title:      HOL/ex/Acc
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Inductive definition of acc(r)
-
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
-*)
-
-open Acc;
-
-(*The intended introduction rule*)
-val prems = goal Acc.thy
-    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
-by (fast_tac (!claset addIs (prems @ 
-                            map (rewrite_rule [pred_def]) acc.intrs)) 1);
-qed "accI";
-
-goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
-by (etac acc.elim 1);
-by (rewtac pred_def);
-by (Fast_tac 1);
-qed "acc_downward";
-
-val [major,indhyp] = goal Acc.thy
-    "[| a : acc(r);                                             \
-\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
-\    |] ==> P(a)";
-by (rtac (major RS acc.induct) 1);
-by (rtac indhyp 1);
-by (resolve_tac acc.intrs 1);
-by (rewtac pred_def);
-by (Fast_tac 2);
-by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
-qed "acc_induct";
-
-
-val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
-by (rtac (major RS wfI) 1);
-by (etac acc.induct 1);
-by (rewtac pred_def);
-by (Fast_tac 1);
-qed "acc_wfI";
-
-val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
-by (rtac (major RS wf_induct) 1);
-by (rtac (impI RS allI) 1);
-by (rtac accI 1);
-by (Fast_tac 1);
-qed "acc_wfD_lemma";
-
-val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
-by (rtac subsetI 1);
-by (res_inst_tac [("p", "x")] PairE 1);
-by (fast_tac (!claset addSIs [SigmaI,
-                             major RS acc_wfD_lemma RS spec RS mp]) 1);
-qed "acc_wfD";
-
-goal Acc.thy "wf(r)  =  (r <= (acc r) Times (acc r))";
-by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
-qed "wf_acc_iff";
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Acc.thy
--- a/src/HOL/ex/Acc.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      HOL/ex/Acc.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Inductive definition of acc(r)
-
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
-*)
-
-Acc = WF + 
-
-constdefs
-  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
-  "pred x r == {y. (y,x):r}"
-
-consts
-  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
-
-inductive "acc(r)"
-  intrs
-    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
-  monos     "[Pow_mono]"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Comb.ML
--- a/src/HOL/ex/Comb.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +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
-*)
-
-open Comb;
-
-(*** 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 Comb.thy [diamond_def]
-    "!!r. [| 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);
-val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
-
-val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
-by (rewtac diamond_def);  (*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 (slow_best_tac  (*Seems to be a brittle, undirected search*)
-    (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
-            addEs [major RS diamond_strip_lemmaE]) 1);
-qed "diamond_rtrancl";
-
-
-(*** Results about Contraction ***)
-
-(*Derive a case for each combinator constructor*)
-val K_contractE = contract.mk_cases comb.simps "K -1-> z";
-val S_contractE = contract.mk_cases comb.simps "S -1-> z";
-val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
-
-AddSIs [contract.K, contract.S];
-AddIs  [contract.Ap1, contract.Ap2];
-AddSEs [K_contractE, S_contractE, Ap_contractE];
-Unsafe_Addss  (!simpset);
-
-goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
-by (Blast_tac 1);
-qed "I_contract_E";
-AddSEs [I_contract_E];
-
-goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
-by (Blast_tac 1);
-qed "K1_contractD";
-AddSEs [K1_contractD];
-
-goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
-qed "Ap_reduce1";
-
-goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
-qed "Ap_reduce2";
-
-(** Counterexample to the diamond property for -1-> **)
-
-goal Comb.thy "K#I#(I#I) -1-> I";
-by (rtac contract.K 1);
-qed "KIII_contract1";
-
-goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
-by (Blast_tac 1);
-qed "KIII_contract2";
-
-goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
-by (Blast_tac 1);
-qed "KIII_contract3";
-
-goalw Comb.thy [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 comb.simps "K =1=> z";
-val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
-val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
-
-AddIs  parcontract.intrs;
-AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Unsafe_Addss  (!simpset);
-
-(*** Basic properties of parallel contraction ***)
-
-goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
-by (Blast_tac 1);
-qed "K1_parcontractD";
-AddSDs [K1_parcontractD];
-
-goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
-by (Blast_tac 1);
-qed "S1_parcontractD";
-AddSDs [S1_parcontractD];
-
-goal Comb.thy
- "!!x y z. 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 Comb.thy [diamond_def] "diamond parcontract";
-by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract.induct 1 THEN prune_params_tac);
-by (Step_tac 1);
-by (ALLGOALS Blast_tac);
-qed "diamond_parcontract";
-
-
-(*** Equivalence of x--->y and x===>y ***)
-
-goal Comb.thy "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 Comb.thy [I_def] "I#x ---> x";
-by (Blast_tac 1);
-qed "reduce_I";
-
-goal Comb.thy "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 Comb.thy "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 Comb.thy "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 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Comb.thy
--- a/src/HOL/ex/Comb.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-(*  Title:      HOL/ex/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.
-*)
-
-
-Comb = Trancl +
-
-(** Datatype definition of combinators S and K, with infixed application **)
-datatype comb = K
-              | S
-              | "#" comb comb (infixl 90)
-
-(** Inductive definition of contractions, -1->
-             and (multi-step) reductions, --->
-**)
-consts
-  contract  :: "(comb*comb) set"
-  "-1->"    :: [comb,comb] => bool   (infixl 50)
-  "--->"    :: [comb,comb] => bool   (infixl 50)
-
-translations
-  "x -1-> y" == "(x,y) : contract"
-  "x ---> y" == "(x,y) : 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"
-
-
-(** 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)
-
-translations
-  "x =1=> y" == "(x,y) : parcontract"
-  "x ===> y" == "(x,y) : 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"
-
-
-(*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))"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/LFilter.ML
--- a/src/HOL/ex/LFilter.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,341 +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
-*)
-
-open LFilter;
-
-
-(*** findRel: basic laws ****)
-
-val findRel_LConsE = 
-    findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
-
-AddSEs [findRel_LConsE];
-
-
-goal thy "!!p. (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 thy "!!p. (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 thy "!!p. (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 thy "!!p. 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 thy "[| l: Domain (findRel p);                                   \
-\            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
-\         |] ==> Q";
-by (rtac (major RS DomainE) 1);
-by (forward_tac [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 (Step_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 thy [find_def] "find p LNil = LNil";
-by (blast_tac (!claset addIs [select_equality]) 1);
-qed "find_LNil";
-
-goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
-by (blast_tac (!claset addIs [select_equality] addDs [findRel_functional]) 1);
-qed "findRel_imp_find";
-
-goal thy "!!p. 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";
-
-goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
-by (blast_tac (!claset addIs [select_equality]) 1);
-qed "diverge_find_LNil";
-
-Addsimps [diverge_find_LNil];
-
-goal thy "!!p. ~ (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 (Step_tac 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
-by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
-qed "find_LCons_seek";
-
-goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
-                           setloop split_tac[expand_if]) 1);
-qed "find_LCons";
-
-
-
-(*** lfilter: basic equations ***)
-
-goal thy "lfilter p LNil = LNil";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (simp_tac (!simpset addsimps [find_LNil]) 1);
-qed "lfilter_LNil";
-
-goal thy "!!p. 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";
-
-
-goal thy "!!p. 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 (!simpset addsimps [find_LCons_found]) 1);
-qed "lfilter_LCons_found";
-
-
-goal thy "!!p. (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 (!simpset addsimps [findRel_imp_find]) 1);
-qed "findRel_imp_lfilter";
-
-goal thy "!!p. ~ (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 (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (etac Domain_findRelE 1);
-by (safe_tac (!claset delrules [conjI]));
-by (asm_full_simp_tac 
-    (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
-                        find_LCons_seek]) 1);
-qed "lfilter_LCons_seek";
-
-
-goal thy "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]
-                           setloop split_tac[expand_if]) 1);
-qed "lfilter_LCons";
-
-AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-Addsimps [lfilter_LNil, lfilter_LCons];
-
-
-goal thy "!!p. 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 (!simpset addsimps [findRel_imp_lfilter]) 1);
-qed "lfilter_eq_LNil";
-
-
-goal thy "!!p. 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 (!simpset addsimps [findRel_imp_find]) 1);
-by (Blast_tac 1);
-qed_spec_mp "lfilter_eq_LCons";
-
-
-goal thy "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 (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (blast_tac (!claset addSEs [Domain_findRelE] 
-                       addIs [findRel_imp_lfilter]) 1);
-qed "lfilter_cases";
-
-
-(*** lfilter: simple facts by coinduction ***)
-
-goal thy "lfilter (%x.True) l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed "lfilter_K_True";
-
-goal thy "lfilter p (lfilter p l) = lfilter p l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
-(*Cases: p x is true or false*)
-by (Blast_tac 1);
-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 thy "!!p. (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 thy "!!p. (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 thy "!!p. (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 thy "!!p. (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 thy "!!p. (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 (!simpset setloop split_tac[expand_if])));
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
-qed_spec_mp "findRel_conj_lfilter";
-
-
-
-goal thy "(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 (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (etac Domain_findRelE 1);
-(*case q x*)
-by (case_tac "p x" 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
-                                     findRel_conj RS findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
-(*case q x and ~(p x) *)
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 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 (!simpset addsimps [diverge_lfilter_LNil]) 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 (!simpset addsimps [findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
-val lemma = result();
-
-
-goal thy "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 (!simpset setloop split_tac[expand_if])));
-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 thy "!!p. (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 thy "!!p. 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 thy "!!p. (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 thy "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 (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
-by (Blast_tac 1);
-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 (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (etac Domain_findRelE 1);
-by (forward_tac [lmap_LCons_findRel] 1);
-by (Step_tac 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
-qed "lfilter_lmap";
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/LFilter.thy
--- a/src/HOL/ex/LFilter.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      HOL/LList.thy
-    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 + Relation +
-
-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"
-
-constdefs
-  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 p l == llist_corec l (%l. case find p l of
-                                            LNil => Inl ()
-                                          | LCons y z => Inr(y,z))"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,886 +0,0 @@
-(*  Title:      HOL/ex/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)?
-*)
-
-open LList;
-
-(** Simplification **)
-
-simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
-
-(*For adding _eqI rules to a simpset; we must remove Pair_eq because
-  it may turn an instance of reflexivity into a conjunction!*)
-fun add_eqI ss = ss addsimps [range_eqI, image_eqI] 
-                    delsimps [Pair_eq];
-
-
-(*This justifies using llist in other recursive type definitions*)
-goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
-by (rtac gfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "llist_mono";
-
-
-goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
-let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (!claset addSIs (equalityI :: 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 LList.thy [list_Fun_def]
-    "!!M. [| 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 LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
-by (Fast_tac 1);
-qed "list_Fun_NIL_I";
-
-goalw LList.thy [list_Fun_def,CONS_def]
-    "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
-by (Fast_tac 1);
-qed "list_Fun_CONS_I";
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-goalw LList.thy (llist.defs @ [list_Fun_def])
-    "!!M N. 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 LList.thy [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";
-
-(*UNUSED; obsolete?
-goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))";
-by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
-qed "split_UN1";
-
-goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))";
-by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
-qed "sum_case2_UN1";
-*)
-
-val prems = goalw LList.thy [CONS_def]
-    "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
-by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 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.thy [LList_corec_def]
-    "LList_corec a f <= sum_case (%u.NIL) \
-\                          (split(%z w. CONS z (LList_corec w f))) (f a)";
-by (rtac UN1_least 1);
-by (res_inst_tac [("n","k")] natE 1);
-by (ALLGOALS (Asm_simp_tac));
-by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
-qed "LList_corec_subset1";
-
-goalw LList.thy [LList_corec_def]
-    "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
-\    LList_corec a f";
-by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
-by (safe_tac (!claset));
-by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
-qed "LList_corec_subset2";
-
-(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
-goal LList.thy
-    "LList_corec a f = sum_case (%u. NIL) \
-\                           (split(%z w. CONS z (LList_corec w f))) (f a)";
-by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
-                         LList_corec_subset2] 1));
-qed "LList_corec";
-
-(*definitional version of same*)
-val [rew] = goal LList.thy
-    "[| !!x. h(x) == LList_corec x f |] ==>     \
-\    h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)";
-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.thy "LList_corec a f : llist({u.True})";
-by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by (safe_tac (!claset));
-by (stac LList_corec 1);
-by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
-                       |> add_eqI) 1);
-qed "LList_corec_type";
-
-(*Lemma for the proof of llist_corec*)
-goal LList.thy
-   "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
-\   llist(range Leaf)";
-by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by (safe_tac (!claset));
-by (stac LList_corec 1);
-by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
-by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
-qed "LList_corec_type2";
-
-
-(**** llist equality as a gfp; the bisimulation principle ****)
-
-(*This theorem is actually used, unlike the many similar ones in ZF*)
-goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
-let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
-                      addEs [rew LListD.elim]) 1)
-end;
-qed "LListD_unfold";
-
-goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
-by (res_inst_tac [("n", "k")] less_induct 1);
-by (safe_tac ((claset_of "Fun") delrules [equalityI]));
-by (etac LListD.elim 1);
-by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
-by (res_inst_tac [("n", "n")] natE 1);
-by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
-by (rename_tac "n'" 1);
-by (res_inst_tac [("n", "n'")] natE 1);
-by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
-by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
-qed "LListD_implies_ntrunc_equality";
-
-(*The domain of the LListD relation*)
-goalw LList.thy (llist.defs @ [NIL_def, CONS_def])
-    "fst``LListD(diag(A)) <= llist(A)";
-by (rtac gfp_upperbound 1);
-(*avoids unfolding LListD on the rhs*)
-by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "fst_image_LListD";
-
-(*This inclusion justifies the use of coinduction to show M=N*)
-goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
-by (rtac subsetI 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by (safe_tac (!claset));
-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 (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
-qed "LListD_subset_diag";
-
-
-(** Coinduction, using LListD_Fun
-    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
- **)
-
-goalw thy [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
-by (REPEAT (ares_tac basic_monos 1));
-qed "LListD_Fun_mono";
-
-goalw LList.thy [LListD_Fun_def]
-    "!!M. [| 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 LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
-by (Fast_tac 1);
-qed "LListD_Fun_NIL_I";
-
-goalw LList.thy [LListD_Fun_def,CONS_def]
- "!!x. [| 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 LList.thy (LListD.defs @ [LListD_Fun_def])
-    "!!M N. 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 LList.thy "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 LList.thy "LListD(diag(A)) = diag(llist(A))";
-by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
-                         diag_subset_LListD] 1));
-qed "LListD_eq_diag";
-
-goal LList.thy 
-    "!!M N. 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 LList.thy 
-    "!!r. [| (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 (!claset));
-qed "LList_equalityI";
-
-
-(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
-
-(*abstract proof using a bisimulation*)
-val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
-\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
-\ ==> h1=h2";
-by (rtac ext 1);
-(*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "{u.True}"),
-                  ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
-by (rtac rangeI 1);
-by (safe_tac (!claset));
-by (stac prem1 1);
-by (stac prem2 1);
-by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
-                                 CollectI RS LListD_Fun_CONS_I]
-                       |> add_eqI) 1);
-qed "LList_corec_unique";
-
-val [prem] = goal LList.thy
- "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \
-\ ==> 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 LList.thy [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
-by (rtac ntrunc_one_In1 1);
-qed "ntrunc_one_CONS";
-
-goalw LList.thy [CONS_def]
-    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
-by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_In1]) 1);
-qed "ntrunc_CONS";
-
-val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
-\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
-\ ==> h1=h2";
-by (rtac (ntrunc_equality RS ext) 1);
-by (rename_tac "x k" 1);
-by (res_inst_tac [("x", "x")] spec 1);
-by (res_inst_tac [("n", "k")] less_induct 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 (!simpset setloop (split_tac [expand_sum_case])) 1);
-by (strip_tac 1);
-by (res_inst_tac [("n", "n")] natE 1);
-by (rename_tac "m" 2);
-by (res_inst_tac [("n", "m")] natE 2);
-by (ALLGOALS(asm_simp_tac(!simpset addsimps
-            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
-result();
-
-
-(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
-
-goal LList.thy "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_Tarski)));
-
-(*A typical use of co-induction to show membership in the gfp.
-  The containing set is simply the singleton {Lconst(M)}. *)
-goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
-by (rtac (singletonI RS llist_coinduct) 1);
-by (safe_tac (!claset));
-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 LList.thy "Lconst(M) = LList_corec M (%x.Inr((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 LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
-by (rtac (equals_LList_corec RS fun_cong) 1);
-by (Simp_tac 1);
-by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
-qed "gfp_Lconst_eq_LList_corec";
-
-
-(*** Isomorphisms ***)
-
-goal LList.thy "inj(Rep_llist)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_llist_inverse 1);
-qed "inj_Rep_llist";
-
-goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
-by (rtac inj_onto_inverseI 1);
-by (etac Abs_llist_inverse 1);
-qed "inj_onto_Abs_llist";
-
-(** Distinctness of constructors **)
-
-goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil";
-by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 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 LList.thy [LNil_def]
-    "Rep_llist(LNil) = NIL";
-by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
-qed "Rep_llist_LNil";
-
-goalw LList.thy [LCons_def]
-    "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
-by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
-                         rangeI, Rep_llist] 1));
-qed "Rep_llist_LCons";
-
-(** Injectiveness of CONS and LCons **)
-
-goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
-by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_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]@llist.intrs);
-AddSDs [inj_onto_Abs_llist RS inj_ontoD,
-        inj_Rep_llist RS injD, Leaf_inject];
-
-goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
-qed "LCons_LCons_eq";
-
-AddIffs [LCons_LCons_eq];
-
-val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
-by (rtac (major RS 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 LList.thy
- "[| 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 subsetI 1);
-by (etac imageE 1);
-by (etac ssubst 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 LList.thy "Lmap f NIL = NIL";
-by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lmap_NIL";
-
-goal LList.thy "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";
-
-(*Another type-checking proof by coinduction*)
-val [major,minor] = goal LList.thy
-    "[| 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 (!claset));
-by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
-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*)
-val [major] = goal LList.thy  "M: llist(A) ==> Lmap f M: llist(f``A)";
-by (rtac (major RS Lmap_type) 1);
-by (etac imageI 1);
-qed "Lmap_type2";
-
-(** Two easy results about Lmap **)
-
-val [prem] = goalw LList.thy [o_def]
-    "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (safe_tac (!claset));
-by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
-by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
-                      rangeI RS LListD_Fun_CONS_I] 1));
-qed "Lmap_compose";
-
-val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (safe_tac (!claset));
-by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
-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 LList.thy [Lappend_def] "Lappend NIL NIL = NIL";
-by (rtac (LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lappend_NIL_NIL";
-
-goalw LList.thy [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 LList.thy [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];
-Delsimps [Pair_eq];
-
-goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Lappend_NIL";
-
-goal LList.thy "!!M. M: llist(A) ==> Lappend M NIL = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Lappend_NIL2";
-
-(** Alternative type-checking proofs for Lappend **)
-
-(*weak co-induction: bisimulation and case analysis on both variables*)
-goal LList.thy
-    "!!M N. [| 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 (!claset));
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (eres_inst_tac [("a", "v")] llist.elim 1);
-by (ALLGOALS
-    (Asm_simp_tac THEN'
-     fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
-qed "Lappend_type";
-
-(*strong co-induction: bisimulation and case analysis on one variable*)
-goal LList.thy
-    "!!M N. [| 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 subsetI 1);
-by (etac imageE 1);
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
-by (Asm_simp_tac 1);
-by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
-qed "Lappend_type";
-
-(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
-
-(** llist_case: case analysis for 'a llist **)
-
-Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
-           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
-
-goalw LList.thy [llist_case_def,LNil_def]  "llist_case c d LNil = c";
-by (Simp_tac 1);
-qed "llist_case_LNil";
-
-goalw LList.thy [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 LList.thy [NIL_def,CONS_def]
-    "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P \
-\    |] ==> P";
-by (rtac (Rep_llist RS llist.elim) 1);
-by (rtac (inj_Rep_llist RS injD RS prem1) 1);
-by (stac Rep_llist_LNil 1);
-by (assume_tac 1);
-by (etac rangeE 1);
-by (rtac (inj_Rep_llist RS injD RS prem2) 1);
-by (asm_simp_tac (!simpset delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
-by (etac (Abs_llist_inverse RS ssubst) 1);
-by (rtac refl 1);
-qed "llistE";
-
-(** llist_corec: corecursion for 'a llist **)
-
-goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
-    "llist_corec a f = sum_case (%u. LNil) \
-\                           (split(%z w. LCons z (llist_corec w f))) (f a)";
-by (stac LList_corec 1);
-by (res_inst_tac [("s","f(a)")] sumE 1);
-by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
-by (res_inst_tac [("p","y")] PairE 1);
-by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
-(*FIXME: correct case splits usd to be found automatically:
-by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 1);*)
-qed "llist_corec";
-
-(*definitional version of same*)
-val [rew] = goal LList.thy
-    "[| !!x. h(x) == llist_corec x f |] ==>     \
-\    h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)";
-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 LList.thy [LListD_Fun_def]
-    "!!r A. r <= (llist A) Times (llist A) ==> \
-\           LListD_Fun (diag A) r <= (llist A) Times (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_Sigma_llist";
-
-goal LList.thy
-    "prod_fun Rep_llist Rep_llist `` r <= \
-\    (llist(range Leaf)) Times (llist(range Leaf))";
-by (fast_tac (!claset addIs [Rep_llist]) 1);
-qed "subset_Sigma_llist";
-
-val [prem] = goal LList.thy
-    "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
-\    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
-by (safe_tac (!claset));
-by (rtac (prem RS subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
-qed "prod_fun_lemma";
-
-goal LList.thy
-    "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
-\    diag(llist(range Leaf))";
-by (rtac equalityI 1);
-by (fast_tac (!claset addIs [Rep_llist]) 1);
-by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
-qed "prod_fun_range_eq_diag";
-
-(*Surprisingly hard to prove.  Used with lfilter*)
-goalw thy [llistD_Fun_def, prod_fun_def]
-    "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
-by (Auto_tac());
-by (rtac image_eqI 1);
-by (fast_tac (!claset addss (!simpset)) 1);
-by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
-qed "llistD_Fun_mono";
-
-(** To show two llists are equal, exhibit a bisimulation! 
-      [also admits true equality] **)
-val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
-    "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
-by (rtac (inj_Rep_llist RS injD) 1);
-by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
-                  ("A", "range(Leaf)")] 
-        LList_equalityI 1);
-by (rtac (prem1 RS prod_fun_imageI) 1);
-by (rtac (prem2 RS 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_Sigma_llist RS prod_fun_lemma) 1);
-by (rtac (subset_Sigma_llist RS Un_least) 1);
-by (rtac diag_subset_Sigma 1);
-qed "llist_equalityI";
-
-(** Rules to prove the 2nd premise of llist_equalityI **)
-goalw LList.thy [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";
-
-val [prem] = goalw LList.thy [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 (rtac (prem RS prod_fun_imageI) 1);
-qed "llistD_Fun_LCons_I";
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-goalw LList.thy [llistD_Fun_def]
-     "!!l. (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_Fun_diag_I) 1);
-qed "llistD_Fun_range_I";
-
-(*A special case of list_equality for functions over lazy lists*)
-val [prem1,prem2] = goal LList.thy
-    "[| 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 LList.thy "lmap f LNil = LNil";
-by (rtac (lmap_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lmap_LNil";
-
-goal LList.thy "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 LList.thy "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 LList.thy "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 LList.thy "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 LList.thy "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 (!claset));
-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 LList.thy "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 LList.thy
-    "nat_rec (LCons b l) (%m. lmap(f)) n =      \
-\    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
-by (nat_ind_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 (nat_ind_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "fun_power_Suc";
-
-val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
- [("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 LList.thy
-    "(!!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 (safe_tac (!claset));
-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 LList.thy [lappend_def] "lappend LNil LNil = LNil";
-by (rtac (llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lappend_LNil_LNil";
-
-goalw LList.thy [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 LList.thy [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 LList.thy "lappend LNil l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lappend_LNil";
-
-goal LList.thy "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 LList.thy "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 (!claset));
-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 LList.thy "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 (!claset));
-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 LList.thy "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 LList.thy "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 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-(*  Title:      HOL/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
-bounds on the amount of lookahead required.
-
-Could try (but would it work for the gfp analogue of term?)
-  LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
-
-A nice but complex example would be [ML for the Working Programmer, page 176]
-  from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
-
-Previous definition of llistD_Fun was explicit:
-  llistD_Fun_def
-   "llistD_Fun(r) ==    
-       {(LNil,LNil)}  Un        
-       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
-*)
-
-LList = Gfp + SList +
-
-types
-  'a llist
-
-arities
-   llist :: (term)term
-
-consts
-  list_Fun   :: ['a item set, 'a item set] => 'a item set
-  LListD_Fun :: 
-      "[('a item * 'a item)set, ('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"
-  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
-
-  Rep_llist  :: 'a llist => 'a item
-  Abs_llist  :: 'a item => 'a llist
-  LNil       :: 'a llist
-  LCons      :: ['a, 'a llist] => 'a llist
-  
-  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
-
-  LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
-  LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
-  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
-
-  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
-  lmap       :: ('a=>'b) => ('a llist => 'b llist)
-
-  iterates   :: ['a => 'a, 'a] => 'a llist
-
-  Lconst     :: 'a item => 'a item
-  Lappend    :: ['a item, 'a item] => 'a item
-  lappend    :: ['a llist, 'a llist] => 'a llist
-
-
-coinductive "llist(A)"
-  intrs
-    NIL_I  "NIL: llist(A)"
-    CONS_I "[| a: A;  M: llist(A) |] ==> CONS a M : 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)"
-
-translations
-  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
-
-
-defs
-  (*Now used exclusively for abbreviating the coinduction rule*)
-  list_Fun_def   "list_Fun A X ==   
-                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
-
-  LListD_Fun_def "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)}"
-
-  (*defining the abstract constructors*)
-  LNil_def      "LNil == Abs_llist(NIL)"
-  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
-
-  llist_case_def
-   "llist_case c d l == 
-       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
-
-  LList_corec_fun_def
-    "LList_corec_fun k f == 
-     nat_rec (%x. {})                         
-             (%j r x. case f x of Inl u    => NIL
-                                | Inr(z,w) => CONS z (r w)) 
-             k"
-
-  LList_corec_def
-    "LList_corec a f == UN k. LList_corec_fun k f a"
-
-  llist_corec_def
-   "llist_corec a f == 
-       Abs_llist(LList_corec a 
-                 (%z.case f z of Inl x    => Inl(x)
-                               | Inr(v,w) => Inr(Leaf(v), w)))"
-
-  llistD_Fun_def
-   "llistD_Fun(r) ==    
-        prod_fun Abs_llist Abs_llist ``         
-                LListD_Fun (diag(range Leaf))   
-                            (prod_fun Rep_llist Rep_llist `` r)"
-
-  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
-
-  Lmap_def
-   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
-
-  lmap_def
-   "lmap f l == llist_corec l (%z. case z of LNil => (Inl ()) 
-                                           | LCons y z => Inr(f(y), z))"
-
-  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
-
-(*Append generates its result by applying f, where
-    f((NIL,NIL))          = Inl(())
-    f((NIL, CONS N1 N2))  = Inr((N1, (NIL,N2))
-    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
-*)
-
-  Lappend_def
-   "Lappend M N == LList_corec (M,N)                                         
-     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
-                      (%M1 M2 N. Inr((M1, (M2,N))))))"
-
-  lappend_def
-   "lappend l n == llist_corec (l,n)                                         
-   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
-                     (%l1 l2 n. Inr((l1, (l2,n))))))"
-
-rules
-    (*faking a type definition...*)
-  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
-  Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
-  Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Mutil.ML
--- a/src/HOL/ex/Mutil.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(*  Title:      HOL/ex/Mutil
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-*)
-
-open Mutil;
-
-Addsimps tiling.intrs;
-
-(** The union of two disjoint tilings is a tiling **)
-
-goal thy "!!t. t: tiling A ==> \
-\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
-by (etac tiling.induct 1);
-by (Simp_tac 1);
-by (simp_tac (!simpset addsimps [Un_assoc]) 1);
-by (blast_tac (!claset addIs tiling.intrs) 1);
-qed_spec_mp "tiling_UnI";
-
-
-(*** Chess boards ***)
-
-val [below_0, below_Suc] = nat_recs below_def;
-Addsimps [below_0, below_Suc];
-
-goal thy "ALL i. (i: below k) = (i<k)";
-by (nat_ind_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
-by (Blast_tac 1);
-qed_spec_mp "below_less_iff";
-
-Addsimps [below_less_iff];
-
-goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "Sigma_Suc1";
-
-goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "Sigma_Suc2";
-
-(*Deletion is essential to allow use of Sigma_Suc1,2*)
-Delsimps [below_Suc];
-
-goal thy "{i} Times below(n + n) : tiling domino";
-by (nat_ind_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
-by (resolve_tac tiling.intrs 1);
-by (assume_tac 2);
-by (subgoal_tac    (*seems the easiest way of turning one to the other*)
-    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
-\    {(i, n+n), (i, Suc(n+n))}" 1);
-by (Blast_tac 2);
-by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (blast_tac (!claset addEs  [less_irrefl, less_asym]
-                       addSDs [below_less_iff RS iffD1]) 1);
-qed "dominoes_tile_row";
-
-goal thy "(below m) Times below(n + n) : tiling domino";
-by (nat_ind_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
-by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
-                      addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
-qed "dominoes_tile_matrix";
-
-
-(*** Basic properties of evnodd ***)
-
-goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A  &  (i+j) mod 2 = b)";
-by (Simp_tac 1);
-qed "evnodd_iff";
-
-goalw thy [evnodd_def] "evnodd A b <= A";
-by (rtac Int_lower1 1);
-qed "evnodd_subset";
-
-(* finite X ==> finite(evnodd X b) *)
-bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
-
-goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (Blast_tac 1);
-qed "evnodd_Un";
-
-goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (Blast_tac 1);
-qed "evnodd_Diff";
-
-goalw thy [evnodd_def] "evnodd {} b = {}";
-by (Simp_tac 1);
-qed "evnodd_empty";
-
-goalw thy [evnodd_def]
-    "evnodd (insert (i,j) C) b = \
-\    (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
-by (asm_full_simp_tac (!simpset addsimps [evnodd_def] 
-             setloop (split_tac [expand_if] THEN' Step_tac)) 1);
-qed "evnodd_insert";
-
-
-(*** Dominoes ***)
-
-goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
-by (eresolve_tac [domino.elim] 1);
-by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
-by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
-by (REPEAT_FIRST assume_tac);
-(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_full_simp_tac (!simpset addsimps
-                          [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
-                          setloop split_tac [expand_if]) 1
-           THEN Blast_tac 1));
-qed "domino_singleton";
-
-goal thy "!!d. d:domino ==> finite d";
-by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
-                      addSEs [domino.elim]) 1);
-qed "domino_finite";
-
-
-(*** Tilings of dominoes ***)
-
-goal thy "!!t. t:tiling domino ==> finite t";
-by (eresolve_tac [tiling.induct] 1);
-by (rtac finite_emptyI 1);
-by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
-qed "tiling_domino_finite";
-
-goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
-by (eresolve_tac [tiling.induct] 1);
-by (simp_tac (!simpset addsimps [evnodd_def]) 1);
-by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
-by (Simp_tac 2 THEN assume_tac 1);
-by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
-by (Simp_tac 2 THEN assume_tac 1);
-by (Step_tac 1);
-by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
-by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
-                                     tiling_domino_finite,
-                                     evnodd_subset RS finite_subset,
-                                     card_insert_disjoint]) 1);
-by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
-qed "tiling_domino_0_1";
-
-goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
-\                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
-\                |] ==> t' ~: tiling domino";
-by (rtac notI 1);
-by (dtac tiling_domino_0_1 1);
-by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "t : tiling domino" 1);
-(*Requires a small simpset that won't move the Suc applications*)
-by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
-by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
-by (asm_simp_tac (!simpset addsimps add_ac) 2);
-by (asm_full_simp_tac 
-    (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty, 
-                        mod_less, tiling_domino_0_1 RS sym]) 1);
-by (rtac less_trans 1);
-by (REPEAT
-    (rtac card_Diff 1 
-     THEN
-     asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 
-     THEN
-     asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
-qed "mutil_not_tiling";
-
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Mutil.thy
--- a/src/HOL/ex/Mutil.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      HOL/ex/Mutil
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-  Originator is Max Black, according to J A Robinson.
-  Popularized as the Mutilated Checkerboard Problem by J McCarthy
-*)
-
-Mutil = Finite +
-consts
-  domino  :: "(nat*nat)set set"
-  tiling  :: 'a set set => 'a set set
-  below   :: nat => nat set
-  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
-
-inductive domino
-  intrs
-    horiz  "{(i, j), (i, Suc j)} : domino"
-    vertl  "{(i, j), (Suc i, j)} : domino"
-
-inductive "tiling A"
-  intrs
-    empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
-
-defs
-  below_def  "below n    == nat_rec {} insert n"
-  evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Perm.ML
--- a/src/HOL/ex/Perm.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(*  Title:      HOL/ex/Perm.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-
-Permutations: example of an inductive definition
-*)
-
-(*It would be nice to prove
-    xs <~~> ys = (!x. count xs x = count ys x)
-See mset on HOL/ex/Sorting.thy
-*)
-
-open Perm;
-
-goal Perm.thy "l <~~> l";
-by (list.induct_tac "l" 1);
-by (REPEAT (ares_tac perm.intrs 1));
-qed "perm_refl";
-
-
-(** Some examples of rule induction on permutations **)
-
-(*The form of the premise lets the induction bind xs and ys.*)
-goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
-by (etac perm.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "perm_Nil_lemma";
-
-(*A more general version is actually easier to understand!*)
-goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
-by (etac perm.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "perm_length";
-
-goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
-by (etac perm.induct 1);
-by (REPEAT (ares_tac perm.intrs 1));
-qed "perm_sym";
-
-goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
-by (etac perm.induct 1);
-by (Fast_tac 4);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
-val perm_mem_lemma = result();
-
-bind_thm ("perm_mem", perm_mem_lemma RS mp);
-
-(** Ways of making new permutations **)
-
-(*We can insert the head anywhere in the list*)
-goal Perm.thy "a # xs @ ys <~~> xs @ a # ys";
-by (list.induct_tac "xs" 1);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-by (Simp_tac 1);
-by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
-qed "perm_append_Cons";
-
-(*single steps
-by (rtac perm.trans 1);
-by (rtac perm.swap 1);
-by (rtac perm.Cons 1);
-*)
-
-goal Perm.thy "xs@ys <~~> ys@xs";
-by (list.induct_tac "xs" 1);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-by (Simp_tac 1);
-by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
-qed "perm_append_swap";
-
-
-goal Perm.thy "a # xs <~~> xs @ [a]";
-by (rtac perm.trans 1);
-by (rtac perm_append_swap 2);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-qed "perm_append_single";
-
-goal Perm.thy "rev xs <~~> xs";
-by (list.induct_tac "xs" 1);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-by (Simp_tac 1);
-by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
-by (etac perm.Cons 1);
-qed "perm_rev";
-
-goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
-by (list.induct_tac "l" 1);
-by (Simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1);
-qed "perm_append1";
-
-goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
-by (rtac (perm_append_swap RS perm.trans) 1);
-by (etac (perm_append1 RS perm.trans) 1);
-by (rtac perm_append_swap 1);
-qed "perm_append2";
-
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Perm.thy
--- a/src/HOL/ex/Perm.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      HOL/ex/Perm.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-
-Permutations: example of an inductive definition
-*)
-
-Perm = List +
-
-consts  perm    :: "('a list * 'a list) set"   
-syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
-
-translations
-    "x <~~> y" == "(x,y) : perm"
-
-inductive perm
-  intrs
-    Nil   "[] <~~> []"
-    swap  "y#x#l <~~> x#y#l"
-    Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
-    trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/PropLog.ML
--- a/src/HOL/ex/PropLog.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +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)
-*)
-
-open PropLog;
-
-(** Monotonicity **)
-goalw PropLog.thy thms.defs "!!G H. 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 PropLog.thy "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 PropLog.thy "!!H. H |- q ==> H |- p->q";
-by (fast_tac (!claset addIs [thms.K,thms.MP]) 1);
-qed "weaken_right";
-
-(*The deduction theorem*)
-goal PropLog.thy "!!H. 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));
-
-(** The function eval **)
-
-goalw PropLog.thy [eval_def] "tt[false] = False";
-by (Simp_tac 1);
-qed "eval_false";
-
-goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
-by (Simp_tac 1);
-qed "eval_var";
-
-goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
-by (Simp_tac 1);
-qed "eval_imp";
-
-Addsimps [eval_false, eval_var, eval_imp];
-
-(*Soundness of the rules wrt truth-table semantics*)
-goalw PropLog.thy [sat_def] "!!H. 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 PropLog.thy "!!H. 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 PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
-by (rtac (expand_if RS iffD2) 1);
-by (PropLog.pl.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 (Fast_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 PropLog.thy "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 PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
-by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (Simp_tac 1);
-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 PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
-by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (Simp_tac 1);
-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";
-
-(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
- could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
-goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
-by (PropLog.pl.induct_tac "p" 1);
-by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
-qed "hyps_finite";
-
-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_finite RS Fin_induct) 1);
-by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (safe_tac (!claset));
-(*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 PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "sat_imp";
-
-val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
-by (rtac (finite RS Fin_induct) 1);
-by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
-by (rtac (weaken_left_insert RS thms.MP) 1);
-by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
-by (Fast_tac 1);
-qed "completeness_lemma";
-
-val completeness = completeness_lemma RS spec RS mp;
-
-val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
-by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
-qed "thms_iff";
-
-writeln"Reached end of file.";
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/PropLog.thy
--- a/src/HOL/ex/PropLog.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*  Title:      HOL/ex/PropLog.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994  TU Muenchen
-
-Inductive definition of propositional logic.
-*)
-
-PropLog = Finite +
-datatype
-    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
-consts
-  thms :: 'a pl set => 'a pl set
-  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
-  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
-  eval2 :: ['a pl, 'a set] => bool
-  eval  :: ['a set, 'a pl] => bool      ("_[_]" [100,0] 100)
-  hyps  :: ['a pl, 'a set] => 'a pl set
-
-translations
-  "H |- p" == "p : 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"
-
-defs
-  sat_def  "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
-  eval_def "tt[p] == eval2 p tt"
-
-primrec eval2 pl
-  "eval2(false) = (%x.False)"
-  "eval2(#v) = (%tt.v:tt)"
-  "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
-
-primrec hyps pl
-  "hyps(false) = (%tt.{})"
-  "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
-  "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
-
-end
-
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed May 07 13:51:22 1997 +0200
@@ -16,22 +16,13 @@
 (** time_use "mesontest2.ML";  ULTRA SLOW **)
 time_use_thy "String";
 time_use_thy "BT";
-time_use_thy "Perm";
-time_use_thy "Comb";
 time_use_thy "InSort";
 time_use_thy "Qsort";
 time_use_thy "LexProd";
 time_use_thy "Puzzle";
-time_use_thy "Mutil";
 time_use_thy "Primes";
 time_use_thy "NatSum";
 time_use     "set.ML";
-time_use_thy "SList";
-time_use_thy "LFilter";
-time_use_thy "Acc";
-time_use_thy "PropLog";
-time_use_thy "Term";
-time_use_thy "Simult";
 time_use_thy "MT";
 
 writeln "END: Root file for HOL examples";
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,372 +0,0 @@
-(*  Title:      HOL/ex/SList.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Definition of type 'a list by a least fixed point
-*)
-
-open SList;
-
-val list_con_defs = [NIL_def, CONS_def];
-
-goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
-let val rew = rewrite_rule list_con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew list.intrs)
-                      addEs [rew list.elim]) 1)
-end;
-qed "list_unfold";
-
-(*This justifies using list in other recursive type definitions*)
-goalw SList.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "list_mono";
-
-(*Type checking -- list creates well-founded sets*)
-goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
-by (rtac lfp_lowerbound 1);
-by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
-qed "list_sexp";
-
-(* A <= sexp ==> list(A) <= sexp *)
-bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
-
-(*Induction for the type 'a list *)
-val prems = goalw SList.thy [Nil_def,Cons_def]
-    "[| P(Nil);   \
-\       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
-by (rtac (Rep_list_inverse RS subst) 1);   (*types force good instantiation*)
-by (rtac (Rep_list RS list.induct) 1);
-by (REPEAT (ares_tac prems 1
-     ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
-qed "list_induct2";
-
-(*Perform induction on xs. *)
-fun list_ind_tac a M = 
-    EVERY [res_inst_tac [("l",a)] list_induct2 M,
-           rename_last_tac a ["1"] (M+1)];
-
-(*** Isomorphisms ***)
-
-goal SList.thy "inj(Rep_list)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_list_inverse 1);
-qed "inj_Rep_list";
-
-goal SList.thy "inj_onto Abs_list (list(range Leaf))";
-by (rtac inj_onto_inverseI 1);
-by (etac Abs_list_inverse 1);
-qed "inj_onto_Abs_list";
-
-(** Distinctness of constructors **)
-
-goalw SList.thy list_con_defs "CONS M N ~= NIL";
-by (rtac In1_not_In0 1);
-qed "CONS_not_NIL";
-bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
-
-bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
-val NIL_neq_CONS = sym RS CONS_neq_NIL;
-
-goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
-by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
-qed "Cons_not_Nil";
-
-bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
-
-(** Injectiveness of CONS and Cons **)
-
-goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
-by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
-qed "CONS_CONS_eq";
-
-(*For reasoning about abstract list constructors*)
-AddIs ([Rep_list] @ list.intrs);
-
-AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
-
-AddSDs [inj_onto_Abs_list RS inj_ontoD,
-        inj_Rep_list RS injD, Leaf_inject];
-
-goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
-qed "Cons_Cons_eq";
-bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
-
-val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
-by (rtac (major RS setup_induction) 1);
-by (etac list.induct 1);
-by (ALLGOALS (Fast_tac));
-qed "CONS_D";
-
-val prems = goalw SList.thy [CONS_def,In1_def]
-    "CONS M N: sexp ==> M: sexp & N: sexp";
-by (cut_facts_tac prems 1);
-by (fast_tac (!claset addSDs [Scons_D]) 1);
-qed "sexp_CONS_D";
-
-
-(*Reasoning about constructors and their freeness*)
-Addsimps list.intrs;
-
-AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
-
-goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
-by (etac list.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "not_CONS_self";
-
-goal SList.thy "!x. l ~= x#l";
-by (list_ind_tac "l" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "not_Cons_self2";
-
-
-goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)";
-by (list_ind_tac "xs" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-by (REPEAT(resolve_tac [exI,refl,conjI] 1));
-qed "neq_Nil_conv2";
-
-(** Conversion rules for List_case: case analysis operator **)
-
-goalw SList.thy [List_case_def,NIL_def] "List_case c h NIL = c";
-by (rtac Case_In0 1);
-qed "List_case_NIL";
-
-goalw SList.thy [List_case_def,CONS_def]  "List_case c h (CONS M N) = h M N";
-by (simp_tac (!simpset addsimps [Split,Case_In1]) 1);
-qed "List_case_CONS";
-
-(*** List_rec -- by wf recursion on pred_sexp ***)
-
-(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
-   hold if pred_sexp^+ were changed to pred_sexp. *)
-
-goal SList.thy
-   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
-                           \     (%g. List_case c (%x y. d x y (g y)))";
-by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
-val List_rec_unfold = standard 
-  ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
-
-(*---------------------------------------------------------------------------
- * Old:
- * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
- *                     |> standard;
- *---------------------------------------------------------------------------*)
-
-(** pred_sexp lemmas **)
-
-goalw SList.thy [CONS_def,In1_def]
-    "!!M. [| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
-by (Asm_simp_tac 1);
-qed "pred_sexp_CONS_I1";
-
-goalw SList.thy [CONS_def,In1_def]
-    "!!M. [| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
-by (Asm_simp_tac 1);
-qed "pred_sexp_CONS_I2";
-
-val [prem] = goal SList.thy
-    "(CONS M1 M2, N) : pred_sexp^+ ==> \
-\    (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
-by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS 
-                   subsetD RS SigmaE2)) 1);
-by (etac (sexp_CONS_D RS conjE) 1);
-by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2,
-                      prem RSN (2, trans_trancl RS transD)] 1));
-qed "pred_sexp_CONS_D";
-
-(** Conversion rules for List_rec **)
-
-goal SList.thy "List_rec NIL c h = c";
-by (rtac (List_rec_unfold RS trans) 1);
-by (simp_tac (!simpset addsimps [List_case_NIL]) 1);
-qed "List_rec_NIL";
-
-goal SList.thy "!!M. [| M: sexp;  N: sexp |] ==> \
-\    List_rec (CONS M N) c h = h M N (List_rec N c h)";
-by (rtac (List_rec_unfold RS trans) 1);
-by (asm_simp_tac (!simpset addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
-qed "List_rec_CONS";
-
-(*** list_rec -- by List_rec ***)
-
-val Rep_list_in_sexp =
-    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
-
-local
-  val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
-                        Abs_list_inverse, Rep_list_inverse,
-                        Rep_list, rangeI, inj_Leaf, inv_f_f,
-                        sexp.LeafI, Rep_list_in_sexp]
-in
-  val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
-      "list_rec Nil c h = c"
-   (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
-
-  val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def]
-      "list_rec (a#l) c h = h a l (list_rec l c h)"
-   (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
-end;
-
-Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons];
-
-
-(*Type checking.  Useful?*)
-val major::A_subset_sexp::prems = goal SList.thy
-    "[| M: list(A);     \
-\       A<=sexp;        \
-\       c: C(NIL);      \
-\       !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
-\    |] ==> List_rec M c h : C(M :: 'a item)";
-val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
-val sexp_A_I = A_subset_sexp RS subsetD;
-by (rtac (major RS list.induct) 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
-qed "List_rec_type";
-
-(** Generalized map functionals **)
-
-goalw SList.thy [Rep_map_def] "Rep_map f Nil = NIL";
-by (rtac list_rec_Nil 1);
-qed "Rep_map_Nil";
-
-goalw SList.thy [Rep_map_def]
-    "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
-by (rtac list_rec_Cons 1);
-qed "Rep_map_Cons";
-
-goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
-by (rtac list_induct2 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Rep_map_type";
-
-goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil";
-by (rtac List_rec_NIL 1);
-qed "Abs_map_NIL";
-
-val prems = goalw SList.thy [Abs_map_def]
-    "[| M: sexp;  N: sexp |] ==> \
-\    Abs_map g (CONS M N) = g(M) # Abs_map g N";
-by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
-qed "Abs_map_CONS";
-
-(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
-val [rew] = goal SList.thy
-    "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
-by (rewtac rew);
-by (rtac list_rec_Nil 1);
-qed "def_list_rec_Nil";
-
-val [rew] = goal SList.thy
-    "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
-by (rewtac rew);
-by (rtac list_rec_Cons 1);
-qed "def_list_rec_Cons";
-
-fun list_recs def =
-      [standard (def RS def_list_rec_Nil),
-       standard (def RS def_list_rec_Cons)];
-
-(*** Unfolding the basic combinators ***)
-
-val [null_Nil, null_Cons]               = list_recs null_def;
-val [_, hd_Cons]                        = list_recs hd_def;
-val [_, tl_Cons]                        = list_recs tl_def;
-val [ttl_Nil, ttl_Cons]                 = list_recs ttl_def;
-val [append_Nil3, append_Cons]          = list_recs append_def;
-val [mem_Nil, mem_Cons]                 = list_recs mem_def;
-val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
-val [map_Nil, map_Cons]                 = list_recs map_def;
-val [list_case_Nil, list_case_Cons]     = list_recs list_case_def;
-val [filter_Nil, filter_Cons]           = list_recs filter_def;
-
-Addsimps
-  [null_Nil, ttl_Nil,
-   mem_Nil, mem_Cons,
-   list_case_Nil, list_case_Cons,
-   append_Nil3, append_Cons,
-   set_of_list_Nil, set_of_list_Cons, 
-   map_Nil, map_Cons,
-   filter_Nil, filter_Cons];
-
-
-(** @ - append **)
-
-goal SList.thy "(xs@ys)@zs = xs@(ys@zs)";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "append_assoc2";
-
-goal SList.thy "xs @ [] = xs";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "append_Nil4";
-
-(** mem **)
-
-goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-qed "mem_append2";
-
-goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-qed "mem_filter2";
-
-
-(** The functional "map" **)
-
-Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
-
-val [major,A_subset_sexp,minor] = goal SList.thy 
-    "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
-\    ==> Rep_map f (Abs_map g M) = M";
-by (rtac (major RS list.induct) 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sexp_A_I,sexp_ListA_I,minor])));
-qed "Abs_map_inverse";
-
-(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
-
-(** list_case **)
-
-goal SList.thy
- "P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\                        (!y ys. xs=y#ys --> P(f y ys)))";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-qed "expand_list_case2";
-
-
-(** Additional mapping lemmas **)
-
-goal SList.thy "map (%x.x) xs = xs";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_ident2";
-
-goal SList.thy "map f (xs@ys) = map f xs @ map f ys";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_append2";
-
-goalw SList.thy [o_def] "map (f o g) xs = map f (map g xs)";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_compose2";
-
-goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
-\       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac(!simpset addsimps
-       [Rep_map_type,list_sexp RS subsetD])));
-qed "Abs_Rep_map";
-
-Addsimps [append_Nil4, map_ident2];
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-(*  Title:      HOL/ex/SList.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Definition of type 'a list (strict lists) by a least fixed point
-
-We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
-so that list can serve as a "functor" for defining other recursive types
-*)
-
-SList = Sexp +
-
-types
-  'a list
-
-arities
-  list :: (term) term
-
-
-consts
-
-  list        :: 'a item set => 'a item set
-  Rep_list    :: 'a list => 'a item
-  Abs_list    :: 'a item => 'a list
-  NIL         :: 'a item
-  CONS        :: ['a item, 'a item] => 'a item
-  Nil         :: 'a list
-  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
-  List_case   :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
-  List_rec    :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
-  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
-  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
-  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
-  Abs_map     :: ('a item => 'b) => 'a item => 'b list
-  null        :: 'a list => bool
-  hd          :: 'a list => 'a
-  tl,ttl      :: 'a list => 'a list
-  set_of_list :: ('a list => 'a set)
-  mem         :: ['a, 'a list] => bool                            (infixl 55)
-  map         :: ('a=>'b) => ('a list => 'b list)
-  "@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
-  filter      :: ['a => bool, 'a list] => 'a list
-
-  (* list Enumeration *)
-
-  "[]"        :: 'a list                              ("[]")
-  "@list"     :: args => 'a list                      ("[(_)]")
-
-  (* Special syntax for filter *)
-  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
-
-translations
-  "[x, xs]"     == "x#[xs]"
-  "[x]"         == "x#[]"
-  "[]"          == "Nil"
-
-  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
-
-  "[x:xs . P]"  == "filter (%x.P) xs"
-
-defs
-  (* Defining the Concrete Constructors *)
-  NIL_def       "NIL == In0(Numb(0))"
-  CONS_def      "CONS M N == In1(M $ N)"
-
-inductive "list(A)"
-  intrs
-    NIL_I  "NIL: list(A)"
-    CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"
-
-rules
-  (* Faking a Type Definition ... *)
-  Rep_list          "Rep_list(xs): list(range(Leaf))"
-  Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
-  Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
-
-
-defs
-  (* Defining the Abstract Constructors *)
-  Nil_def       "Nil == Abs_list(NIL)"
-  Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
-
-  List_case_def "List_case c d == Case (%x.c) (Split d)"
-
-  (* list Recursion -- the trancl is Essential; see list.ML *)
-
-  List_rec_def
-   "List_rec M c d == wfrec (trancl pred_sexp)
-                            (%g. List_case c (%x y. d x y (g y))) M"
-
-  list_rec_def
-   "list_rec l c d == 
-   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
-
-  (* Generalized Map Functionals *)
-
-  Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
-  Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
-
-  null_def      "null(xs)            == list_rec xs True (%x xs r.False)"
-  hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
-  tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
-  (* a total version of tl: *)
-  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
-
-  set_of_list_def "set_of_list xs    == list_rec xs {} (%x l r. insert x r)"
-
-  mem_def       "x mem xs            == 
-                   list_rec xs False (%y ys r. if y=x then True else r)"
-  map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
-  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
-  filter_def    "filter P xs         == 
-                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
-
-  list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
-
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,298 +0,0 @@
-(*  Title:      HOL/ex/Simult.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Primitives for simultaneous recursive type definitions
-  includes worked example of trees & forests
-
-This is essentially the same data structure that on ex/term.ML, which is
-simpler because it uses list as a new type former.  The approach in this
-file may be superior for other simultaneous recursions.
-*)
-
-open Simult;
-
-(*** Monotonicity and unfolding of the function ***)
-
-goal Simult.thy "mono(%Z.  A <*> Part Z In1 \
-\                      <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))";
-by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
-                      Part_mono] 1));
-qed "TF_fun_mono";
-
-val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
-
-goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
-by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
-qed "TF_mono";
-
-goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
-by (rtac lfp_lowerbound 1);
-by (blast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
-                      addSEs [PartE]) 1);
-qed "TF_sexp";
-
-(* A <= sexp ==> TF(A) <= sexp *)
-val TF_subset_sexp = standard
-    (TF_mono RS (TF_sexp RSN (2,subset_trans)));
-
-
-(** Elimination -- structural induction on the set TF **)
-
-val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
-
-val major::prems = goalw Simult.thy TF_Rep_defs
- "[| i: TF(A);  \
-\    !!M N. [| M: A;  N: Part (TF A) In1;  R(N) |] ==> R(TCONS M N);    \
-\    R(FNIL);                   \
-\    !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  R(M);  R(N) \
-\            |] ==> R(FCONS M N)    \
-\    |] ==> R(i)";
-by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (blast_tac (!claset addIs (prems@[PartI])
-                       addEs [usumE, uprodE, PartE]) 1);
-qed "TF_induct";
-
-(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
-goalw Simult.thy [Part_def]
- "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
-\                   (M: Part (TF A) In1 --> Q(M)) \
-\  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
-by (Blast_tac 1);
-qed "TF_induct_lemma";
-
-(*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
-
-(*Induction on TF with separate predicates P, Q*)
-val prems = goalw Simult.thy TF_Rep_defs
-    "[| !!M N. [| M: A;  N: Part (TF A) In1;  Q(N) |] ==> P(TCONS M N); \
-\       Q(FNIL);        \
-\       !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  P(M);  Q(N) \
-\               |] ==> Q(FCONS M N)     \
-\    |] ==> (! M: Part (TF A) In0. P(M)) & (! N: Part (TF A) In1. Q(N))";
-by (rtac (ballI RS TF_induct_lemma) 1);
-by (etac TF_induct 1);
-by (rewrite_goals_tac TF_Rep_defs);
-	(*Blast_tac needs this type instantiation in order to preserve the
-          right overloading of equality.  The injectiveness properties for
-          type 'a item hold only for set types.*)
-val PartE' = read_instantiate [("'a", "?'c set")] PartE;
-by (ALLGOALS (blast_tac (!claset addSEs [PartE'] addIs prems)));
-qed "Tree_Forest_induct";
-
-(*Induction for the abstract types 'a tree, 'a forest*)
-val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
-    "[| !!x ts. Q(ts) ==> P(Tcons x ts);     \
-\       Q(Fnil);        \
-\       !!t ts. [| P(t);  Q(ts) |] ==> Q(Fcons t ts)    \
-\    |] ==> (! t. P(t)) & (! ts. Q(ts))";
-by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
-                  ("Q1","%z.Q(Abs_Forest(z))")] 
-    (Tree_Forest_induct RS conjE) 1);
-(*Instantiates ?A1 to range(Leaf). *)
-by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
-			      Rep_Forest_inverse RS subst] 
-                       addSIs [Rep_Tree,Rep_Forest]) 4);
-(*Cannot use simplifier: the rewrites work in the wrong direction!*)
-by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
-					Abs_Forest_inverse RS subst] 
-                                addSIs prems)));
-qed "tree_forest_induct";
-
-
-
-(*** Isomorphisms ***)
-
-goal Simult.thy "inj(Rep_Tree)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_Tree_inverse 1);
-qed "inj_Rep_Tree";
-
-goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)";
-by (rtac inj_onto_inverseI 1);
-by (etac Abs_Tree_inverse 1);
-qed "inj_onto_Abs_Tree";
-
-goal Simult.thy "inj(Rep_Forest)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_Forest_inverse 1);
-qed "inj_Rep_Forest";
-
-goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)";
-by (rtac inj_onto_inverseI 1);
-by (etac Abs_Forest_inverse 1);
-qed "inj_onto_Abs_Forest";
-
-(** Introduction rules for constructors **)
-
-(* c : A <*> Part (TF A) In1 
-        <+> {Numb(0)} <+> Part (TF A) In0 <*> Part (TF A) In1 ==> c : TF(A) *)
-val TF_I = TF_unfold RS equalityD2 RS subsetD;
-
-(*For reasoning about the representation*)
-AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
-AddSEs [Scons_inject];
-
-goalw Simult.thy TF_Rep_defs
-    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (Blast_tac 1);
-qed "TCONS_I";
-
-(* FNIL is a TF(A) -- this also justifies the type definition*)
-goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
-by (Blast_tac 1);
-qed "FNIL_I";
-
-goalw Simult.thy TF_Rep_defs
-    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
-\         FCONS M N : Part (TF A) In1";
-by (Blast_tac 1);
-qed "FCONS_I";
-
-(** Injectiveness of TCONS and FCONS **)
-
-goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
-by (Blast_tac 1);
-qed "TCONS_TCONS_eq";
-bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
-
-goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
-by (Blast_tac 1);
-qed "FCONS_FCONS_eq";
-bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
-
-(** Distinctness of TCONS, FNIL and FCONS **)
-
-goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
-by (Blast_tac 1);
-qed "TCONS_not_FNIL";
-bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
-
-bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
-val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
-
-goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
-by (Blast_tac 1);
-qed "FCONS_not_FNIL";
-bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
-
-bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
-val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
-
-goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
-by (Blast_tac 1);
-qed "TCONS_not_FCONS";
-bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
-
-bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
-val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
-
-(*???? Too many derived rules ????
-  Automatically generate symmetric forms?  Always expand TF_Rep_defs? *)
-
-(** Injectiveness of Tcons and Fcons **)
-
-(*For reasoning about abstract constructors*)
-AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
-AddSEs [TCONS_inject, FCONS_inject,
-                           TCONS_neq_FNIL, FNIL_neq_TCONS,
-                           FCONS_neq_FNIL, FNIL_neq_FCONS,
-                           TCONS_neq_FCONS, FCONS_neq_TCONS];
-AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
-                           inj_onto_Abs_Forest RS inj_ontoD,
-                           inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
-                           Leaf_inject];
-
-goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
-by (Blast_tac 1);
-qed "Tcons_Tcons_eq";
-bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
-
-goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
-by (Blast_tac 1);
-qed "Fcons_not_Fnil";
-
-bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
-val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
-
-
-(** Injectiveness of Fcons **)
-
-goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
-by (Blast_tac 1);
-qed "Fcons_Fcons_eq";
-bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
-
-
-(*** TF_rec -- by wf recursion on pred_sexp ***)
-
-goal Simult.thy
-   "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
-                         \       (%g. Case (Split(%x y. b x y (g y))) \
-                         \           (List_case c (%x y. d x y (g x) (g y))))";
-by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
-val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS 
-                    ((result() RS eq_reflection) RS def_wfrec);
-
-(*---------------------------------------------------------------------------
- * Old: 
- * val TF_rec_unfold =
- *   wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
- *---------------------------------------------------------------------------*)
-
-(** conversion rules for TF_rec **)
-
-goalw Simult.thy [TCONS_def]
-    "!!M N. [| M: sexp;  N: sexp |] ==>         \
-\           TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
-by (rtac (TF_rec_unfold RS trans) 1);
-by (simp_tac (!simpset addsimps [Case_In0, Split]) 1);
-by (asm_simp_tac (!simpset addsimps [In0_def]) 1);
-qed "TF_rec_TCONS";
-
-goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c";
-by (rtac (TF_rec_unfold RS trans) 1);
-by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
-qed "TF_rec_FNIL";
-
-goalw Simult.thy [FCONS_def]
- "!!M N. [| M: sexp;  N: sexp |] ==>    \
-\        TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
-by (rtac (TF_rec_unfold RS trans) 1);
-by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
-by (asm_simp_tac (!simpset addsimps [CONS_def,In1_def]) 1);
-qed "TF_rec_FCONS";
-
-
-(*** tree_rec, forest_rec -- by TF_rec ***)
-
-val Rep_Tree_in_sexp =
-    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
-     Rep_Tree] MRS subsetD;
-val Rep_Forest_in_sexp =
-    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
-     Rep_Forest] MRS subsetD;
-
-val tf_rec_ss = HOL_ss addsimps
-  [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
-   TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
-   Rep_Tree_inverse, Rep_Forest_inverse,
-   Abs_Tree_inverse, Abs_Forest_inverse,
-   inj_Leaf, inv_f_f, sexp.LeafI, range_eqI,
-   Rep_Tree_in_sexp, Rep_Forest_in_sexp];
-
-goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
-    "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)";
-by (simp_tac tf_rec_ss 1);
-qed "tree_rec_Tcons";
-
-goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c";
-by (simp_tac tf_rec_ss 1);
-qed "forest_rec_Fnil";
-
-goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
-    "forest_rec (Fcons t tf) b c d = \
-\    d t tf (tree_rec t b c d) (forest_rec tf b c d)";
-by (simp_tac tf_rec_ss 1);
-qed "forest_rec_Cons";
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Simult.thy
--- a/src/HOL/ex/Simult.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(*  Title:      HOL/ex/Simult
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-A simultaneous recursive type definition: trees & forests
-
-This is essentially the same data structure that on ex/term.ML, which is
-simpler because it uses list as a new type former.  The approach in this
-file may be superior for other simultaneous recursions.
-
-The inductive definition package does not help defining this sort of mutually
-recursive data structure because it uses Inl, Inr instead of In0, In1.
-*)
-
-Simult = SList +
-
-types    'a tree
-         'a forest
-
-arities  tree,forest :: (term)term
-
-consts
-  TF          :: 'a item set => 'a item set
-  FNIL        :: 'a item
-  TCONS,FCONS :: ['a item, 'a item] => 'a item
-  Rep_Tree    :: 'a tree => 'a item
-  Abs_Tree    :: 'a item => 'a tree
-  Rep_Forest  :: 'a forest => 'a item
-  Abs_Forest  :: 'a item => 'a forest
-  Tcons       :: ['a, 'a forest] => 'a tree
-  Fcons       :: ['a tree, 'a forest] => 'a forest
-  Fnil        :: 'a forest
-  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
-                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
-  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
-                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
-  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
-                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
-
-defs
-     (*the concrete constants*)
-  TCONS_def     "TCONS M N == In0(M $ N)"
-  FNIL_def      "FNIL      == In1(NIL)"
-  FCONS_def     "FCONS M N == In1(CONS M N)"
-     (*the abstract constants*)
-  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
-  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
-  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
-
-  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
-                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
-
-rules
-  (*faking a type definition for tree...*)
-  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
-  Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
-  Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
-    (*faking a type definition for forest...*)
-  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
-  Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
-  Abs_Forest_inverse 
-        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
-
-
-defs
-     (*recursion*)
-  TF_rec_def    
-   "TF_rec M b c d == wfrec (trancl pred_sexp)
-               (%g. Case (Split(%x y. b x y (g y))) 
-                      (List_case c (%x y. d x y (g x) (g y)))) M"
-
-  tree_rec_def
-   "tree_rec t b c d == 
-   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
-          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
-
-  forest_rec_def
-   "forest_rec tf b c d == 
-   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
-          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
-end
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Term.ML
--- a/src/HOL/ex/Term.ML	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(*  Title:      HOL/ex/Term
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Terms over a given alphabet -- function applications; illustrates list functor
-  (essentially the same type as in Trees & Forests)
-*)
-
-open Term;
-
-(*** Monotonicity and unfolding of the function ***)
-
-goal Term.thy "term(A) = A <*> list(term(A))";
-by (fast_tac (!claset addSIs (equalityI :: term.intrs)
-                      addEs [term.elim]) 1);
-qed "term_unfold";
-
-(*This justifies using term in other recursive type definitions*)
-goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
-by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
-qed "term_mono";
-
-(** Type checking -- term creates well-founded sets **)
-
-goalw Term.thy term.defs "term(sexp) <= sexp";
-by (rtac lfp_lowerbound 1);
-by (fast_tac (!claset addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
-qed "term_sexp";
-
-(* A <= sexp ==> term(A) <= sexp *)
-bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
-
-
-(** Elimination -- structural induction on the set term(A) **)
-
-(*Induction for the set term(A) *)
-val [major,minor] = goal Term.thy 
-    "[| M: term(A);  \
-\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x.R(x)}) \
-\               |] ==> R(x$zs)  \
-\    |] ==> R(M)";
-by (rtac (major RS term.induct) 1);
-by (REPEAT (eresolve_tac ([minor] @
-                ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
-(*Proof could also use  mono_Int RS subsetD RS IntE *)
-qed "Term_induct";
-
-(*Induction on term(A) followed by induction on list *)
-val major::prems = goal Term.thy
-    "[| M: term(A);  \
-\       !!x.      [| x: A |] ==> R(x$NIL);  \
-\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
-\                 |] ==> R(x $ CONS z zs)  \
-\    |] ==> R(M)";
-by (rtac (major RS Term_induct) 1);
-by (etac list.induct 1);
-by (REPEAT (ares_tac prems 1));
-qed "Term_induct2";
-
-(*** Structural Induction on the abstract type 'a term ***)
-
-val Rep_term_in_sexp =
-    Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
-
-(*Induction for the abstract type 'a term*)
-val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
-    "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts)  \
-\    |] ==> R(t)";
-by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
-by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
-by (rtac (Rep_term RS Term_induct) 1);
-by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
-    list_subset_sexp, range_Leaf_subset_sexp] 1
-     ORELSE etac rev_subsetD 1));
-by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
-        (Abs_map_inverse RS subst) 1);
-by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
-by (etac Abs_term_inverse 1);
-by (etac rangeE 1);
-by (hyp_subst_tac 1);
-by (resolve_tac prems 1);
-by (etac list.induct 1);
-by (etac CollectE 2);
-by (stac Abs_map_CONS 2);
-by (etac conjunct1 2);
-by (etac rev_subsetD 2);
-by (rtac list_subset_sexp 2);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Fast_tac);
-qed "term_induct";
-
-(*Induction for the abstract type 'a term*)
-val prems = goal Term.thy 
-    "[| !!x. R(App x Nil);  \
-\       !!x t ts. R(App x ts) ==> R(App x (t#ts))  \
-\    |] ==> R(t)";
-by (rtac term_induct 1);  (*types force good instantiation*)
-by (etac rev_mp 1);
-by (rtac list_induct2 1);  (*types force good instantiation*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
-qed "term_induct2";
-
-(*Perform induction on xs. *)
-fun term_ind2_tac a i = 
-    EVERY [res_inst_tac [("t",a)] term_induct2 i,
-           rename_last_tac a ["1","s"] (i+1)];
-
-
-
-(*** Term_rec -- by wf recursion on pred_sexp ***)
-
-goal Term.thy
-   "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
-                             \ (%g. Split(%x y. d x y (Abs_map g y)))";
-by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
-bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
-                            ((result() RS eq_reflection) RS def_wfrec));
-
-(*---------------------------------------------------------------------------
- * Old:
- * val Term_rec_unfold =
- *     wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
- *---------------------------------------------------------------------------*)
-
-(** conversion rules **)
-
-val [prem] = goal Term.thy
-    "N: list(term(A)) ==>  \
-\    !M. (N,M): pred_sexp^+ --> \
-\        Abs_map (cut h (pred_sexp^+) M) N = \
-\        Abs_map h N";
-by (rtac (prem RS list.induct) 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (etac (pred_sexp_CONS_D RS conjE) 1);
-by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 1);
-qed "Abs_map_lemma";
-
-val [prem1,prem2,A_subset_sexp] = goal Term.thy
-    "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
-\    Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
-by (rtac (Term_rec_unfold RS trans) 1);
-by (simp_tac (HOL_ss addsimps
-      [Split,
-       prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
-       prem1, prem2 RS rev_subsetD, list_subset_sexp,
-       term_subset_sexp, A_subset_sexp]) 1);
-qed "Term_rec";
-
-(*** term_rec -- by Term_rec ***)
-
-local
-  val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
-                        [("f","Rep_term")] Rep_map_type;
-  val Rep_Tlist = Rep_term RS Rep_map_type1;
-  val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
-
-  (*Now avoids conditional rewriting with the premise N: list(term(A)),
-    since A will be uninstantiated and will cause rewriting to fail. *)
-  val term_rec_ss = HOL_ss
-      addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
-                Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
-                inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
-in
-
-val term_rec = prove_goalw Term.thy
-         [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
-    "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)"
- (fn _ => [simp_tac term_rec_ss 1])
-
-end;
diff -r 1c0dfa7ebb72 -r 3f0ab2c306f7 src/HOL/ex/Term.thy
--- a/src/HOL/ex/Term.thy	Wed May 07 13:50:52 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(*  Title:      HOL/ex/Term
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Terms over a given alphabet -- function applications; illustrates list functor
-  (essentially the same type as in Trees & Forests)
-
-There is no constructor APP because it is simply cons ($) 
-*)
-
-Term = SList +
-
-types   'a term
-
-arities term :: (term)term
-
-consts
-  term          :: 'a item set => 'a item set
-  Rep_term      :: 'a term => 'a item
-  Abs_term      :: 'a item => 'a term
-  Rep_Tlist     :: 'a term list => 'a item
-  Abs_Tlist     :: 'a item => 'a term list
-  App           :: ['a, ('a term)list] => 'a term
-  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
-  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
-
-inductive "term(A)"
-  intrs
-    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
-  monos   "[list_mono]"
-
-defs
-  (*defining abstraction/representation functions for term list...*)
-  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
-  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
-
-  (*defining the abstract constants*)
-  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
-
-  (*list recursion*)
-  Term_rec_def  
-   "Term_rec M d == wfrec (trancl pred_sexp)
-           (%g. Split(%x y. d x y (Abs_map g y))) M"
-
-  term_rec_def
-   "term_rec t d == 
-   Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
-
-rules
-    (*faking a type definition for term...*)
-  Rep_term              "Rep_term(n): term(range(Leaf))"
-  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
-  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
-end