reorganization of the ZF examples

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Acc.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,58 @@
+(*  Title:      ZF/ex/acc
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  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.
+*)
+
+(*The introduction rule must require  a \\<in> field(r)  
+  Otherwise acc(r) would be a proper class!    *)
+
+(*The intended introduction rule*)
+val prems = goal Acc.thy
+    "[| !!b. <b,a>:r ==> b \\<in> acc(r);  a \\<in> field(r) |] ==> a \\<in> acc(r)";
+by (fast_tac (claset() addIs [e-mail]) 1);
+qed "accI";
+
+Goal "[| b \\<in> acc(r);  <a,b>: r |] ==> a \\<in> acc(r)";
+by (etac acc.elim 1);
+by (Fast_tac 1);
+qed "acc_downward";
+
+val [major,indhyp] = goal Acc.thy
+    "[| a \\<in> acc(r);                                             \
+\       !!x. [| x \\<in> acc(r);  \\<forall>y. <y,x>:r --> P(y) |] ==> P(x) \
+\    |] ==> P(a)";
+by (rtac (major RS acc.induct) 1);
+by (rtac indhyp 1);
+by (Fast_tac 2);
+by (resolve_tac acc.intrs 1);
+by (assume_tac 2);
+by (etac (Collect_subset RS Pow_mono RS subsetD) 1);
+qed "acc_induct";
+
+Goal "wf[acc(r)](r)";
+by (rtac wf_onI2 1);
+by (etac acc_induct 1);
+by (Fast_tac 1);
+qed "wf_on_acc";
+
+(* field(r) \\<subseteq> acc(r) ==> wf(r) *)
+val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
+
+val [major] = goal Acc.thy "wf(r) ==> field(r) \\<subseteq> acc(r)";
+by (rtac subsetI 1);
+by (etac (major RS wf_induct2) 1);
+by (rtac subset_refl 1);
+by (rtac accI 1);
+by (assume_tac 2);
+by (Fast_tac 1);
+qed "acc_wfD";
+
+Goal "wf(r) <-> field(r) \\<subseteq> acc(r)";
+by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
+qed "wf_acc_iff";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Acc.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,23 @@
+(*  Title:      ZF/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 = Main +
+
+consts
+  acc :: i=>i
+
+inductive
+  domains "acc(r)" <= "field(r)"
+  intrs
+    vimage  "[| r-``{a}: Pow(acc(r)); a \\<in> field(r) |] ==> a \\<in> acc(r)"
+  monos      Pow_mono
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Comb.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,222 @@
+(*  Title:      ZF/ex/comb.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   1993  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
+*)
+
+(*** Transitive closure preserves the Church-Rosser property ***)
+
+Goalw [diamond_def]
+    "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
+\    \\<forall>y'. <x,y'>:r --> (\\<exists>z. <y',z>: r^+ & <y,z>: r)";
+by (etac trancl_induct 1);
+by (blast_tac (claset() addIs [r_into_trancl]) 1);
+by (slow_best_tac (claset() addSDs [spec RS mp]
+                           addIs  [r_into_trancl, trans_trancl RS transD]) 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 trancl_induct 1);
+by (ALLGOALS (*Seems to be a brittle, undirected search*)
+    (slow_best_tac (claset() addIs [r_into_trancl, trans_trancl RS transD]
+                            addEs [major RS diamond_strip_lemmaE])));
+qed "diamond_trancl";
+
+
+val [_,_,comb_Ap] = comb.intrs;
+val Ap_E = comb.mk_cases "p#q \\<in> comb";
+
+AddSIs comb.intrs;
+
+
+(*** Results about Contraction ***)
+
+(*For type checking: replaces a-1->b by a,b \\<in> comb *)
+val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
+val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
+val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
+
+Goal "field(contract) = comb";
+by (blast_tac (claset() addIs [contract.K] addSEs [contract_combE2]) 1);
+qed "field_contract_eq";
+
+bind_thm ("reduction_refl",
+    (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl));
+
+bind_thm ("rtrancl_into_rtrancl2",
+    (r_into_rtrancl RS (trans_rtrancl RS transD)));
+
+AddSIs [reduction_refl, contract.K, contract.S];
+
+val reduction_rls = [contract.K RS rtrancl_into_rtrancl2,
+                     contract.S RS rtrancl_into_rtrancl2,
+                     contract.Ap1 RS rtrancl_into_rtrancl2,
+                     contract.Ap2 RS rtrancl_into_rtrancl2];
+
+(*Example only: not used*)
+Goalw [I_def] "p \\<in> comb ==> I#p ---> p";
+by (blast_tac (claset() addIs reduction_rls) 1);
+qed "reduce_I";
+
+Goalw [I_def] "I \\<in> comb";
+by (Blast_tac 1);
+qed "comb_I";
+
+(** Non-contraction results **)
+
+(*Derive a case for each combinator constructor*)
+val K_contractE = contract.mk_cases "K -1-> r";
+val S_contractE = contract.mk_cases "S -1-> r";
+val Ap_contractE = contract.mk_cases "p#q -1-> r";
+
+AddIs  [contract.Ap1, contract.Ap2];
+AddSEs [K_contractE, S_contractE, Ap_contractE];
+
+Goalw [I_def] "I -1-> r ==> P";
+by Auto_tac;
+qed "I_contract_E";
+
+Goal "K#p -1-> r ==> (\\<exists>q. r = K#q & p -1-> q)";
+by Auto_tac;
+qed "K1_contractD";
+
+Goal "[| p ---> q;  r \\<in> comb |] ==> p#r ---> q#r";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (blast_tac (claset() addIs reduction_rls) 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1);
+qed "Ap_reduce1";
+
+Goal "[| p ---> q;  r \\<in> comb |] ==> r#p ---> r#q";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (blast_tac (claset() addIs reduction_rls) 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1);
+qed "Ap_reduce2";
+
+(** Counterexample to the diamond property for -1-> **)
+
+Goal "K#I#(I#I) -1-> I";
+by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
+qed "KIII_contract1";
+
+Goalw [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
+by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
+qed "KIII_contract2";
+
+Goal "K#I#((K#I)#(K#I)) -1-> I";
+by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
+qed "KIII_contract3";
+
+Goalw [diamond_def] "~ diamond(contract)";
+by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3]
+                       addSEs [I_contract_E]) 1);
+qed "not_diamond_contract";
+
+
+
+(*** Results about Parallel Contraction ***)
+
+(*For type checking: replaces a=1=>b by a,b \\<in> comb *)
+val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
+val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
+val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
+
+Goal "field(parcontract) = comb";
+by (blast_tac (claset() addIs [parcontract.K] 
+                      addSEs [parcontract_combE2]) 1);
+qed "field_parcontract_eq";
+
+(*Derive a case for each combinator constructor*)
+val K_parcontractE = parcontract.mk_cases "K =1=> r";
+val S_parcontractE = parcontract.mk_cases "S =1=> r";
+val Ap_parcontractE = parcontract.mk_cases "p#q =1=> r";
+
+AddIs  parcontract.intrs;
+AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE];
+
+(*** Basic properties of parallel contraction ***)
+
+Goal "K#p =1=> r ==> (\\<exists>p'. r = K#p' & p =1=> p')";
+by Auto_tac;
+qed "K1_parcontractD";
+AddSDs [K1_parcontractD];
+
+Goal "S#p =1=> r ==> (\\<exists>p'. r = S#p' & p =1=> p')";
+by Auto_tac;
+qed "S1_parcontractD";
+AddSDs [S1_parcontractD];
+
+Goal "S#p#q =1=> r ==> (\\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
+by Auto_tac;
+qed "S2_parcontractD";
+AddSDs [S2_parcontractD];
+
+(*Church-Rosser property for parallel contraction*)
+Goalw [diamond_def] "diamond(parcontract)";
+by (rtac (impI RS allI RS allI) 1);
+by (etac parcontract.induct 1);
+by (ALLGOALS 
+    (blast_tac (claset() addSEs comb.free_SEs
+			 addIs [parcontract_combD2])));
+qed "diamond_parcontract";
+
+(*** Equivalence of p--->q and p===>q ***)
+
+Goal "p-1->q ==> p=1=>q";
+by (etac contract.induct 1);
+by Auto_tac;
+qed "contract_imp_parcontract";
+
+Goal "p--->q ==> p===>q";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (blast_tac (claset() addIs [r_into_trancl]) 1);
+by (blast_tac (claset() addIs [contract_imp_parcontract, 
+			       r_into_trancl, trans_trancl RS transD]) 1);
+qed "reduce_imp_parreduce";
+
+
+Goal "p=1=>q ==> p--->q";
+by (etac parcontract.induct 1);
+by (blast_tac (claset() addIs reduction_rls) 1);
+by (blast_tac (claset() addIs reduction_rls) 1);
+by (blast_tac (claset() addIs reduction_rls) 1);
+by (blast_tac 
+    (claset() addIs [trans_rtrancl RS transD,
+		     Ap_reduce1, Ap_reduce2, parcontract_combD1,
+		     parcontract_combD2]) 1);
+qed "parcontract_imp_reduce";
+
+Goal "p===>q ==> p--->q";
+by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
+by (etac trancl_induct 1);
+by (etac parcontract_imp_reduce 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (etac parcontract_imp_reduce 1);
+qed "parreduce_imp_reduce";
+
+Goal "p===>q <-> p--->q";
+by (blast_tac (claset() addIs [parreduce_imp_reduce, reduce_imp_parreduce]) 1);
+qed "parreduce_iff_reduce";
+
+writeln"Reached end of file.";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Comb.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,79 @@
+(*  Title:      ZF/ex/Comb.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   1994  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 = Main +
+
+(** Datatype definition of combinators S and K, with infixed application **)
+consts comb :: i
+datatype
+  "comb" = K
+         | S
+         | "#" ("p \\<in> comb", "q \\<in> comb")   (infixl 90)
+
+(** Inductive definition of contractions, -1->
+             and (multi-step) reductions, --->
+**)
+consts
+  contract  :: i
+  "-1->"    :: [i,i] => o                       (infixl 50)
+  "--->"    :: [i,i] => o                       (infixl 50)
+
+translations
+  "p -1-> q" == "<p,q> \\<in> contract"
+  "p ---> q" == "<p,q> \\<in> contract^*"
+
+inductive
+  domains   "contract" <= "comb*comb"
+  intrs
+    K     "[| p \\<in> comb;  q \\<in> comb |] ==> K#p#q -1-> p"
+    S     "[| p \\<in> comb;  q \\<in> comb;  r \\<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
+    Ap1   "[| p-1->q;  r \\<in> comb |] ==> p#r -1-> q#r"
+    Ap2   "[| p-1->q;  r \\<in> comb |] ==> r#p -1-> r#q"
+  type_intrs "comb.intrs"
+
+
+(** Inductive definition of parallel contractions, =1=>
+             and (multi-step) parallel reductions, ===>
+**)
+consts
+  parcontract :: i
+  "=1=>"    :: [i,i] => o                       (infixl 50)
+  "===>"    :: [i,i] => o                       (infixl 50)
+
+translations
+  "p =1=> q" == "<p,q> \\<in> parcontract"
+  "p ===> q" == "<p,q> \\<in> parcontract^+"
+
+inductive
+  domains   "parcontract" <= "comb*comb"
+  intrs
+    refl  "[| p \\<in> comb |] ==> p =1=> p"
+    K     "[| p \\<in> comb;  q \\<in> comb |] ==> K#p#q =1=> p"
+    S     "[| p \\<in> comb;  q \\<in> comb;  r \\<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
+    Ap    "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"
+  type_intrs "comb.intrs"
+
+
+(*Misc definitions*)
+constdefs
+  I :: i
+  "I == S#K#K"
+
+  diamond :: i => o
+  "diamond(r) == \\<forall>x y. <x,y>:r --> 
+                          (\\<forall>y'. <x,y'>:r --> 
+                                   (\\<exists>z. <y,z>:r & <y',z> \\<in> r))"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/ListN.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,46 @@
+(*  Title:      ZF/ex/ListN
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Inductive definition of lists of n elements
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
+*)
+
+Goal "l \\<in> list(A) ==> <length(l),l> \\<in> listn(A)";
+by (etac list.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (REPEAT (ares_tac listn.intrs 1));
+qed "list_into_listn";
+
+Goal "<n,l> \\<in> listn(A) <-> l \\<in> list(A) & length(l)=n";
+by (rtac iffI 1);
+by (blast_tac (claset() addIs [list_into_listn]) 2);
+by (etac listn.induct 1);
+by Auto_tac;
+qed "listn_iff";
+
+Goal "listn(A)``{n} = {l \\<in> list(A). length(l)=n}";
+by (rtac equality_iffI 1);
+by (simp_tac (simpset() addsimps [listn_iff,separation,image_singleton_iff]) 1);
+qed "listn_image_eq";
+
+Goalw listn.defs "A \\<subseteq> B ==> listn(A) \\<subseteq> listn(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac listn.bnd_mono 1));
+by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
+qed "listn_mono";
+
+Goal "[| <n,l> \\<in> listn(A); <n',l'> \\<in> listn(A) |] ==> <n#+n', l@l'> \\<in> listn(A)";
+by (etac listn.induct 1);
+by (ftac (impOfSubs listn.dom_subset) 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs)));
+qed "listn_append";
+
+val Nil_listn_case  = listn.mk_cases "<i,Nil> \\<in> listn(A)"
+and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> \\<in> listn(A)";
+
+val zero_listn_case = listn.mk_cases "<0,l> \\<in> listn(A)"
+and succ_listn_case = listn.mk_cases "<succ(i),l> \\<in> listn(A)";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/ListN.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,22 @@
+(*  Title:      ZF/ex/ListN
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of lists of n elements
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
+*)
+
+ListN = Main +
+
+consts  listn ::i=>i
+inductive
+  domains   "listn(A)" <= "nat*list(A)"
+  intrs
+    NilI  "<0,Nil> \\<in> listn(A)"
+    ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)"
+  type_intrs "nat_typechecks @ list.intrs"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Mutil.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,147 @@
+(*  Title:      ZF/ex/Mutil
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+The Mutilated Checkerboard Problem, formalized inductively
+*)
+
+open Mutil;
+
+
+(** Basic properties of evnodd **)
+
+Goalw [evnodd_def] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b";
+by (Blast_tac 1);
+qed "evnodd_iff";
+
+Goalw [evnodd_def] "evnodd(A, b) \\<subseteq> A";
+by (Blast_tac 1);
+qed "evnodd_subset";
+
+(* Finite(X) ==> Finite(evnodd(X,b)) *)
+bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite);
+
+Goalw [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)";
+by (simp_tac (simpset() addsimps [Collect_Un]) 1);
+qed "evnodd_Un";
+
+Goalw [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)";
+by (simp_tac (simpset() addsimps [Collect_Diff]) 1);
+qed "evnodd_Diff";
+
+Goalw [evnodd_def]
+    "evnodd(cons(<i,j>,C), b) = \
+\    (if (i#+j) mod 2 = b then cons(<i,j>, evnodd(C,b)) else evnodd(C,b))";
+by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1);
+qed "evnodd_cons";
+
+Goalw [evnodd_def] "evnodd(0, b) = 0";
+by (simp_tac (simpset() addsimps [evnodd_def]) 1);
+qed "evnodd_0";
+
+Addsimps [evnodd_cons, evnodd_0];
+
+(*** Dominoes ***)
+
+Goal "d \\<in> domino ==> Finite(d)";
+by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
+qed "domino_Finite";
+
+Goal "[| d \\<in> domino; b<2 |] ==> \\<exists>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 (ares_tac [add_type]));
+(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
+by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self]) 1
+	    THEN blast_tac (claset() addDs [ltD]) 1));
+qed "domino_singleton";
+
+
+(*** Tilings ***)
+
+(** The union of two disjoint tilings is a tiling **)
+
+Goal "t \\<in> tiling(A) ==> \
+\              u \\<in> tiling(A) --> t Int u = 0 --> t Un u \\<in> tiling(A)";
+by (etac tiling.induct 1);
+by (simp_tac (simpset() addsimps tiling.intrs) 1);
+by (asm_full_simp_tac (simpset() addsimps [Un_assoc,
+					  subset_empty_iff RS iff_sym]) 1);
+by (blast_tac (claset() addIs tiling.intrs) 1);
+qed_spec_mp "tiling_UnI";
+
+Goal "t \\<in> tiling(domino) ==> Finite(t)";
+by (eresolve_tac [tiling.induct] 1);
+by (rtac Finite_0 1);
+by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1);
+qed "tiling_domino_Finite";
+
+Goal "t \\<in> tiling(domino) ==> |evnodd(t,0)| = |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 Safe_tac;
+by (subgoal_tac "\\<forall>p b. p \\<in> evnodd(a,b) --> p\\<notin>evnodd(t,b)" 1);
+by (asm_simp_tac 
+    (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
+			 evnodd_subset RS subset_Finite,
+			 Finite_imp_cardinal_cons]) 1);
+by (blast_tac (claset() addSDs [evnodd_subset RS subsetD]
+                        addEs [equalityE]) 1);
+qed "tiling_domino_0_1";
+
+Goal "[| i \\<in> nat;  n \\<in> nat |] ==> {i} * (n #+ n) \\<in> tiling(domino)";
+by (induct_tac "n" 1);
+by (simp_tac (simpset() addsimps tiling.intrs) 1);
+by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
+by (resolve_tac tiling.intrs 1);
+by (assume_tac 2);
+by (rename_tac "n'" 1);
+by (subgoal_tac    (*seems the easiest way of turning one to the other*)
+    "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {<i,n'#+n'>, <i,succ(n'#+n')>}" 1);
+by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
+by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1);
+qed "dominoes_tile_row";
+
+Goal "[| m \\<in> nat;  n \\<in> nat |] ==> m * (n #+ n) \\<in> tiling(domino)";
+by (induct_tac "m" 1);
+by (simp_tac (simpset() addsimps tiling.intrs) 1);
+by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1);
+by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] 
+                    addEs [mem_irrefl]) 1);
+qed "dominoes_tile_matrix";
+
+Goal "[| x=y; x<y |] ==> P";
+by Auto_tac;
+qed "eq_lt_E";
+
+Goal "[| m \\<in> nat;  n \\<in> nat;                                 \
+\        t = (succ(m)#+succ(m))*(succ(n)#+succ(n));       \
+\        t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \
+\     ==> t' \\<notin> tiling(domino)";
+by (rtac notI 1);
+by (dtac tiling_domino_0_1 1);
+by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1);
+by (subgoal_tac "t \\<in> tiling(domino)" 1);
+(*Requires a small simpset that won't move the succ applications*)
+by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, 
+                                  dominoes_tile_matrix]) 2);
+by (asm_full_simp_tac 
+    (simpset() addsimps [evnodd_Diff, mod2_add_self,
+                        mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
+by (rtac lt_trans 1);
+by (REPEAT
+    (rtac Finite_imp_cardinal_Diff 1 
+     THEN
+     asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, 
+                                      Finite_Diff]) 1 
+     THEN
+     asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, 
+                                      mod2_add_self]) 1));
+qed "mutil_not_tiling";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Mutil.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,36 @@
+(*  Title:      ZF/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 = Main +
+consts
+  domino  :: i
+  tiling  :: i=>i
+
+inductive
+  domains "domino" <= "Pow(nat*nat)"
+  intrs
+    horiz  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <i,succ(j)>} \\<in> domino"
+    vertl  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <succ(i),j>} \\<in> domino"
+  type_intrs  empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
+
+
+inductive
+    domains "tiling(A)" <= "Pow(Union(A))"
+  intrs
+    empty  "0 \\<in> tiling(A)"
+    Un     "[| a \\<in> A;  t \\<in> tiling(A);  a Int t = 0 |] ==> a Un t \\<in> tiling(A)"
+  type_intrs  empty_subsetI, Union_upper, Un_least, PowI
+  type_elims "[make_elim PowD]"
+
+constdefs
+  evnodd  :: [i,i]=>i
+  "evnodd(A,b) == {z \\<in> A. \\<exists>i j. z=<i,j> & (i#+j) mod 2 = b}"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Primrec.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,297 @@
+(*  Title:      ZF/ex/Primrec
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz, 
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
+*)
+
+(*** Inductive definition of the PR functions ***)
+
+(* c \\<in> prim_rec ==> c \\<in> list(nat) -> nat *)
+val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
+
+AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
+
+Goal "i \\<in> nat ==> ACK(i): prim_rec";
+by (induct_tac "i" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "ACK_in_prim_rec";
+
+AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
+	list_add_type, nat_into_Ord, rec_type];
+
+Goal "[| i \\<in> nat;  j \\<in> nat |] ==>  ack(i,j): nat";
+by Auto_tac;
+qed "ack_type";
+AddTCs [ack_type];
+
+(** Ackermann's function cases **)
+
+(*PROPERTY A 1*)
+Goal "j \\<in> nat ==> ack(0,j) = succ(j)";
+by (asm_simp_tac (simpset() addsimps [SC]) 1);
+qed "ack_0";
+
+(*PROPERTY A 2*)
+Goal "ack(succ(i), 0) = ack(i,1)";
+by (asm_simp_tac (simpset() addsimps [CONST,PREC_0]) 1);
+qed "ack_succ_0";
+
+(*PROPERTY A 3*)
+Goal "[| i \\<in> nat;  j \\<in> nat |]  \
+\     ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
+by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
+qed "ack_succ_succ";
+
+Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type];
+Delsimps [ACK_0, ACK_succ];
+
+
+(*PROPERTY A 4*)
+Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. j < ack(i,j)";
+by (induct_tac "i" 1);
+by (Asm_simp_tac 1);
+by (rtac ballI 1);
+by (induct_tac "j" 1);
+by (etac (succ_leI RS lt_trans1) 2);
+by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
+by Auto_tac;
+qed_spec_mp "lt_ack2";
+
+(*PROPERTY A 5-, the single-step lemma*)
+Goal "[| i \\<in> nat; j \\<in> nat |] ==> ack(i,j) < ack(i, succ(j))";
+by (induct_tac "i" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2])));
+qed "ack_lt_ack_succ2";
+
+(*PROPERTY A 5, monotonicity for < *)
+Goal "[| j<k; i \\<in> nat; k \\<in> nat |] ==> ack(i,j) < ack(i,k)";
+by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
+by (etac succ_lt_induct 1);
+by (assume_tac 1);
+by (rtac lt_trans 2);
+by (auto_tac (claset() addIs [ack_lt_ack_succ2], simpset()));
+qed "ack_lt_mono2";
+
+(*PROPERTY A 5', monotonicity for le *)
+Goal "[| j le k;  i \\<in> nat;  k \\<in> nat |] ==> ack(i,j) le ack(i,k)";
+by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
+qed "ack_le_mono2";
+
+(*PROPERTY A 6*)
+Goal "[| i \\<in> nat;  j \\<in> nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
+by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac ack_le_mono2 1);
+by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
+by Auto_tac;
+qed "ack2_le_ack1";
+
+(*PROPERTY A 7-, the single-step lemma*)
+Goal "[| i \\<in> nat; j \\<in> nat |] ==> ack(i,j) < ack(succ(i),j)";
+by (rtac (ack_lt_mono2 RS lt_trans2) 1);
+by (rtac ack2_le_ack1 4);
+by Auto_tac;
+qed "ack_lt_ack_succ1";
+
+(*PROPERTY A 7, monotonicity for < *)
+Goal "[| i<j; j \\<in> nat; k \\<in> nat |] ==> ack(i,k) < ack(j,k)";
+by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
+by (etac succ_lt_induct 1);
+by (assume_tac 1);
+by (rtac lt_trans 2);
+by (auto_tac (claset() addIs [ack_lt_ack_succ1], simpset()));
+qed "ack_lt_mono1";
+
+(*PROPERTY A 7', monotonicity for le *)
+Goal "[| i le j; j \\<in> nat; k \\<in> nat |] ==> ack(i,k) le ack(j,k)";
+by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
+qed "ack_le_mono1";
+
+(*PROPERTY A 8*)
+Goal "j \\<in> nat ==> ack(1,j) = succ(succ(j))";
+by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "ack_1";
+
+(*PROPERTY A 9*)
+Goal "j \\<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
+by (induct_tac "j" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right])));
+qed "ack_2";
+
+(*PROPERTY A 10*)
+Goal "[| i1 \\<in> nat; i2 \\<in> nat; j \\<in> nat |] ==> \
+\               ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
+by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
+by (Asm_simp_tac 1);
+by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
+by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 4);
+by Auto_tac;
+qed "ack_nest_bound";
+
+(*PROPERTY A 11*)
+Goal "[| i1 \\<in> nat; i2 \\<in> nat; j \\<in> nat |] ==> \
+\          ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
+by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
+by (asm_simp_tac (simpset() addsimps [ack_2]) 1);
+by (rtac (ack_nest_bound RS lt_trans2) 2);
+by (Asm_simp_tac 5);
+by (rtac (add_le_mono RS leI RS leI) 1);
+by (auto_tac (claset() addIs [add_le_self, add_le_self2, ack_le_mono1], 
+	      simpset()));
+qed "ack_add_bound";
+
+(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
+  used k#+4.  Quantified version must be nested \\<exists>k'. \\<forall>i,j... *)
+Goal "[| i < ack(k,j);  j \\<in> nat;  k \\<in> nat |] ==> \
+\             i#+j < ack(succ(succ(succ(succ(k)))), j)";
+by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
+by (rtac (ack_add_bound RS lt_trans2) 2);
+by (rtac add_lt_mono 1);
+by Auto_tac;
+qed "ack_add_bound2";
+
+(*** MAIN RESULT ***)
+
+Addsimps [list_add_type];
+
+Goalw [SC_def] "l \\<in> list(nat) ==> SC ` l < ack(1, list_add(l))";
+by (exhaust_tac "l" 1);
+by (asm_simp_tac (simpset() addsimps [succ_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1);
+qed "SC_case";
+
+(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
+Goal "[| i \\<in> nat; j \\<in> nat |] ==> i < ack(i,j)";
+by (induct_tac "i" 1);
+by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
+by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
+by Auto_tac;
+qed "lt_ack1";
+
+Goalw [CONST_def]
+    "[| l \\<in> list(nat);  k \\<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
+by (asm_simp_tac (simpset() addsimps [lt_ack1]) 1);
+qed "CONST_case";
+
+Goalw [PROJ_def]
+    "l \\<in> list(nat) ==> \\<forall>i \\<in> nat. PROJ(i) ` l < ack(0, list_add(l))";
+by (Asm_simp_tac 1);
+by (etac list.induct 1);
+by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
+by (Asm_simp_tac 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","x")] natE 1);
+by (asm_simp_tac (simpset() addsimps [add_le_self]) 1);
+by (Asm_simp_tac 1);
+by (etac (bspec RS lt_trans2) 1);
+by (rtac (add_le_self2 RS succ_leI) 2);
+by Auto_tac;
+qed_spec_mp "PROJ_case";
+
+(** COMP case **)
+
+Goal "fs \\<in> list({f \\<in> prim_rec .                                 \
+\                  \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat).                  \
+\                             f`l < ack(kf, list_add(l))})      \
+\      ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat).                          \
+\                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
+by (etac list.induct 1);
+by (res_inst_tac [("x","0")] bexI 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le])));
+by (Clarify_tac 1);
+by (rtac (ballI RS bexI) 1);
+by (rtac (add_lt_mono RS lt_trans) 1);
+by (REPEAT (FIRSTGOAL (etac bspec)));
+by (rtac ack_add_bound 5);
+by Auto_tac;
+qed "COMP_map_lemma";
+
+Goalw [COMP_def]
+ "[| kg: nat;                                 \
+\         \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l));          \
+\         fs \\<in> list({f \\<in> prim_rec .                               \
+\                    \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat).                \
+\                       f`l < ack(kf, list_add(l))})            \
+\      |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
+by (Asm_simp_tac 1);
+by (ftac list_CollectD 1);
+by (etac (COMP_map_lemma RS bexE) 1);
+by (rtac (ballI RS bexI) 1);
+by (etac (bspec RS lt_trans) 1);
+by (rtac lt_trans 2);
+by (rtac ack_nest_bound 3);
+by (etac (bspec RS ack_lt_mono2) 2);
+by Auto_tac;
+qed "COMP_case";
+
+(** PREC case **)
+
+Goalw [PREC_def]
+ "[| \\<forall>l \\<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
+\           \\<forall>l \\<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
+\           f \\<in> prim_rec;  kf: nat;                                       \
+\           g \\<in> prim_rec;  kg: nat;                                       \
+\           l \\<in> list(nat)                                                \
+\        |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
+by (exhaust_tac "l" 1);
+by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
+by (Asm_simp_tac 1);
+by (etac ssubst 1);  (*get rid of the needless assumption*)
+by (induct_tac "a" 1);
+(*base case*)
+by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
+	    assume_tac, rtac (add_le_self RS ack_lt_mono1)]);
+by (ALLGOALS Asm_simp_tac);
+(*ind step*)
+by (rtac (succ_leI RS lt_trans1) 1);
+by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
+by (etac bspec 2);
+by (rtac (nat_le_refl RS add_le_mono) 1);
+by Typecheck_tac;
+by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
+(*final part of the simplification*)
+by (Asm_simp_tac 1);
+by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
+by (etac ack_lt_mono2 4);
+by Auto_tac;
+qed "PREC_case_lemma";
+
+Goal "[| f \\<in> prim_rec;  kf: nat;                               \
+\        g \\<in> prim_rec;  kg: nat;                               \
+\        \\<forall>l \\<in> list(nat). f`l < ack(kf, list_add(l));        \
+\        \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l))         \
+\     |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))";
+by (rtac (ballI RS bexI) 1);
+by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
+by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec));
+by Typecheck_tac;
+qed "PREC_case";
+
+Goal "f \\<in> prim_rec ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). f`l < ack(k, list_add(l))";
+by (etac prim_rec.induct 1);
+by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
+			      PREC_case], 
+	      simpset()));
+qed "ack_bounds_prim_rec";
+
+Goal "~ (\\<lambda>l \\<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \\<in> prim_rec";
+by (rtac notI 1);
+by (etac (ack_bounds_prim_rec RS bexE) 1);
+by (rtac lt_irrefl 1);
+by (dres_inst_tac [("x", "[x]")] bspec 1);
+by Auto_tac;
+qed "ack_not_prim_rec";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Primrec.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,35 @@
+(*  Title:      ZF/ex/Primrec.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Primitive Recursive Functions: the inductive definition
+
+Proof adopted from
+Nora Szasz, 
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
+*)
+
+Primrec = Primrec_defs +
+consts
+    prim_rec :: i
+
+inductive
+  domains "prim_rec" <= "list(nat)->nat"
+  intrs
+    SC       "SC \\<in> prim_rec"
+    CONST    "k \\<in> nat ==> CONST(k) \\<in> prim_rec"
+    PROJ     "i \\<in> nat ==> PROJ(i) \\<in> prim_rec"
+    COMP     "[| g \\<in> prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
+    PREC     "[| f \\<in> prim_rec; g \\<in> prim_rec |] ==> PREC(f,g): prim_rec"
+  monos       list_mono
+  con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
+  type_intrs "nat_typechecks @ list.intrs @                     
+              [lam_type, list_case_type, drop_type, map_type,   
+              apply_type, rec_type]"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Primrec_defs.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,40 @@
+(*  Title:      ZF/ex/Primrec
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Primitive Recursive Functions: preliminary definitions
+*)
+
+(*Theory TF redeclares map_type*)
+val map_type = thm "List.map_type";
+
+(** Useful special cases of evaluation ***)
+
+Goalw [SC_def] "[| x \\<in> nat;  l \\<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+by (Asm_simp_tac 1);
+qed "SC";
+
+Goalw [CONST_def] "[| l \\<in> list(nat) |] ==> CONST(k) ` l = k";
+by (Asm_simp_tac 1);
+qed "CONST";
+
+Goalw [PROJ_def] "[| x \\<in> nat;  l \\<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+by (Asm_simp_tac 1);
+qed "PROJ_0";
+
+Goalw [COMP_def] "[| l \\<in> list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+by (Asm_simp_tac 1);
+qed "COMP_1";
+
+Goalw [PREC_def] "l \\<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+by (Asm_simp_tac 1);
+qed "PREC_0";
+
+Goalw [PREC_def]
+    "[| x \\<in> nat;  l \\<in> list(nat) |] ==>  \
+\         PREC(f,g) ` (Cons(succ(x),l)) = \
+\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
+by (Asm_simp_tac 1);
+qed "PREC_succ";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Primrec_defs.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,46 @@
+(*  Title:      ZF/ex/Primrec_defs.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Primitive Recursive Functions: preliminary definitions of the constructors
+
+[These must reside in a separate theory in order to be visible in the
+ con_defs part of prim_rec's inductive definition.]
+*)
+
+Primrec_defs = Main +
+
+consts
+    SC      :: i
+    CONST   :: i=>i
+    PROJ    :: i=>i
+    COMP    :: [i,i]=>i
+    PREC    :: [i,i]=>i
+    ACK     :: i=>i
+    ack     :: [i,i]=>i
+
+translations
+  "ack(x,y)"  == "ACK(x) ` [y]"
+
+defs
+
+  SC_def    "SC == \\<lambda>l \\<in> list(nat).list_case(0, %x xs. succ(x), l)"
+
+  CONST_def "CONST(k) == \\<lambda>l \\<in> list(nat).k"
+
+  PROJ_def  "PROJ(i) == \\<lambda>l \\<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
+
+  COMP_def  "COMP(g,fs) == \\<lambda>l \\<in> list(nat). g ` List.map(%f. f`l, fs)"
+
+  (*Note that g is applied first to PREC(f,g)`y and then to y!*)
+  PREC_def  "PREC(f,g) == 
+            \\<lambda>l \\<in> list(nat). list_case(0, 
+                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+  
+primrec
+  ACK_0     "ACK(0) = SC"
+  ACK_succ  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
+				  COMP(ACK(i), [PROJ(0)]))"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/PropLog.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,249 @@
+(*  Title:      ZF/ex/prop-log.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow & Lawrence C Paulson
+    Copyright   1992  University of Cambridge
+
+Inductive definition of propositional logic.
+Soundness and completeness w.r.t. truth-tables.
+
+Prove: If H|=p then G|=p where G \\<in> Fin(H)
+*)
+
+Addsimps prop.intrs;
+
+(*** Semantics of propositional logic ***)
+
+(** The function is_true **)
+
+Goalw [is_true_def] "is_true(Fls,t) <-> False";
+by (Simp_tac 1);
+qed "is_true_Fls";
+
+Goalw [is_true_def] "is_true(#v,t) <-> v \\<in> t";
+by (Simp_tac 1);
+qed "is_true_Var";
+
+Goalw [is_true_def] "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
+by (Simp_tac 1);
+qed "is_true_Imp";
+
+Addsimps [is_true_Fls, is_true_Var, is_true_Imp];
+
+
+(*** Proof theory of propositional logic ***)
+
+Goalw thms.defs "G \\<subseteq> H ==> thms(G) \\<subseteq> thms(H)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac thms.bnd_mono 1));
+by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
+qed "thms_mono";
+
+val thms_in_pl = thms.dom_subset RS subsetD;
+
+val ImpE = prop.mk_cases "p=>q \\<in> prop";
+
+(*Stronger Modus Ponens rule: no typechecking!*)
+Goal "[| H |- p=>q;  H |- p |] ==> H |- q";
+by (rtac thms.MP 1);
+by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1));
+qed "thms_MP";
+
+(*Rule is called I for Identity Combinator, not for Introduction*)
+Goal "p \\<in> prop ==> H |- p=>p";
+by (rtac (thms.S RS thms_MP RS thms_MP) 1);
+by (rtac thms.K 5);
+by (rtac thms.K 4);
+by (REPEAT (ares_tac prop.intrs 1));
+qed "thms_I";
+
+(** Weakening, left and right **)
+
+(* [| G \\<subseteq> H;  G|-p |] ==> H|-p   Order of premises is convenient with RS*)
+bind_thm ("weaken_left", (thms_mono RS subsetD));
+
+(* H |- p ==> cons(a,H) |- p *)
+val weaken_left_cons = subset_consI RS weaken_left;
+
+val weaken_left_Un1  = Un_upper1 RS weaken_left;
+val weaken_left_Un2  = Un_upper2 RS weaken_left;
+
+Goal "[| H |- q;  p \\<in> prop |] ==> H |- p=>q";
+by (rtac (thms.K RS thms_MP) 1);
+by (REPEAT (ares_tac [thms_in_pl] 1));
+qed "weaken_right";
+
+(*The deduction theorem*)
+Goal "[| cons(p,H) |- q;  p \\<in> prop |] ==>  H |- p=>q";
+by (etac thms.induct 1);
+by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.S RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.DN RS weaken_right]) 1);
+by (blast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1);
+qed "deduction";
+
+
+(*The cut rule*)
+Goal "[| H|-p;  cons(p,H) |- q |] ==>  H |- q";
+by (rtac (deduction RS thms_MP) 1);
+by (REPEAT (ares_tac [thms_in_pl] 1));
+qed "cut";
+
+Goal "[| H |- Fls; p \\<in> prop |] ==> H |- p";
+by (rtac (thms.DN RS thms_MP) 1);
+by (rtac weaken_right 2);
+by (REPEAT (ares_tac (prop.intrs@[consI1]) 1));
+qed "thms_FlsE";
+
+(* [| H |- p=>Fls;  H |- p;  q \\<in> prop |] ==> H |- q *)
+bind_thm ("thms_notE", (thms_MP RS thms_FlsE));
+
+(*Soundness of the rules wrt truth-table semantics*)
+Goalw [logcon_def] "H |- p ==> H |= p";
+by (etac thms.induct 1);
+by Auto_tac;
+qed "soundness";
+
+(*** Towards the completeness proof ***)
+
+val [premf,premq] = goal PropLog.thy
+    "[| H |- p=>Fls; q \\<in> prop |] ==> H |- p=>q";
+by (rtac (premf RS thms_in_pl RS ImpE) 1);
+by (rtac deduction 1);
+by (rtac (premf RS weaken_left_cons RS thms_notE) 1);
+by (REPEAT (ares_tac [premq, consI1, thms.H] 1));
+qed "Fls_Imp";
+
+val [premp,premq] = goal PropLog.thy
+    "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls";
+by (cut_facts_tac ([premp,premq] RL [thms_in_pl]) 1);
+by (etac ImpE 1);
+by (rtac deduction 1);
+by (rtac (premq RS weaken_left_cons RS thms_MP) 1);
+by (rtac (consI1 RS thms.H RS thms_MP) 1);
+by (rtac (premp RS weaken_left_cons) 2);
+by (REPEAT (ares_tac prop.intrs 1));
+qed "Imp_Fls";
+
+(*Typical example of strengthening the induction formula*)
+Goal "p \\<in> prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)";
+by (Simp_tac 1);
+by (induct_tac "p" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
+by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, 
+			       Fls_Imp RS weaken_left_Un2]));
+by (ALLGOALS (blast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
+					weaken_right, Imp_Fls])));
+qed "hyps_thms_if";
+
+(*Key lemma for completeness; yields a set of assumptions satisfying p*)
+Goalw [logcon_def] "[| p \\<in> prop;  0 |= p |] ==> hyps(p,t) |- p";
+by (dtac hyps_thms_if 1);
+by (Asm_full_simp_tac 1);
+qed "logcon_thms_p";
+
+(*For proving certain theorems in our new propositional logic*)
+val thms_cs = 
+    ZF_cs addSIs (prop.intrs @ [deduction])
+          addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
+
+(*The excluded middle in the form of an elimination rule*)
+Goal "[| p \\<in> prop;  q \\<in> prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
+by (rtac (deduction RS deduction) 1);
+by (rtac (thms.DN RS thms_MP) 1);
+by (ALLGOALS (blast_tac thms_cs));
+qed "thms_excluded_middle";
+
+(*Hard to prove directly because it requires cuts*)
+Goal "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \\<in> prop |] ==> H |- q";
+by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
+by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
+qed "thms_excluded_middle_rule";
+
+(*** Completeness -- lemmas for reducing the set of assumptions ***)
+
+(*For the case hyps(p,t)-cons(#v,Y) |- p;
+  we also have hyps(p,t)-{#v} \\<subseteq> hyps(p, t-{v}) *)
+Goal "p \\<in> prop ==> hyps(p, t-{v}) \\<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})";
+by (induct_tac "p" 1);
+by Auto_tac;
+qed "hyps_Diff";
+
+(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
+  we also have hyps(p,t)-{#v=>Fls} \\<subseteq> hyps(p, cons(v,t)) *)
+Goal "p \\<in> prop ==> hyps(p, cons(v,t)) \\<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})";
+by (induct_tac "p" 1);
+by Auto_tac;
+qed "hyps_cons";
+
+(** Two lemmas for use with weaken_left **)
+
+Goal "B-C \\<subseteq> cons(a, B-cons(a,C))";
+by (Fast_tac 1);
+qed "cons_Diff_same";
+
+Goal "cons(a, B-{c}) - D \\<subseteq> cons(a, B-cons(c,D))";
+by (Fast_tac 1);
+qed "cons_Diff_subset2";
+
+(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
+ could probably prove the stronger hyps(p,t) \\<in> Fin(hyps(p,0) Un hyps(p,nat))*)
+Goal "p \\<in> prop ==> hyps(p,t) \\<in> Fin(\\<Union>v \\<in> nat. {#v, #v=>Fls})";
+by (induct_tac "p" 1);
+by Auto_tac;  
+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 [premp,sat] = goal PropLog.thy
+    "[| p \\<in> prop;  0 |= p |] ==> \\<forall>t. hyps(p,t) - hyps(p,t0) |- p";
+by (rtac (premp RS hyps_finite RS Fin_induct) 1);
+by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
+by Safe_tac;
+(*Case hyps(p,t)-cons(#v,Y) |- p *)
+by (rtac thms_excluded_middle_rule 1);
+by (etac prop.Var_I 3);
+by (rtac (cons_Diff_same RS weaken_left) 1);
+by (etac spec 1);
+by (rtac (cons_Diff_subset2 RS weaken_left) 1);
+by (rtac (premp RS hyps_Diff RS Diff_weaken_left) 1);
+by (etac spec 1);
+(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
+by (rtac thms_excluded_middle_rule 1);
+by (etac prop.Var_I 3);
+by (rtac (cons_Diff_same RS weaken_left) 2);
+by (etac spec 2);
+by (rtac (cons_Diff_subset2 RS weaken_left) 1);
+by (rtac (premp RS hyps_cons RS Diff_weaken_left) 1);
+by (etac spec 1);
+qed "completeness_0_lemma";
+
+(*The base case for completeness*)
+val [premp,sat] = goal PropLog.thy "[| p \\<in> prop;  0 |= p |] ==> 0 |- p";
+by (rtac (Diff_cancel RS subst) 1);
+by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1);
+qed "completeness_0";
+
+(*A semantic analogue of the Deduction Theorem*)
+Goalw [logcon_def] "[| cons(p,H) |= q |] ==> H |= p=>q";
+by Auto_tac;
+qed "logcon_Imp";
+
+Goal "H \\<in> Fin(prop) ==> \\<forall>p \\<in> prop. H |= p --> H |- p";
+by (etac Fin_induct 1);
+by (safe_tac (claset() addSIs [completeness_0]));
+by (rtac (weaken_left_cons RS thms_MP) 1);
+by (blast_tac (claset() addSIs (logcon_Imp::prop.intrs)) 1);
+by (blast_tac thms_cs 1);
+qed "completeness_lemma";
+
+val completeness = completeness_lemma RS bspec RS mp;
+
+val [finite] = goal PropLog.thy "H \\<in> Fin(prop) ==> H |- p <-> H |= p & p \\<in> prop";
+by (fast_tac (claset() addSEs [soundness, finite RS completeness, 
+			       thms_in_pl]) 1);
+qed "thms_iff";
+
+writeln"Reached end of file.";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/PropLog.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,68 @@
+(*  Title:      ZF/ex/PropLog.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Lawrence C Paulson
+    Copyright   1993  University of Cambridge
+
+Datatype definition of propositional logic formulae and inductive definition
+of the propositional tautologies.
+*)
+
+PropLog = Main +
+
+(** The datatype of propositions; note mixfix syntax **)
+consts
+  prop     :: i
+
+datatype
+  "prop" = Fls
+         | Var ("n \\<in> nat")                       ("#_" [100] 100)
+         | "=>" ("p \\<in> prop", "q \\<in> prop")          (infixr 90)
+
+(** The proof system **)
+consts
+  thms     :: i => i
+
+syntax
+  "|-"     :: [i,i] => o                        (infixl 50)
+
+translations
+  "H |- p" == "p \\<in> thms(H)"
+
+inductive
+  domains "thms(H)" <= "prop"
+  intrs
+    H  "[| p \\<in> H;  p \\<in> prop |] ==> H |- p"
+    K  "[| p \\<in> prop;  q \\<in> prop |] ==> H |- p=>q=>p"
+    S  "[| p \\<in> prop;  q \\<in> prop;  r \\<in> prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
+    DN "p \\<in> prop ==> H |- ((p=>Fls) => Fls) => p"
+    MP "[| H |- p=>q;  H |- p;  p \\<in> prop;  q \\<in> prop |] ==> H |- q"
+  type_intrs "prop.intrs"
+
+
+(** The semantics **)
+consts
+  "|="        :: [i,i] => o                        (infixl 50)
+  hyps        :: [i,i] => i
+  is_true_fun :: [i,i] => i
+
+constdefs (*this definitionis necessary since predicates can't be recursive*)
+  is_true     :: [i,i] => o
+    "is_true(p,t) == is_true_fun(p,t)=1"
+
+defs
+  (*Logical consequence: for every valuation, if all elements of H are true
+     then so is p*)
+  logcon_def  "H |= p == \\<forall>t. (\\<forall>q \\<in> H. is_true(q,t)) --> is_true(p,t)"
+
+primrec (** A finite set of hypotheses from t and the Vars in p **)
+  "hyps(Fls, t)    = 0"
+  "hyps(Var(v), t) = (if v \\<in> t then {#v} else {#v=>Fls})"
+  "hyps(p=>q, t)   = hyps(p,t) Un hyps(q,t)"
+ 
+primrec (** Semantics of propositional logic **)
+  "is_true_fun(Fls, t)    = 0"
+  "is_true_fun(Var(v), t) = (if v \\<in> t then 1 else 0)"
+  "is_true_fun(p=>q, t)   = (if is_true_fun(p,t)=1 then is_true_fun(q,t)
+			     else 1)"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Rmap.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,56 @@
+(*  Title:      ZF/ex/Rmap
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+Goalw rmap.defs "r \\<subseteq> s ==> rmap(r) \\<subseteq> rmap(s)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac rmap.bnd_mono 1));
+by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
+                      basic_monos) 1));
+qed "rmap_mono";
+
+val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> \\<in> rmap(r)"
+and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> \\<in> rmap(r)";
+
+AddIs  rmap.intrs;
+AddSEs [Nil_rmap_case, Cons_rmap_case];
+
+Goal "r \\<subseteq> A*B ==> rmap(r) \\<subseteq> list(A)*list(B)";
+by (rtac (rmap.dom_subset RS subset_trans) 1);
+by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
+                      Sigma_mono, list_mono] 1));
+qed "rmap_rel_type";
+
+Goal "A \\<subseteq> domain(r) ==> list(A) \\<subseteq> domain(rmap(r))";
+by (rtac subsetI 1);
+by (etac list.induct 1);
+by (ALLGOALS Fast_tac);
+qed "rmap_total";
+
+Goalw [function_def] "function(r) ==> function(rmap(r))";
+by (rtac (impI RS allI RS allI) 1);
+by (etac rmap.induct 1);
+by (ALLGOALS Fast_tac);
+qed "rmap_functional";
+
+
+(** If f is a function then rmap(f) behaves as expected. **)
+
+Goal "f \\<in> A->B ==> rmap(f): list(A)->list(B)";
+by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type,
+					   rmap_functional, rmap_total]) 1);
+qed "rmap_fun_type";
+
+Goalw [apply_def] "rmap(f)`Nil = Nil";
+by (Blast_tac 1);
+qed "rmap_Nil";
+
+Goal "[| f \\<in> A->B;  x \\<in> A;  xs: list(A) |]  \
+\     ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
+by (rtac apply_equality 1);
+by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
+qed "rmap_Cons";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Rmap.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,25 @@
+(*  Title:      ZF/ex/Rmap
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+Rmap = Main +
+
+consts
+  rmap :: i=>i
+
+inductive
+  domains "rmap(r)" <= "list(domain(r))*list(range(r))"
+  intrs
+    NilI  "<Nil,Nil> \\<in> rmap(r)"
+
+    ConsI "[| <x,y>: r;  <xs,ys> \\<in> rmap(r) |] ==> 
+          <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)"
+
+  type_intrs "[domainI,rangeI] @ list.intrs"
+
+end
+  

--- a/src/ZF/IsaMakefile	Wed Nov 07 00:16:19 2001 +0100
+++ b/src/ZF/IsaMakefile	Wed Nov 07 12:29:07 2001 +0100
@@ -10,7 +10,7 @@
 images: ZF
 
 #Note: keep targets sorted
-test: ZF-AC ZF-Coind ZF-ex ZF-IMP ZF-Resid ZF-UNITY
+test: ZF-AC ZF-Coind ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
 all: images test
 
 
@@ -84,24 +84,6 @@
 	@$(ISATOOL) usedir $(OUT)/ZF Coind
 
 
-## ZF-ex
-
-ZF-ex: ZF $(LOG)/ZF-ex.gz
-
-$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \
-  ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
-  ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \
-  ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \
-  ex/LList.ML ex/LList.thy \
-  ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
-  ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
-  ex/NatSum.ML ex/NatSum.thy  ex/Primrec_defs.ML ex/Primrec_defs.thy \
-  ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
-  ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
-  ex/Term.ML ex/Term.thy ex/misc.thy
-	@$(ISATOOL) usedir $(OUT)/ZF ex
-
-
 ## ZF-IMP
 
 ZF-IMP: ZF $(LOG)/ZF-IMP.gz
@@ -138,6 +120,34 @@
 	@$(ISATOOL) usedir $(OUT)/ZF UNITY
 
 
+## ZF-Induct
+
+ZF-Induct: ZF $(LOG)/ZF-Induct.gz
+
+$(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
+  Induct/Comb.ML Induct/Comb.thy \
+  Induct/ListN.ML Induct/ListN.thy  Induct/Mutil.ML Induct/Mutil.thy\
+  Induct/Primrec_defs.ML Induct/Primrec_defs.thy\
+  Induct/Primrec.ML Induct/Primrec.thy\
+  Induct/PropLog.ML Induct/PropLog.thy  Induct/Rmap.ML Induct/Rmap.thy
+	@$(ISATOOL) usedir $(OUT)/ZF Induct
+
+## ZF-ex
+
+ZF-ex: ZF $(LOG)/ZF-ex.gz
+
+$(LOG)/ZF-ex.gz: $(OUT)/ZF  ex/ROOT.ML ex/BT.ML ex/BT.thy \
+  ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
+  ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
+  ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \
+  ex/Limit.ML ex/Limit.thy  ex/LList.ML ex/LList.thy\
+  ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy\
+  ex/NatSum.ML ex/NatSum.thy \
+  ex/Ramsey.ML ex/Ramsey.thy  ex/TF.ML ex/TF.thy \
+  ex/Term.ML ex/Term.thy ex/misc.thy
+	@$(ISATOOL) usedir $(OUT)/ZF ex
+
+
 ## clean
 
 clean:

--- a/src/ZF/ex/Acc.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      ZF/ex/acc
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  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.
-*)
-
-(*The introduction rule must require  a \\<in> field(r)  
-  Otherwise acc(r) would be a proper class!    *)
-
-(*The intended introduction rule*)
-val prems = goal Acc.thy
-    "[| !!b. <b,a>:r ==> b \\<in> acc(r);  a \\<in> field(r) |] ==> a \\<in> acc(r)";
-by (fast_tac (claset() addIs [e-mail]) 1);
-qed "accI";
-
-Goal "[| b \\<in> acc(r);  <a,b>: r |] ==> a \\<in> acc(r)";
-by (etac acc.elim 1);
-by (Fast_tac 1);
-qed "acc_downward";
-
-val [major,indhyp] = goal Acc.thy
-    "[| a \\<in> acc(r);                                             \
-\       !!x. [| x \\<in> acc(r);  \\<forall>y. <y,x>:r --> P(y) |] ==> P(x) \
-\    |] ==> P(a)";
-by (rtac (major RS acc.induct) 1);
-by (rtac indhyp 1);
-by (Fast_tac 2);
-by (resolve_tac acc.intrs 1);
-by (assume_tac 2);
-by (etac (Collect_subset RS Pow_mono RS subsetD) 1);
-qed "acc_induct";
-
-Goal "wf[acc(r)](r)";
-by (rtac wf_onI2 1);
-by (etac acc_induct 1);
-by (Fast_tac 1);
-qed "wf_on_acc";
-
-(* field(r) \\<subseteq> acc(r) ==> wf(r) *)
-val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
-
-val [major] = goal Acc.thy "wf(r) ==> field(r) \\<subseteq> acc(r)";
-by (rtac subsetI 1);
-by (etac (major RS wf_induct2) 1);
-by (rtac subset_refl 1);
-by (rtac accI 1);
-by (assume_tac 2);
-by (Fast_tac 1);
-qed "acc_wfD";
-
-Goal "wf(r) <-> field(r) \\<subseteq> acc(r)";
-by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
-qed "wf_acc_iff";

--- a/src/ZF/ex/Acc.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      ZF/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 = Main +
-
-consts
-  acc :: i=>i
-
-inductive
-  domains "acc(r)" <= "field(r)"
-  intrs
-    vimage  "[| r-``{a}: Pow(acc(r)); a \\<in> field(r) |] ==> a \\<in> acc(r)"
-  monos      Pow_mono
-
-end

--- a/src/ZF/ex/Comb.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(*  Title:      ZF/ex/comb.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson
-    Copyright   1993  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
-*)
-
-(*** Transitive closure preserves the Church-Rosser property ***)
-
-Goalw [diamond_def]
-    "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
-\    \\<forall>y'. <x,y'>:r --> (\\<exists>z. <y',z>: r^+ & <y,z>: r)";
-by (etac trancl_induct 1);
-by (blast_tac (claset() addIs [r_into_trancl]) 1);
-by (slow_best_tac (claset() addSDs [spec RS mp]
-                           addIs  [r_into_trancl, trans_trancl RS transD]) 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 trancl_induct 1);
-by (ALLGOALS (*Seems to be a brittle, undirected search*)
-    (slow_best_tac (claset() addIs [r_into_trancl, trans_trancl RS transD]
-                            addEs [major RS diamond_strip_lemmaE])));
-qed "diamond_trancl";
-
-
-val [_,_,comb_Ap] = comb.intrs;
-val Ap_E = comb.mk_cases "p#q \\<in> comb";
-
-AddSIs comb.intrs;
-
-
-(*** Results about Contraction ***)
-
-(*For type checking: replaces a-1->b by a,b \\<in> comb *)
-val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
-val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
-val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
-
-Goal "field(contract) = comb";
-by (blast_tac (claset() addIs [contract.K] addSEs [contract_combE2]) 1);
-qed "field_contract_eq";
-
-bind_thm ("reduction_refl",
-    (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl));
-
-bind_thm ("rtrancl_into_rtrancl2",
-    (r_into_rtrancl RS (trans_rtrancl RS transD)));
-
-AddSIs [reduction_refl, contract.K, contract.S];
-
-val reduction_rls = [contract.K RS rtrancl_into_rtrancl2,
-                     contract.S RS rtrancl_into_rtrancl2,
-                     contract.Ap1 RS rtrancl_into_rtrancl2,
-                     contract.Ap2 RS rtrancl_into_rtrancl2];
-
-(*Example only: not used*)
-Goalw [I_def] "p \\<in> comb ==> I#p ---> p";
-by (blast_tac (claset() addIs reduction_rls) 1);
-qed "reduce_I";
-
-Goalw [I_def] "I \\<in> comb";
-by (Blast_tac 1);
-qed "comb_I";
-
-(** Non-contraction results **)
-
-(*Derive a case for each combinator constructor*)
-val K_contractE = contract.mk_cases "K -1-> r";
-val S_contractE = contract.mk_cases "S -1-> r";
-val Ap_contractE = contract.mk_cases "p#q -1-> r";
-
-AddIs  [contract.Ap1, contract.Ap2];
-AddSEs [K_contractE, S_contractE, Ap_contractE];
-
-Goalw [I_def] "I -1-> r ==> P";
-by Auto_tac;
-qed "I_contract_E";
-
-Goal "K#p -1-> r ==> (\\<exists>q. r = K#q & p -1-> q)";
-by Auto_tac;
-qed "K1_contractD";
-
-Goal "[| p ---> q;  r \\<in> comb |] ==> p#r ---> q#r";
-by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
-by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset() addIs reduction_rls) 1);
-by (etac (trans_rtrancl RS transD) 1);
-by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1);
-qed "Ap_reduce1";
-
-Goal "[| p ---> q;  r \\<in> comb |] ==> r#p ---> r#q";
-by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
-by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset() addIs reduction_rls) 1);
-by (etac (trans_rtrancl RS transD) 1);
-by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1);
-qed "Ap_reduce2";
-
-(** Counterexample to the diamond property for -1-> **)
-
-Goal "K#I#(I#I) -1-> I";
-by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
-qed "KIII_contract1";
-
-Goalw [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
-by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
-qed "KIII_contract2";
-
-Goal "K#I#((K#I)#(K#I)) -1-> I";
-by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
-qed "KIII_contract3";
-
-Goalw [diamond_def] "~ diamond(contract)";
-by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3]
-                       addSEs [I_contract_E]) 1);
-qed "not_diamond_contract";
-
-
-
-(*** Results about Parallel Contraction ***)
-
-(*For type checking: replaces a=1=>b by a,b \\<in> comb *)
-val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
-val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
-val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
-
-Goal "field(parcontract) = comb";
-by (blast_tac (claset() addIs [parcontract.K] 
-                      addSEs [parcontract_combE2]) 1);
-qed "field_parcontract_eq";
-
-(*Derive a case for each combinator constructor*)
-val K_parcontractE = parcontract.mk_cases "K =1=> r";
-val S_parcontractE = parcontract.mk_cases "S =1=> r";
-val Ap_parcontractE = parcontract.mk_cases "p#q =1=> r";
-
-AddIs  parcontract.intrs;
-AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE];
-
-(*** Basic properties of parallel contraction ***)
-
-Goal "K#p =1=> r ==> (\\<exists>p'. r = K#p' & p =1=> p')";
-by Auto_tac;
-qed "K1_parcontractD";
-AddSDs [K1_parcontractD];
-
-Goal "S#p =1=> r ==> (\\<exists>p'. r = S#p' & p =1=> p')";
-by Auto_tac;
-qed "S1_parcontractD";
-AddSDs [S1_parcontractD];
-
-Goal "S#p#q =1=> r ==> (\\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
-by Auto_tac;
-qed "S2_parcontractD";
-AddSDs [S2_parcontractD];
-
-(*Church-Rosser property for parallel contraction*)
-Goalw [diamond_def] "diamond(parcontract)";
-by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract.induct 1);
-by (ALLGOALS 
-    (blast_tac (claset() addSEs comb.free_SEs
-			 addIs [parcontract_combD2])));
-qed "diamond_parcontract";
-
-(*** Equivalence of p--->q and p===>q ***)
-
-Goal "p-1->q ==> p=1=>q";
-by (etac contract.induct 1);
-by Auto_tac;
-qed "contract_imp_parcontract";
-
-Goal "p--->q ==> p===>q";
-by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
-by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset() addIs [r_into_trancl]) 1);
-by (blast_tac (claset() addIs [contract_imp_parcontract, 
-			       r_into_trancl, trans_trancl RS transD]) 1);
-qed "reduce_imp_parreduce";
-
-
-Goal "p=1=>q ==> p--->q";
-by (etac parcontract.induct 1);
-by (blast_tac (claset() addIs reduction_rls) 1);
-by (blast_tac (claset() addIs reduction_rls) 1);
-by (blast_tac (claset() addIs reduction_rls) 1);
-by (blast_tac 
-    (claset() addIs [trans_rtrancl RS transD,
-		     Ap_reduce1, Ap_reduce2, parcontract_combD1,
-		     parcontract_combD2]) 1);
-qed "parcontract_imp_reduce";
-
-Goal "p===>q ==> p--->q";
-by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
-by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
-by (etac trancl_induct 1);
-by (etac parcontract_imp_reduce 1);
-by (etac (trans_rtrancl RS transD) 1);
-by (etac parcontract_imp_reduce 1);
-qed "parreduce_imp_reduce";
-
-Goal "p===>q <-> p--->q";
-by (blast_tac (claset() addIs [parreduce_imp_reduce, reduce_imp_parreduce]) 1);
-qed "parreduce_iff_reduce";
-
-writeln"Reached end of file.";

--- a/src/ZF/ex/Comb.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(*  Title:      ZF/ex/Comb.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson
-    Copyright   1994  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 = Main +
-
-(** Datatype definition of combinators S and K, with infixed application **)
-consts comb :: i
-datatype
-  "comb" = K
-         | S
-         | "#" ("p \\<in> comb", "q \\<in> comb")   (infixl 90)
-
-(** Inductive definition of contractions, -1->
-             and (multi-step) reductions, --->
-**)
-consts
-  contract  :: i
-  "-1->"    :: [i,i] => o                       (infixl 50)
-  "--->"    :: [i,i] => o                       (infixl 50)
-
-translations
-  "p -1-> q" == "<p,q> \\<in> contract"
-  "p ---> q" == "<p,q> \\<in> contract^*"
-
-inductive
-  domains   "contract" <= "comb*comb"
-  intrs
-    K     "[| p \\<in> comb;  q \\<in> comb |] ==> K#p#q -1-> p"
-    S     "[| p \\<in> comb;  q \\<in> comb;  r \\<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
-    Ap1   "[| p-1->q;  r \\<in> comb |] ==> p#r -1-> q#r"
-    Ap2   "[| p-1->q;  r \\<in> comb |] ==> r#p -1-> r#q"
-  type_intrs "comb.intrs"
-
-
-(** Inductive definition of parallel contractions, =1=>
-             and (multi-step) parallel reductions, ===>
-**)
-consts
-  parcontract :: i
-  "=1=>"    :: [i,i] => o                       (infixl 50)
-  "===>"    :: [i,i] => o                       (infixl 50)
-
-translations
-  "p =1=> q" == "<p,q> \\<in> parcontract"
-  "p ===> q" == "<p,q> \\<in> parcontract^+"
-
-inductive
-  domains   "parcontract" <= "comb*comb"
-  intrs
-    refl  "[| p \\<in> comb |] ==> p =1=> p"
-    K     "[| p \\<in> comb;  q \\<in> comb |] ==> K#p#q =1=> p"
-    S     "[| p \\<in> comb;  q \\<in> comb;  r \\<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
-    Ap    "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"
-  type_intrs "comb.intrs"
-
-
-(*Misc definitions*)
-constdefs
-  I :: i
-  "I == S#K#K"
-
-  diamond :: i => o
-  "diamond(r) == \\<forall>x y. <x,y>:r --> 
-                          (\\<forall>y'. <x,y'>:r --> 
-                                   (\\<exists>z. <y,z>:r & <y',z> \\<in> r))"
-
-end

--- a/src/ZF/ex/ListN.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*  Title:      ZF/ex/ListN
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Inductive definition of lists of n elements
-
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
-*)
-
-Goal "l \\<in> list(A) ==> <length(l),l> \\<in> listn(A)";
-by (etac list.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (ares_tac listn.intrs 1));
-qed "list_into_listn";
-
-Goal "<n,l> \\<in> listn(A) <-> l \\<in> list(A) & length(l)=n";
-by (rtac iffI 1);
-by (blast_tac (claset() addIs [list_into_listn]) 2);
-by (etac listn.induct 1);
-by Auto_tac;
-qed "listn_iff";
-
-Goal "listn(A)``{n} = {l \\<in> list(A). length(l)=n}";
-by (rtac equality_iffI 1);
-by (simp_tac (simpset() addsimps [listn_iff,separation,image_singleton_iff]) 1);
-qed "listn_image_eq";
-
-Goalw listn.defs "A \\<subseteq> B ==> listn(A) \\<subseteq> listn(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac listn.bnd_mono 1));
-by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
-qed "listn_mono";
-
-Goal "[| <n,l> \\<in> listn(A); <n',l'> \\<in> listn(A) |] ==> <n#+n', l@l'> \\<in> listn(A)";
-by (etac listn.induct 1);
-by (ftac (impOfSubs listn.dom_subset) 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs)));
-qed "listn_append";
-
-val Nil_listn_case  = listn.mk_cases "<i,Nil> \\<in> listn(A)"
-and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> \\<in> listn(A)";
-
-val zero_listn_case = listn.mk_cases "<0,l> \\<in> listn(A)"
-and succ_listn_case = listn.mk_cases "<succ(i),l> \\<in> listn(A)";

--- a/src/ZF/ex/ListN.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      ZF/ex/ListN
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Inductive definition of lists of n elements
-
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
-*)
-
-ListN = Main +
-
-consts  listn ::i=>i
-inductive
-  domains   "listn(A)" <= "nat*list(A)"
-  intrs
-    NilI  "<0,Nil> \\<in> listn(A)"
-    ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)"
-  type_intrs "nat_typechecks @ list.intrs"
-
-end

--- a/src/ZF/ex/Mutil.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-(*  Title:      ZF/ex/Mutil
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-The Mutilated Checkerboard Problem, formalized inductively
-*)
-
-open Mutil;
-
-
-(** Basic properties of evnodd **)
-
-Goalw [evnodd_def] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b";
-by (Blast_tac 1);
-qed "evnodd_iff";
-
-Goalw [evnodd_def] "evnodd(A, b) \\<subseteq> A";
-by (Blast_tac 1);
-qed "evnodd_subset";
-
-(* Finite(X) ==> Finite(evnodd(X,b)) *)
-bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite);
-
-Goalw [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)";
-by (simp_tac (simpset() addsimps [Collect_Un]) 1);
-qed "evnodd_Un";
-
-Goalw [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)";
-by (simp_tac (simpset() addsimps [Collect_Diff]) 1);
-qed "evnodd_Diff";
-
-Goalw [evnodd_def]
-    "evnodd(cons(<i,j>,C), b) = \
-\    (if (i#+j) mod 2 = b then cons(<i,j>, evnodd(C,b)) else evnodd(C,b))";
-by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1);
-qed "evnodd_cons";
-
-Goalw [evnodd_def] "evnodd(0, b) = 0";
-by (simp_tac (simpset() addsimps [evnodd_def]) 1);
-qed "evnodd_0";
-
-Addsimps [evnodd_cons, evnodd_0];
-
-(*** Dominoes ***)
-
-Goal "d \\<in> domino ==> Finite(d)";
-by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
-qed "domino_Finite";
-
-Goal "[| d \\<in> domino; b<2 |] ==> \\<exists>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 (ares_tac [add_type]));
-(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self]) 1
-	    THEN blast_tac (claset() addDs [ltD]) 1));
-qed "domino_singleton";
-
-
-(*** Tilings ***)
-
-(** The union of two disjoint tilings is a tiling **)
-
-Goal "t \\<in> tiling(A) ==> \
-\              u \\<in> tiling(A) --> t Int u = 0 --> t Un u \\<in> tiling(A)";
-by (etac tiling.induct 1);
-by (simp_tac (simpset() addsimps tiling.intrs) 1);
-by (asm_full_simp_tac (simpset() addsimps [Un_assoc,
-					  subset_empty_iff RS iff_sym]) 1);
-by (blast_tac (claset() addIs tiling.intrs) 1);
-qed_spec_mp "tiling_UnI";
-
-Goal "t \\<in> tiling(domino) ==> Finite(t)";
-by (eresolve_tac [tiling.induct] 1);
-by (rtac Finite_0 1);
-by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1);
-qed "tiling_domino_Finite";
-
-Goal "t \\<in> tiling(domino) ==> |evnodd(t,0)| = |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 Safe_tac;
-by (subgoal_tac "\\<forall>p b. p \\<in> evnodd(a,b) --> p\\<notin>evnodd(t,b)" 1);
-by (asm_simp_tac 
-    (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
-			 evnodd_subset RS subset_Finite,
-			 Finite_imp_cardinal_cons]) 1);
-by (blast_tac (claset() addSDs [evnodd_subset RS subsetD]
-                        addEs [equalityE]) 1);
-qed "tiling_domino_0_1";
-
-Goal "[| i \\<in> nat;  n \\<in> nat |] ==> {i} * (n #+ n) \\<in> tiling(domino)";
-by (induct_tac "n" 1);
-by (simp_tac (simpset() addsimps tiling.intrs) 1);
-by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
-by (resolve_tac tiling.intrs 1);
-by (assume_tac 2);
-by (rename_tac "n'" 1);
-by (subgoal_tac    (*seems the easiest way of turning one to the other*)
-    "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {<i,n'#+n'>, <i,succ(n'#+n')>}" 1);
-by (Blast_tac 2);
-by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
-by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1);
-qed "dominoes_tile_row";
-
-Goal "[| m \\<in> nat;  n \\<in> nat |] ==> m * (n #+ n) \\<in> tiling(domino)";
-by (induct_tac "m" 1);
-by (simp_tac (simpset() addsimps tiling.intrs) 1);
-by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1);
-by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] 
-                    addEs [mem_irrefl]) 1);
-qed "dominoes_tile_matrix";
-
-Goal "[| x=y; x<y |] ==> P";
-by Auto_tac;
-qed "eq_lt_E";
-
-Goal "[| m \\<in> nat;  n \\<in> nat;                                 \
-\        t = (succ(m)#+succ(m))*(succ(n)#+succ(n));       \
-\        t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \
-\     ==> t' \\<notin> tiling(domino)";
-by (rtac notI 1);
-by (dtac tiling_domino_0_1 1);
-by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1);
-by (subgoal_tac "t \\<in> tiling(domino)" 1);
-(*Requires a small simpset that won't move the succ applications*)
-by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, 
-                                  dominoes_tile_matrix]) 2);
-by (asm_full_simp_tac 
-    (simpset() addsimps [evnodd_Diff, mod2_add_self,
-                        mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
-by (rtac lt_trans 1);
-by (REPEAT
-    (rtac Finite_imp_cardinal_Diff 1 
-     THEN
-     asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, 
-                                      Finite_Diff]) 1 
-     THEN
-     asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, 
-                                      mod2_add_self]) 1));
-qed "mutil_not_tiling";

--- a/src/ZF/ex/Mutil.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      ZF/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 = Main +
-consts
-  domino  :: i
-  tiling  :: i=>i
-
-inductive
-  domains "domino" <= "Pow(nat*nat)"
-  intrs
-    horiz  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <i,succ(j)>} \\<in> domino"
-    vertl  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <succ(i),j>} \\<in> domino"
-  type_intrs  empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
-
-
-inductive
-    domains "tiling(A)" <= "Pow(Union(A))"
-  intrs
-    empty  "0 \\<in> tiling(A)"
-    Un     "[| a \\<in> A;  t \\<in> tiling(A);  a Int t = 0 |] ==> a Un t \\<in> tiling(A)"
-  type_intrs  empty_subsetI, Union_upper, Un_least, PowI
-  type_elims "[make_elim PowD]"
-
-constdefs
-  evnodd  :: [i,i]=>i
-  "evnodd(A,b) == {z \\<in> A. \\<exists>i j. z=<i,j> & (i#+j) mod 2 = b}"
-
-end

--- a/src/ZF/ex/Primrec.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,297 +0,0 @@
-(*  Title:      ZF/ex/Primrec
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Primitive Recursive Functions
-
-Proof adopted from
-Nora Szasz, 
-A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
-In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
-
-See also E. Mendelson, Introduction to Mathematical Logic.
-(Van Nostrand, 1964), page 250, exercise 11.
-*)
-
-(*** Inductive definition of the PR functions ***)
-
-(* c \\<in> prim_rec ==> c \\<in> list(nat) -> nat *)
-val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
-
-AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
-
-Goal "i \\<in> nat ==> ACK(i): prim_rec";
-by (induct_tac "i" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "ACK_in_prim_rec";
-
-AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
-	list_add_type, nat_into_Ord, rec_type];
-
-Goal "[| i \\<in> nat;  j \\<in> nat |] ==>  ack(i,j): nat";
-by Auto_tac;
-qed "ack_type";
-AddTCs [ack_type];
-
-(** Ackermann's function cases **)
-
-(*PROPERTY A 1*)
-Goal "j \\<in> nat ==> ack(0,j) = succ(j)";
-by (asm_simp_tac (simpset() addsimps [SC]) 1);
-qed "ack_0";
-
-(*PROPERTY A 2*)
-Goal "ack(succ(i), 0) = ack(i,1)";
-by (asm_simp_tac (simpset() addsimps [CONST,PREC_0]) 1);
-qed "ack_succ_0";
-
-(*PROPERTY A 3*)
-Goal "[| i \\<in> nat;  j \\<in> nat |]  \
-\     ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
-by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
-qed "ack_succ_succ";
-
-Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type];
-Delsimps [ACK_0, ACK_succ];
-
-
-(*PROPERTY A 4*)
-Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. j < ack(i,j)";
-by (induct_tac "i" 1);
-by (Asm_simp_tac 1);
-by (rtac ballI 1);
-by (induct_tac "j" 1);
-by (etac (succ_leI RS lt_trans1) 2);
-by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
-by Auto_tac;
-qed_spec_mp "lt_ack2";
-
-(*PROPERTY A 5-, the single-step lemma*)
-Goal "[| i \\<in> nat; j \\<in> nat |] ==> ack(i,j) < ack(i, succ(j))";
-by (induct_tac "i" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2])));
-qed "ack_lt_ack_succ2";
-
-(*PROPERTY A 5, monotonicity for < *)
-Goal "[| j<k; i \\<in> nat; k \\<in> nat |] ==> ack(i,j) < ack(i,k)";
-by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
-by (etac succ_lt_induct 1);
-by (assume_tac 1);
-by (rtac lt_trans 2);
-by (auto_tac (claset() addIs [ack_lt_ack_succ2], simpset()));
-qed "ack_lt_mono2";
-
-(*PROPERTY A 5', monotonicity for le *)
-Goal "[| j le k;  i \\<in> nat;  k \\<in> nat |] ==> ack(i,j) le ack(i,k)";
-by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
-by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
-qed "ack_le_mono2";
-
-(*PROPERTY A 6*)
-Goal "[| i \\<in> nat;  j \\<in> nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
-by (induct_tac "j" 1);
-by (ALLGOALS Asm_simp_tac);
-by (rtac ack_le_mono2 1);
-by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
-by Auto_tac;
-qed "ack2_le_ack1";
-
-(*PROPERTY A 7-, the single-step lemma*)
-Goal "[| i \\<in> nat; j \\<in> nat |] ==> ack(i,j) < ack(succ(i),j)";
-by (rtac (ack_lt_mono2 RS lt_trans2) 1);
-by (rtac ack2_le_ack1 4);
-by Auto_tac;
-qed "ack_lt_ack_succ1";
-
-(*PROPERTY A 7, monotonicity for < *)
-Goal "[| i<j; j \\<in> nat; k \\<in> nat |] ==> ack(i,k) < ack(j,k)";
-by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
-by (etac succ_lt_induct 1);
-by (assume_tac 1);
-by (rtac lt_trans 2);
-by (auto_tac (claset() addIs [ack_lt_ack_succ1], simpset()));
-qed "ack_lt_mono1";
-
-(*PROPERTY A 7', monotonicity for le *)
-Goal "[| i le j; j \\<in> nat; k \\<in> nat |] ==> ack(i,k) le ack(j,k)";
-by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
-by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
-qed "ack_le_mono1";
-
-(*PROPERTY A 8*)
-Goal "j \\<in> nat ==> ack(1,j) = succ(succ(j))";
-by (induct_tac "j" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "ack_1";
-
-(*PROPERTY A 9*)
-Goal "j \\<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
-by (induct_tac "j" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right])));
-qed "ack_2";
-
-(*PROPERTY A 10*)
-Goal "[| i1 \\<in> nat; i2 \\<in> nat; j \\<in> nat |] ==> \
-\               ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
-by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
-by (Asm_simp_tac 1);
-by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
-by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 4);
-by Auto_tac;
-qed "ack_nest_bound";
-
-(*PROPERTY A 11*)
-Goal "[| i1 \\<in> nat; i2 \\<in> nat; j \\<in> nat |] ==> \
-\          ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
-by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
-by (asm_simp_tac (simpset() addsimps [ack_2]) 1);
-by (rtac (ack_nest_bound RS lt_trans2) 2);
-by (Asm_simp_tac 5);
-by (rtac (add_le_mono RS leI RS leI) 1);
-by (auto_tac (claset() addIs [add_le_self, add_le_self2, ack_le_mono1], 
-	      simpset()));
-qed "ack_add_bound";
-
-(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
-  used k#+4.  Quantified version must be nested \\<exists>k'. \\<forall>i,j... *)
-Goal "[| i < ack(k,j);  j \\<in> nat;  k \\<in> nat |] ==> \
-\             i#+j < ack(succ(succ(succ(succ(k)))), j)";
-by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
-by (rtac (ack_add_bound RS lt_trans2) 2);
-by (rtac add_lt_mono 1);
-by Auto_tac;
-qed "ack_add_bound2";
-
-(*** MAIN RESULT ***)
-
-Addsimps [list_add_type];
-
-Goalw [SC_def] "l \\<in> list(nat) ==> SC ` l < ack(1, list_add(l))";
-by (exhaust_tac "l" 1);
-by (asm_simp_tac (simpset() addsimps [succ_iff]) 1);
-by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1);
-qed "SC_case";
-
-(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
-Goal "[| i \\<in> nat; j \\<in> nat |] ==> i < ack(i,j)";
-by (induct_tac "i" 1);
-by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
-by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
-by Auto_tac;
-qed "lt_ack1";
-
-Goalw [CONST_def]
-    "[| l \\<in> list(nat);  k \\<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
-by (asm_simp_tac (simpset() addsimps [lt_ack1]) 1);
-qed "CONST_case";
-
-Goalw [PROJ_def]
-    "l \\<in> list(nat) ==> \\<forall>i \\<in> nat. PROJ(i) ` l < ack(0, list_add(l))";
-by (Asm_simp_tac 1);
-by (etac list.induct 1);
-by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
-by (Asm_simp_tac 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("n","x")] natE 1);
-by (asm_simp_tac (simpset() addsimps [add_le_self]) 1);
-by (Asm_simp_tac 1);
-by (etac (bspec RS lt_trans2) 1);
-by (rtac (add_le_self2 RS succ_leI) 2);
-by Auto_tac;
-qed_spec_mp "PROJ_case";
-
-(** COMP case **)
-
-Goal "fs \\<in> list({f \\<in> prim_rec .                                 \
-\                  \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat).                  \
-\                             f`l < ack(kf, list_add(l))})      \
-\      ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat).                          \
-\                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
-by (etac list.induct 1);
-by (res_inst_tac [("x","0")] bexI 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le])));
-by (Clarify_tac 1);
-by (rtac (ballI RS bexI) 1);
-by (rtac (add_lt_mono RS lt_trans) 1);
-by (REPEAT (FIRSTGOAL (etac bspec)));
-by (rtac ack_add_bound 5);
-by Auto_tac;
-qed "COMP_map_lemma";
-
-Goalw [COMP_def]
- "[| kg: nat;                                 \
-\         \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l));          \
-\         fs \\<in> list({f \\<in> prim_rec .                               \
-\                    \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat).                \
-\                       f`l < ack(kf, list_add(l))})            \
-\      |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
-by (Asm_simp_tac 1);
-by (ftac list_CollectD 1);
-by (etac (COMP_map_lemma RS bexE) 1);
-by (rtac (ballI RS bexI) 1);
-by (etac (bspec RS lt_trans) 1);
-by (rtac lt_trans 2);
-by (rtac ack_nest_bound 3);
-by (etac (bspec RS ack_lt_mono2) 2);
-by Auto_tac;
-qed "COMP_case";
-
-(** PREC case **)
-
-Goalw [PREC_def]
- "[| \\<forall>l \\<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
-\           \\<forall>l \\<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
-\           f \\<in> prim_rec;  kf: nat;                                       \
-\           g \\<in> prim_rec;  kg: nat;                                       \
-\           l \\<in> list(nat)                                                \
-\        |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
-by (exhaust_tac "l" 1);
-by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
-by (Asm_simp_tac 1);
-by (etac ssubst 1);  (*get rid of the needless assumption*)
-by (induct_tac "a" 1);
-(*base case*)
-by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
-	    assume_tac, rtac (add_le_self RS ack_lt_mono1)]);
-by (ALLGOALS Asm_simp_tac);
-(*ind step*)
-by (rtac (succ_leI RS lt_trans1) 1);
-by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
-by (etac bspec 2);
-by (rtac (nat_le_refl RS add_le_mono) 1);
-by Typecheck_tac;
-by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
-(*final part of the simplification*)
-by (Asm_simp_tac 1);
-by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
-by (etac ack_lt_mono2 4);
-by Auto_tac;
-qed "PREC_case_lemma";
-
-Goal "[| f \\<in> prim_rec;  kf: nat;                               \
-\        g \\<in> prim_rec;  kg: nat;                               \
-\        \\<forall>l \\<in> list(nat). f`l < ack(kf, list_add(l));        \
-\        \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l))         \
-\     |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))";
-by (rtac (ballI RS bexI) 1);
-by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
-by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec));
-by Typecheck_tac;
-qed "PREC_case";
-
-Goal "f \\<in> prim_rec ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). f`l < ack(k, list_add(l))";
-by (etac prim_rec.induct 1);
-by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
-			      PREC_case], 
-	      simpset()));
-qed "ack_bounds_prim_rec";
-
-Goal "~ (\\<lambda>l \\<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \\<in> prim_rec";
-by (rtac notI 1);
-by (etac (ack_bounds_prim_rec RS bexE) 1);
-by (rtac lt_irrefl 1);
-by (dres_inst_tac [("x", "[x]")] bspec 1);
-by Auto_tac;
-qed "ack_not_prim_rec";
-

--- a/src/ZF/ex/Primrec.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      ZF/ex/Primrec.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Primitive Recursive Functions: the inductive definition
-
-Proof adopted from
-Nora Szasz, 
-A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
-In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
-
-See also E. Mendelson, Introduction to Mathematical Logic.
-(Van Nostrand, 1964), page 250, exercise 11.
-*)
-
-Primrec = Primrec_defs +
-consts
-    prim_rec :: i
-
-inductive
-  domains "prim_rec" <= "list(nat)->nat"
-  intrs
-    SC       "SC \\<in> prim_rec"
-    CONST    "k \\<in> nat ==> CONST(k) \\<in> prim_rec"
-    PROJ     "i \\<in> nat ==> PROJ(i) \\<in> prim_rec"
-    COMP     "[| g \\<in> prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
-    PREC     "[| f \\<in> prim_rec; g \\<in> prim_rec |] ==> PREC(f,g): prim_rec"
-  monos       list_mono
-  con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
-  type_intrs "nat_typechecks @ list.intrs @                     
-              [lam_type, list_case_type, drop_type, map_type,   
-              apply_type, rec_type]"
-
-end

--- a/src/ZF/ex/Primrec_defs.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(*  Title:      ZF/ex/Primrec
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Primitive Recursive Functions: preliminary definitions
-*)
-
-(*Theory TF redeclares map_type*)
-val map_type = thm "List.map_type";
-
-(** Useful special cases of evaluation ***)
-
-Goalw [SC_def] "[| x \\<in> nat;  l \\<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
-by (Asm_simp_tac 1);
-qed "SC";
-
-Goalw [CONST_def] "[| l \\<in> list(nat) |] ==> CONST(k) ` l = k";
-by (Asm_simp_tac 1);
-qed "CONST";
-
-Goalw [PROJ_def] "[| x \\<in> nat;  l \\<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
-by (Asm_simp_tac 1);
-qed "PROJ_0";
-
-Goalw [COMP_def] "[| l \\<in> list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
-by (Asm_simp_tac 1);
-qed "COMP_1";
-
-Goalw [PREC_def] "l \\<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
-by (Asm_simp_tac 1);
-qed "PREC_0";
-
-Goalw [PREC_def]
-    "[| x \\<in> nat;  l \\<in> list(nat) |] ==>  \
-\         PREC(f,g) ` (Cons(succ(x),l)) = \
-\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
-by (Asm_simp_tac 1);
-qed "PREC_succ";
-

--- a/src/ZF/ex/Primrec_defs.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*  Title:      ZF/ex/Primrec_defs.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Primitive Recursive Functions: preliminary definitions of the constructors
-
-[These must reside in a separate theory in order to be visible in the
- con_defs part of prim_rec's inductive definition.]
-*)
-
-Primrec_defs = Main +
-
-consts
-    SC      :: i
-    CONST   :: i=>i
-    PROJ    :: i=>i
-    COMP    :: [i,i]=>i
-    PREC    :: [i,i]=>i
-    ACK     :: i=>i
-    ack     :: [i,i]=>i
-
-translations
-  "ack(x,y)"  == "ACK(x) ` [y]"
-
-defs
-
-  SC_def    "SC == \\<lambda>l \\<in> list(nat).list_case(0, %x xs. succ(x), l)"
-
-  CONST_def "CONST(k) == \\<lambda>l \\<in> list(nat).k"
-
-  PROJ_def  "PROJ(i) == \\<lambda>l \\<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
-
-  COMP_def  "COMP(g,fs) == \\<lambda>l \\<in> list(nat). g ` List.map(%f. f`l, fs)"
-
-  (*Note that g is applied first to PREC(f,g)`y and then to y!*)
-  PREC_def  "PREC(f,g) == 
-            \\<lambda>l \\<in> list(nat). list_case(0, 
-                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
-  
-primrec
-  ACK_0     "ACK(0) = SC"
-  ACK_succ  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
-				  COMP(ACK(i), [PROJ(0)]))"
-
-end

--- a/src/ZF/ex/PropLog.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-(*  Title:      ZF/ex/prop-log.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow & Lawrence C Paulson
-    Copyright   1992  University of Cambridge
-
-Inductive definition of propositional logic.
-Soundness and completeness w.r.t. truth-tables.
-
-Prove: If H|=p then G|=p where G \\<in> Fin(H)
-*)
-
-Addsimps prop.intrs;
-
-(*** Semantics of propositional logic ***)
-
-(** The function is_true **)
-
-Goalw [is_true_def] "is_true(Fls,t) <-> False";
-by (Simp_tac 1);
-qed "is_true_Fls";
-
-Goalw [is_true_def] "is_true(#v,t) <-> v \\<in> t";
-by (Simp_tac 1);
-qed "is_true_Var";
-
-Goalw [is_true_def] "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
-by (Simp_tac 1);
-qed "is_true_Imp";
-
-Addsimps [is_true_Fls, is_true_Var, is_true_Imp];
-
-
-(*** Proof theory of propositional logic ***)
-
-Goalw thms.defs "G \\<subseteq> H ==> thms(G) \\<subseteq> thms(H)";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac thms.bnd_mono 1));
-by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-qed "thms_mono";
-
-val thms_in_pl = thms.dom_subset RS subsetD;
-
-val ImpE = prop.mk_cases "p=>q \\<in> prop";
-
-(*Stronger Modus Ponens rule: no typechecking!*)
-Goal "[| H |- p=>q;  H |- p |] ==> H |- q";
-by (rtac thms.MP 1);
-by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1));
-qed "thms_MP";
-
-(*Rule is called I for Identity Combinator, not for Introduction*)
-Goal "p \\<in> prop ==> H |- p=>p";
-by (rtac (thms.S RS thms_MP RS thms_MP) 1);
-by (rtac thms.K 5);
-by (rtac thms.K 4);
-by (REPEAT (ares_tac prop.intrs 1));
-qed "thms_I";
-
-(** Weakening, left and right **)
-
-(* [| G \\<subseteq> H;  G|-p |] ==> H|-p   Order of premises is convenient with RS*)
-bind_thm ("weaken_left", (thms_mono RS subsetD));
-
-(* H |- p ==> cons(a,H) |- p *)
-val weaken_left_cons = subset_consI RS weaken_left;
-
-val weaken_left_Un1  = Un_upper1 RS weaken_left;
-val weaken_left_Un2  = Un_upper2 RS weaken_left;
-
-Goal "[| H |- q;  p \\<in> prop |] ==> H |- p=>q";
-by (rtac (thms.K RS thms_MP) 1);
-by (REPEAT (ares_tac [thms_in_pl] 1));
-qed "weaken_right";
-
-(*The deduction theorem*)
-Goal "[| cons(p,H) |- q;  p \\<in> prop |] ==>  H |- p=>q";
-by (etac thms.induct 1);
-by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1);
-by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1);
-by (blast_tac (claset() addIs [thms.S RS weaken_right]) 1);
-by (blast_tac (claset() addIs [thms.DN RS weaken_right]) 1);
-by (blast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1);
-qed "deduction";
-
-
-(*The cut rule*)
-Goal "[| H|-p;  cons(p,H) |- q |] ==>  H |- q";
-by (rtac (deduction RS thms_MP) 1);
-by (REPEAT (ares_tac [thms_in_pl] 1));
-qed "cut";
-
-Goal "[| H |- Fls; p \\<in> prop |] ==> H |- p";
-by (rtac (thms.DN RS thms_MP) 1);
-by (rtac weaken_right 2);
-by (REPEAT (ares_tac (prop.intrs@[consI1]) 1));
-qed "thms_FlsE";
-
-(* [| H |- p=>Fls;  H |- p;  q \\<in> prop |] ==> H |- q *)
-bind_thm ("thms_notE", (thms_MP RS thms_FlsE));
-
-(*Soundness of the rules wrt truth-table semantics*)
-Goalw [logcon_def] "H |- p ==> H |= p";
-by (etac thms.induct 1);
-by Auto_tac;
-qed "soundness";
-
-(*** Towards the completeness proof ***)
-
-val [premf,premq] = goal PropLog.thy
-    "[| H |- p=>Fls; q \\<in> prop |] ==> H |- p=>q";
-by (rtac (premf RS thms_in_pl RS ImpE) 1);
-by (rtac deduction 1);
-by (rtac (premf RS weaken_left_cons RS thms_notE) 1);
-by (REPEAT (ares_tac [premq, consI1, thms.H] 1));
-qed "Fls_Imp";
-
-val [premp,premq] = goal PropLog.thy
-    "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls";
-by (cut_facts_tac ([premp,premq] RL [thms_in_pl]) 1);
-by (etac ImpE 1);
-by (rtac deduction 1);
-by (rtac (premq RS weaken_left_cons RS thms_MP) 1);
-by (rtac (consI1 RS thms.H RS thms_MP) 1);
-by (rtac (premp RS weaken_left_cons) 2);
-by (REPEAT (ares_tac prop.intrs 1));
-qed "Imp_Fls";
-
-(*Typical example of strengthening the induction formula*)
-Goal "p \\<in> prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)";
-by (Simp_tac 1);
-by (induct_tac "p" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
-by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, 
-			       Fls_Imp RS weaken_left_Un2]));
-by (ALLGOALS (blast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
-					weaken_right, Imp_Fls])));
-qed "hyps_thms_if";
-
-(*Key lemma for completeness; yields a set of assumptions satisfying p*)
-Goalw [logcon_def] "[| p \\<in> prop;  0 |= p |] ==> hyps(p,t) |- p";
-by (dtac hyps_thms_if 1);
-by (Asm_full_simp_tac 1);
-qed "logcon_thms_p";
-
-(*For proving certain theorems in our new propositional logic*)
-val thms_cs = 
-    ZF_cs addSIs (prop.intrs @ [deduction])
-          addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
-
-(*The excluded middle in the form of an elimination rule*)
-Goal "[| p \\<in> prop;  q \\<in> prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
-by (rtac (deduction RS deduction) 1);
-by (rtac (thms.DN RS thms_MP) 1);
-by (ALLGOALS (blast_tac thms_cs));
-qed "thms_excluded_middle";
-
-(*Hard to prove directly because it requires cuts*)
-Goal "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \\<in> prop |] ==> H |- q";
-by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
-by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
-qed "thms_excluded_middle_rule";
-
-(*** Completeness -- lemmas for reducing the set of assumptions ***)
-
-(*For the case hyps(p,t)-cons(#v,Y) |- p;
-  we also have hyps(p,t)-{#v} \\<subseteq> hyps(p, t-{v}) *)
-Goal "p \\<in> prop ==> hyps(p, t-{v}) \\<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "hyps_Diff";
-
-(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
-  we also have hyps(p,t)-{#v=>Fls} \\<subseteq> hyps(p, cons(v,t)) *)
-Goal "p \\<in> prop ==> hyps(p, cons(v,t)) \\<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "hyps_cons";
-
-(** Two lemmas for use with weaken_left **)
-
-Goal "B-C \\<subseteq> cons(a, B-cons(a,C))";
-by (Fast_tac 1);
-qed "cons_Diff_same";
-
-Goal "cons(a, B-{c}) - D \\<subseteq> cons(a, B-cons(c,D))";
-by (Fast_tac 1);
-qed "cons_Diff_subset2";
-
-(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
- could probably prove the stronger hyps(p,t) \\<in> Fin(hyps(p,0) Un hyps(p,nat))*)
-Goal "p \\<in> prop ==> hyps(p,t) \\<in> Fin(\\<Union>v \\<in> nat. {#v, #v=>Fls})";
-by (induct_tac "p" 1);
-by Auto_tac;  
-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 [premp,sat] = goal PropLog.thy
-    "[| p \\<in> prop;  0 |= p |] ==> \\<forall>t. hyps(p,t) - hyps(p,t0) |- p";
-by (rtac (premp RS hyps_finite RS Fin_induct) 1);
-by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
-by Safe_tac;
-(*Case hyps(p,t)-cons(#v,Y) |- p *)
-by (rtac thms_excluded_middle_rule 1);
-by (etac prop.Var_I 3);
-by (rtac (cons_Diff_same RS weaken_left) 1);
-by (etac spec 1);
-by (rtac (cons_Diff_subset2 RS weaken_left) 1);
-by (rtac (premp RS hyps_Diff RS Diff_weaken_left) 1);
-by (etac spec 1);
-(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
-by (rtac thms_excluded_middle_rule 1);
-by (etac prop.Var_I 3);
-by (rtac (cons_Diff_same RS weaken_left) 2);
-by (etac spec 2);
-by (rtac (cons_Diff_subset2 RS weaken_left) 1);
-by (rtac (premp RS hyps_cons RS Diff_weaken_left) 1);
-by (etac spec 1);
-qed "completeness_0_lemma";
-
-(*The base case for completeness*)
-val [premp,sat] = goal PropLog.thy "[| p \\<in> prop;  0 |= p |] ==> 0 |- p";
-by (rtac (Diff_cancel RS subst) 1);
-by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1);
-qed "completeness_0";
-
-(*A semantic analogue of the Deduction Theorem*)
-Goalw [logcon_def] "[| cons(p,H) |= q |] ==> H |= p=>q";
-by Auto_tac;
-qed "logcon_Imp";
-
-Goal "H \\<in> Fin(prop) ==> \\<forall>p \\<in> prop. H |= p --> H |- p";
-by (etac Fin_induct 1);
-by (safe_tac (claset() addSIs [completeness_0]));
-by (rtac (weaken_left_cons RS thms_MP) 1);
-by (blast_tac (claset() addSIs (logcon_Imp::prop.intrs)) 1);
-by (blast_tac thms_cs 1);
-qed "completeness_lemma";
-
-val completeness = completeness_lemma RS bspec RS mp;
-
-val [finite] = goal PropLog.thy "H \\<in> Fin(prop) ==> H |- p <-> H |= p & p \\<in> prop";
-by (fast_tac (claset() addSEs [soundness, finite RS completeness, 
-			       thms_in_pl]) 1);
-qed "thms_iff";
-
-writeln"Reached end of file.";

--- a/src/ZF/ex/PropLog.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      ZF/ex/PropLog.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow & Lawrence C Paulson
-    Copyright   1993  University of Cambridge
-
-Datatype definition of propositional logic formulae and inductive definition
-of the propositional tautologies.
-*)
-
-PropLog = Main +
-
-(** The datatype of propositions; note mixfix syntax **)
-consts
-  prop     :: i
-
-datatype
-  "prop" = Fls
-         | Var ("n \\<in> nat")                       ("#_" [100] 100)
-         | "=>" ("p \\<in> prop", "q \\<in> prop")          (infixr 90)
-
-(** The proof system **)
-consts
-  thms     :: i => i
-
-syntax
-  "|-"     :: [i,i] => o                        (infixl 50)
-
-translations
-  "H |- p" == "p \\<in> thms(H)"
-
-inductive
-  domains "thms(H)" <= "prop"
-  intrs
-    H  "[| p \\<in> H;  p \\<in> prop |] ==> H |- p"
-    K  "[| p \\<in> prop;  q \\<in> prop |] ==> H |- p=>q=>p"
-    S  "[| p \\<in> prop;  q \\<in> prop;  r \\<in> prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
-    DN "p \\<in> prop ==> H |- ((p=>Fls) => Fls) => p"
-    MP "[| H |- p=>q;  H |- p;  p \\<in> prop;  q \\<in> prop |] ==> H |- q"
-  type_intrs "prop.intrs"
-
-
-(** The semantics **)
-consts
-  "|="        :: [i,i] => o                        (infixl 50)
-  hyps        :: [i,i] => i
-  is_true_fun :: [i,i] => i
-
-constdefs (*this definitionis necessary since predicates can't be recursive*)
-  is_true     :: [i,i] => o
-    "is_true(p,t) == is_true_fun(p,t)=1"
-
-defs
-  (*Logical consequence: for every valuation, if all elements of H are true
-     then so is p*)
-  logcon_def  "H |= p == \\<forall>t. (\\<forall>q \\<in> H. is_true(q,t)) --> is_true(p,t)"
-
-primrec (** A finite set of hypotheses from t and the Vars in p **)
-  "hyps(Fls, t)    = 0"
-  "hyps(Var(v), t) = (if v \\<in> t then {#v} else {#v=>Fls})"
-  "hyps(p=>q, t)   = hyps(p,t) Un hyps(q,t)"
- 
-primrec (** Semantics of propositional logic **)
-  "is_true_fun(Fls, t)    = 0"
-  "is_true_fun(Var(v), t) = (if v \\<in> t then 1 else 0)"
-  "is_true_fun(p=>q, t)   = (if is_true_fun(p,t)=1 then is_true_fun(q,t)
-			     else 1)"
-
-end

--- a/src/ZF/ex/ROOT.ML	Wed Nov 07 00:16:19 2001 +0100
+++ b/src/ZF/ex/ROOT.ML	Wed Nov 07 12:29:07 2001 +0100
@@ -7,6 +7,7 @@
 *)
 
 time_use_thy "misc";
+time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
 time_use_thy "Primes";          (*GCD theory*)
 time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
@@ -22,17 +23,6 @@
 time_use_thy "Brouwer";         (*Infinite-branching trees*)
 time_use_thy "Enum";            (*Enormous enumeration type*)
 
-(** Inductive definitions **)
-time_use_thy "Rmap";            (*mapping a relation over a list*)
-time_use_thy "Mutil";           (*mutilated chess board*)
-time_use_thy "PropLog";         (*completeness of propositional logic*)
-time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
-(*two Coq examples by Christine Paulin-Mohring*)
-time_use_thy "ListN";
-time_use_thy "Acc";
-time_use_thy "Comb";            (*Combinatory Logic example*)
-time_use_thy "Primrec";         (*Primitive recursive functions*)
-
 (** CoDatatypes **)
 time_use_thy "LList";
 time_use_thy "CoUnit";

--- a/src/ZF/ex/Rmap.ML	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(*  Title:      ZF/ex/Rmap
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Inductive definition of an operator to "map" a relation over a list
-*)
-
-Goalw rmap.defs "r \\<subseteq> s ==> rmap(r) \\<subseteq> rmap(s)";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac rmap.bnd_mono 1));
-by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
-                      basic_monos) 1));
-qed "rmap_mono";
-
-val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> \\<in> rmap(r)"
-and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> \\<in> rmap(r)";
-
-AddIs  rmap.intrs;
-AddSEs [Nil_rmap_case, Cons_rmap_case];
-
-Goal "r \\<subseteq> A*B ==> rmap(r) \\<subseteq> list(A)*list(B)";
-by (rtac (rmap.dom_subset RS subset_trans) 1);
-by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
-                      Sigma_mono, list_mono] 1));
-qed "rmap_rel_type";
-
-Goal "A \\<subseteq> domain(r) ==> list(A) \\<subseteq> domain(rmap(r))";
-by (rtac subsetI 1);
-by (etac list.induct 1);
-by (ALLGOALS Fast_tac);
-qed "rmap_total";
-
-Goalw [function_def] "function(r) ==> function(rmap(r))";
-by (rtac (impI RS allI RS allI) 1);
-by (etac rmap.induct 1);
-by (ALLGOALS Fast_tac);
-qed "rmap_functional";
-
-
-(** If f is a function then rmap(f) behaves as expected. **)
-
-Goal "f \\<in> A->B ==> rmap(f): list(A)->list(B)";
-by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type,
-					   rmap_functional, rmap_total]) 1);
-qed "rmap_fun_type";
-
-Goalw [apply_def] "rmap(f)`Nil = Nil";
-by (Blast_tac 1);
-qed "rmap_Nil";
-
-Goal "[| f \\<in> A->B;  x \\<in> A;  xs: list(A) |]  \
-\     ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
-by (rtac apply_equality 1);
-by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
-qed "rmap_Cons";

--- a/src/ZF/ex/Rmap.thy	Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      ZF/ex/Rmap
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Inductive definition of an operator to "map" a relation over a list
-*)
-
-Rmap = Main +
-
-consts
-  rmap :: i=>i
-
-inductive
-  domains "rmap(r)" <= "list(domain(r))*list(range(r))"
-  intrs
-    NilI  "<Nil,Nil> \\<in> rmap(r)"
-
-    ConsI "[| <x,y>: r;  <xs,ys> \\<in> rmap(r) |] ==> 
-          <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)"
-
-  type_intrs "[domainI,rangeI] @ list.intrs"
-
-end
-