# HG changeset patch
# User paulson
# Date 1008857868 -3600
# Node ID 5820841f21fd503243ab5081c1fd81073431b841
# Parent  7fb12775ce98d2c8a7ffbe57da20b4e6a98ebfb6
converted some ZF/Induct examples to Isar

diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Acc.ML
--- a/src/ZF/Induct/Acc.ML	Thu Dec 20 15:00:02 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 prems@acc.intrs) 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";
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Acc.thy	Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/Acc.thy
+(*  Title:      ZF/Induct/Acc.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
@@ -9,15 +9,52 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Acc = Main +
+theory Acc = Main:
 
 consts
-  acc :: i=>i
+  acc :: "i=>i"
 
 inductive
   domains "acc(r)" <= "field(r)"
-  intrs
-    vimage  "[| r-``{a}: Pow(acc(r)); a \\<in> field(r) |] ==> a \\<in> acc(r)"
+  intros
+    vimage:  "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
   monos      Pow_mono
 
+
+(*The introduction rule must require  a \<in> field(r)  
+  Otherwise acc(r) would be a proper class!    *)
+
+(*The intended introduction rule*)
+lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r);  a \<in> field(r) |] ==> a \<in> acc(r)"
+by (blast intro: acc.intros)
+
+lemma acc_downward: "[| b \<in> acc(r);  <a,b>: r |] ==> a \<in> acc(r)"
+by (erule acc.cases, blast)
+
+lemma acc_induct:
+    "[| a \<in> acc(r);                                              
+        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r --> P(y) |] ==> P(x)  
+     |] ==> P(a)"
+apply (erule acc.induct)
+apply (blast intro: acc.intros) 
+done
+
+lemma wf_on_acc: "wf[acc(r)](r)"
+apply (rule wf_onI2)
+apply (erule acc_induct)
+apply fast
+done
+
+(* field(r) \<subseteq> acc(r) ==> wf(r) *)
+lemmas acc_wfI = wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf]
+
+lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)"
+apply (rule subsetI)
+apply (erule wf_induct2, assumption)
+apply (blast intro: accI)+
+done
+
+lemma wf_acc_iff: "wf(r) <-> field(r) \<subseteq> acc(r)"
+by (rule iffI, erule acc_wfD, erule acc_wfI) 
+
 end
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Comb.ML
--- a/src/ZF/Induct/Comb.ML	Thu Dec 20 15:00:02 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.";
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Comb.thy	Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/Comb.thy
+(*  Title:      ZF/Induct/Comb.thy
     ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1994  University of Cambridge
@@ -10,60 +10,63 @@
     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
 *)
 
 
-Comb = Main +
+theory 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)
+         | "#" ("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)
+  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^*"
+  "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"
+  intros
+    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_intros "comb.intros"
 
 
 (** 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)
+  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^+"
+  "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"
+  intros
+    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_intros "comb.intros"
 
 
 (*Misc definitions*)
@@ -71,9 +74,197 @@
   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))"
+  diamond :: "i => o"
+  "diamond(r) == \<forall>x y. <x,y>\<in>r --> 
+                          (\<forall>y'. <x,y'>\<in>r --> 
+                                   (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
+
+
+
+(*** Transitive closure preserves the Church-Rosser property ***)
+
+lemma diamond_strip_lemmaD [rule_format]:
+    "[| diamond(r);  <x,y>:r^+ |] ==>  
+     \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
+apply (unfold diamond_def)
+apply (erule trancl_induct)
+apply (blast intro: r_into_trancl)
+apply clarify
+apply (drule spec [THEN mp], assumption) 
+apply (blast intro: r_into_trancl trans_trancl [THEN transD])
+done
+
+
+lemma diamond_trancl: "diamond(r) ==> diamond(r^+)"
+apply (simp (no_asm_simp) add: diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule trancl_induct)
+apply (auto ); 
+apply (best intro: r_into_trancl trans_trancl [THEN transD]
+             dest: diamond_strip_lemmaD)+
+done
+
+
+inductive_cases Ap_E [elim!]: "p#q \<in> comb"
+
+declare comb.intros [intro!]
+
+
+(*** Results about Contraction ***)
+
+(*For type checking: replaces a-1->b by a,b \<in> comb *)
+lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
+lemmas contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemma field_contract_eq: "field(contract) = comb"
+by (blast intro: contract.K elim!: contract_combE2)
+
+lemmas reduction_refl = 
+    field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl]
+
+lemmas rtrancl_into_rtrancl2 =  
+    r_into_rtrancl [THEN trans_rtrancl [THEN transD]]
+
+declare reduction_refl [intro!] contract.K [intro!] contract.S [intro!]
+
+lemmas reduction_rls = contract.K [THEN rtrancl_into_rtrancl2]
+                     contract.S [THEN rtrancl_into_rtrancl2]
+                     contract.Ap1 [THEN rtrancl_into_rtrancl2]
+                     contract.Ap2 [THEN rtrancl_into_rtrancl2]
+
+(*Example only: not used*)
+lemma reduce_I: "p \<in> comb ==> I#p ---> p"
+by (unfold I_def, blast intro: reduction_rls)
+
+lemma comb_I: "I \<in> comb"
+by (unfold I_def, blast)
+
+(** Non-contraction results **)
+
+(*Derive a case for each combinator constructor*)
+inductive_cases K_contractE [elim!]: "K -1-> r"
+inductive_cases S_contractE [elim!]: "S -1-> r"
+inductive_cases Ap_contractE [elim!]: "p#q -1-> r"
+
+declare contract.Ap1 [intro] contract.Ap2 [intro]
+
+lemma I_contract_E: "I -1-> r ==> P"
+by (auto simp add: I_def) 
+
+lemma K1_contractD: "K#p -1-> r ==> (\<exists>q. r = K#q & p -1-> q)"
+by auto
+
+lemma Ap_reduce1: "[| p ---> q;  r \<in> comb |] ==> p#r ---> q#r"
+apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+apply (erule rtrancl_induct)
+apply (blast intro: reduction_rls)
+apply (erule trans_rtrancl [THEN transD])
+apply (blast intro: contract_combD2 reduction_rls)
+done
+
+lemma Ap_reduce2: "[| p ---> q;  r \<in> comb |] ==> r#p ---> r#q"
+apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+apply (erule rtrancl_induct)
+apply (blast intro: reduction_rls)
+apply (erule trans_rtrancl [THEN transD])
+apply (blast intro: contract_combD2 reduction_rls)
+done
+
+(** Counterexample to the diamond property for -1-> **)
+
+lemma KIII_contract1: "K#I#(I#I) -1-> I"
+by (blast intro: comb.intros contract.K comb_I)
+
+lemma KIII_contract2: "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"
+by (unfold I_def, blast intro: comb.intros contract.intros)
+
+
+lemma KIII_contract3: "K#I#((K#I)#(K#I)) -1-> I"
+by (blast intro: comb.intros contract.K comb_I)
+
+lemma not_diamond_contract: "~ diamond(contract)"
+apply (unfold diamond_def)
+apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3 
+             elim!: I_contract_E)
+done
+
+
+
+(*** Results about Parallel Contraction ***)
+
+(*For type checking: replaces a=1=>b by a,b \<in> comb *)
+lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
+lemmas parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemma field_parcontract_eq: "field(parcontract) = comb"
+by (blast intro: parcontract.K elim!: parcontract_combE2)
+
+(*Derive a case for each combinator constructor*)
+inductive_cases K_parcontractE [elim!]: "K =1=> r"
+inductive_cases S_parcontractE [elim!]: "S =1=> r"
+inductive_cases Ap_parcontractE [elim!]: "p#q =1=> r"
+
+declare parcontract.intros [intro]
+
+
+(*** Basic properties of parallel contraction ***)
+
+lemma K1_parcontractD [dest!]: "K#p =1=> r ==> (\<exists>p'. r = K#p' & p =1=> p')"
+by auto
+
+lemma S1_parcontractD [dest!]: "S#p =1=> r ==> (\<exists>p'. r = S#p' & p =1=> p')"
+by auto
+
+lemma S2_parcontractD [dest!]:
+     "S#p#q =1=> r ==> (\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"
+by auto
+
+
+(*Church-Rosser property for parallel contraction*)
+lemma diamond_parcontract: "diamond(parcontract)"
+apply (unfold diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule parcontract.induct)
+apply (blast elim!: comb.free_elims  intro: parcontract_combD2)+
+done
+
+(*** Equivalence of p--->q and p===>q ***)
+
+lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
+by (erule contract.induct, auto)
+
+lemma reduce_imp_parreduce: "p--->q ==> p===>q"
+apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+apply (erule rtrancl_induct)
+ apply (blast intro: r_into_trancl)
+apply (blast intro: contract_imp_parcontract r_into_trancl 
+                    trans_trancl [THEN transD])
+done
+
+
+lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
+apply (erule parcontract.induct)
+   apply (blast intro: reduction_rls)
+  apply (blast intro: reduction_rls)
+ apply (blast intro: reduction_rls)
+apply (blast intro: trans_rtrancl [THEN transD] 
+                Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
+done
+
+lemma parreduce_imp_reduce: "p===>q ==> p--->q"
+apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
+apply (erule trancl_induct, erule parcontract_imp_reduce)
+apply (erule trans_rtrancl [THEN transD])
+apply (erule parcontract_imp_reduce)
+done
+
+lemma parreduce_iff_reduce: "p===>q <-> p--->q"
+by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
 
 end
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/ListN.ML
--- a/src/ZF/Induct/ListN.ML	Thu Dec 20 15:00:02 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)";
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/ListN.thy	Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/ListN
+(*  Title:      ZF/Induct/ListN
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
@@ -9,14 +9,50 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-ListN = Main +
+theory ListN = Main:
 
-consts  listn ::i=>i
+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"
+  intros
+    NilI:  "<0,Nil> \<in> listn(A)"
+    ConsI: "[| a \<in> A; <n,l> \<in> listn(A) |] ==> <succ(n), Cons(a,l)> \<in> listn(A)"
+  type_intros  nat_typechecks list.intros
+
+
+lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
+by (erule list.induct, simp_all add: listn.intros)
+
+lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
+apply (rule iffI)
+apply (erule listn.induct)
+apply auto
+apply (blast intro: list_into_listn)
+done
+
+lemma listn_image_eq: "listn(A)``{n} = {l \<in> list(A). length(l)=n}"
+apply (rule equality_iffI)
+apply (simp (no_asm) add: listn_iff separation image_singleton_iff)
+done
+
+lemma listn_mono: "A \<subseteq> B ==> listn(A) \<subseteq> listn(B)"
+apply (unfold listn.defs )
+apply (rule lfp_mono)
+apply (rule listn.bnd_mono)+
+apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
+done
+
+lemma listn_append:
+     "[| <n,l> \<in> listn(A); <n',l'> \<in> listn(A) |] ==> <n#+n', l@l'> \<in> listn(A)"
+apply (erule listn.induct)
+apply (frule listn.dom_subset [THEN subsetD])
+apply (simp_all add: listn.intros)
+done
+
+inductive_cases Nil_listn_case: "<i,Nil> \<in> listn(A)"
+inductive_cases Cons_listn_case: "<i,Cons(x,l)> \<in> listn(A)"
+
+inductive_cases zero_listn_case: "<0,l> \<in> listn(A)"
+inductive_cases succ_listn_case: "<succ(i),l> \<in> listn(A)"
 
 end
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Multiset.ML
--- a/src/ZF/Induct/Multiset.ML	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Multiset.ML	Thu Dec 20 15:17:48 2001 +0100
@@ -884,7 +884,7 @@
 
 Goal "acc(0)=0";
 by (auto_tac (claset()  addSIs [equalityI]
-    addDs  [acc.dom_subset RS subsetD], simpset()));
+    addDs  [thm "acc.dom_subset" RS subsetD], simpset()));
 qed "acc_0";
 
 Goal "[| ALL b:A. <b,a>:r --> \
@@ -893,10 +893,10 @@
 \   ALL M. <M,M0> : multirel1(A, r) --> M +# {#a#} : acc(multirel1(A, r)) |] \
 \ ==> M0 +# {#a#} : acc(multirel1(A, r))";
 by (subgoal_tac "multiset[A](M0)" 1);
-by (etac acc.elim 2);
+by (etac (thm "acc.cases") 2);
 by (etac fieldE 2);
 by (REPEAT(blast_tac (claset() addDs [multirel1D]) 2));
-by (rtac accI 1);
+by (rtac (thm "accI") 1);
 by (rename_tac "N" 1);
 by (dtac less_munion 1);
 by (Blast_tac 1);
@@ -926,13 +926,12 @@
 Goal  "[| ALL b:A. <b,a>:r  \
 \  --> (ALL M : acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r))); \
 \       M:acc(multirel1(A, r)); a:A|] ==> M +# {#a#} : acc(multirel1(A, r))";
-by (etac acc_induct 1);
+by (etac (thm "acc_induct") 1);
 by (blast_tac (claset() addIs [lemma1]) 1);
 qed "lemma2";
 
-Goal
- "[| wf[A](r); a:A |] ==> \
-\  ALL M:acc(multirel1(A, r)). M +# {#a#} : acc(multirel1(A, r))";
+Goal "[| wf[A](r); a:A |] \
+\     ==> ALL M:acc(multirel1(A, r)). M +# {#a#} : acc(multirel1(A, r))";
 by (eres_inst_tac [("a","a")] wf_on_induct 1);
 by (Blast_tac 1);
 by (blast_tac (claset() addIs [lemma2]) 1);
@@ -943,7 +942,7 @@
 by (etac  multiset_induct 1);
 by (ALLGOALS(Clarify_tac));
 (* proving the base case *)
-by (rtac accI 1);
+by (rtac (thm "accI") 1);
 by (cut_inst_tac [("M", "b"), ("r", "r")] not_less_0 1);
 by (Force_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [multirel1_def]) 1);
@@ -974,7 +973,7 @@
 by (rtac wf_on_field_imp_wf 1);
 by (asm_simp_tac (simpset() addsimps [wf_on_0]) 1);
 by (res_inst_tac [("A", "acc(multirel1(A,r))")] wf_on_subset_A 1);
-by (rtac wf_on_acc  1);
+by (rtac (thm "wf_on_acc") 1);
 by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
 by (blast_tac (claset() addIs [all_accessible]) 1);
@@ -1031,8 +1030,7 @@
 by (auto_tac (claset() addDs [domain_type], simpset() addsimps [lemma]));
 qed "mdiff_union_single_conv";
 
-Goal 
-"[| n le m;  m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
+Goal "[| n le m;  m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
 by (auto_tac (claset(), simpset() addsimps 
          [le_iff, diff_self_eq_0, less_iff_succ_add]));
 qed "diff_add_commute";
@@ -1105,9 +1103,8 @@
 qed "melem_imp_eq_diff_union";
 Addsimps [melem_imp_eq_diff_union];
     
-Goal 
-"[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \
-\  ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A";
+Goal "[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \
+\     ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A";
 by (dtac msize_eq_succ_imp_elem 1);
 by Auto_tac;
 by (res_inst_tac [("x", "a")] exI 1);
@@ -1372,8 +1369,7 @@
 AddSEs [mless_irrefl];
 
 (*transitivity*)
-Goalw [mless_def]
-     "[| K <# M; M <# N |] ==> K <# N";
+Goalw [mless_def] "[| K <# M; M <# N |] ==> K <# N";
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "i Un ia")] exI 1);
 by (blast_tac (claset() addDs 
@@ -1459,13 +1455,11 @@
 
 (* <#= *)
 
-Goalw [mle_def]
- "M <#= N ==> omultiset(M) & omultiset(N)";
+Goalw [mle_def] "M <#= N ==> omultiset(M) & omultiset(N)";
 by (auto_tac (claset(), simpset() addsimps [mless_imp_omultiset]));
 qed "mle_imp_omultiset";
 
-Goal
-  "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L";
+Goal "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L";
 by (forw_inst_tac [("M", "M")] mle_imp_omultiset 1);
 by (forw_inst_tac [("M", "N")] mle_imp_omultiset 1);
 by (rewtac mle_def);
@@ -1483,8 +1477,7 @@
 qed "omultiset_0";
 AddIffs [omultiset_0];
 
-Goalw [mle_def, mless_def]
-     "omultiset(M) ==> 0 <#= M";
+Goalw [mle_def, mless_def] "omultiset(M) ==> 0 <#= M";
 by (subgoal_tac "EX i. Ord(i) & multiset[field(Memrel(i))](M)" 1);
 by (asm_full_simp_tac (simpset() addsimps [omultiset_def]) 2);
 by (case_tac "M=0" 1);
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Primrec.ML
--- a/src/ZF/Induct/Primrec.ML	Thu Dec 20 15:00:02 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";
-
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Primrec.thy	Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/Primrec.thy
+(*  Title:      ZF/Induct/Primrec.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
@@ -14,22 +14,357 @@
 (Van Nostrand, 1964), page 250, exercise 11.
 *)
 
-Primrec = Primrec_defs +
+theory Primrec = Main:
+
+constdefs
+  SC      :: "i"
+    "SC == \<lambda>l \<in> list(nat). list_case(0, %x xs. succ(x), l)"
+
+  CONST   :: "i=>i"
+    "CONST(k) == \<lambda>l \<in> list(nat). k"
+
+  PROJ    :: "i=>i"
+    "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
+
+  COMP    :: "[i,i]=>i"
+    "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List.map(%f. f`l, fs)"
+
+  PREC    :: "[i,i]=>i"
+		(*Note that g is applied first to PREC(f,g)`y and then to y!*)
+  "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)"
+
 consts
-    prim_rec :: i
+  ACK     :: "i=>i"
+
+primrec
+  ACK_0:     "ACK(0) = SC"
+  ACK_succ:  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
+		 	 	   COMP(ACK(i), [PROJ(0)]))"
+
+syntax
+  ack     :: "[i,i]=>i"  
+
+translations
+  "ack(x,y)"  == "ACK(x) ` [y]"
+
+
+
+(** Useful special cases of evaluation ***)
+
+lemma SC: "[| x \<in> nat;  l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"
+by (simp add: SC_def) 
+
+lemma CONST: "l \<in> list(nat) ==> CONST(k) ` l = k"
+by (simp add: CONST_def) 
+
+lemma PROJ_0: "[| x \<in> nat;  l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"
+by (simp add: PROJ_def) 
+
+lemma COMP_1: "l \<in> list(nat) ==> COMP(g,[f]) ` l = g` [f`l]"
+by (simp add: COMP_def) 
+
+lemma PREC_0: "l \<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"
+by (simp add: PREC_def) 
+
+lemma PREC_succ: 
+    "[| 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 (simp add: PREC_def) 
+
+
+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]"
+  intros
+    "SC \<in> prim_rec"
+    "k \<in> nat ==> CONST(k) \<in> prim_rec"
+    "i \<in> nat ==> PROJ(i) \<in> prim_rec"
+    "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs): prim_rec"
+    "[| 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_intros  nat_typechecks list.intros
+               lam_type list_case_type drop_type List.map_type   
+               apply_type rec_type
+
+
+(*** Inductive definition of the PR functions ***)
+
+(* c \<in> prim_rec ==> c \<in> list(nat) -> nat *)
+lemmas prim_rec_into_fun [TC] = subsetD [OF prim_rec.dom_subset]
+lemmas [TC] = apply_type [OF prim_rec_into_fun]
+
+declare prim_rec.intros [TC]
+declare nat_into_Ord [TC]
+declare rec_type [TC]
+
+lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i): prim_rec"
+by (induct_tac "i", simp_all)
+
+lemma ack_type [TC]: "[| i \<in> nat;  j \<in> nat |] ==>  ack(i,j): nat"
+by auto
+
+(** Ackermann's function cases **)
+
+(*PROPERTY A 1*)
+lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"
+by (simp add: SC)
+
+(*PROPERTY A 2*)
+lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
+by (simp add: CONST PREC_0)
+
+(*PROPERTY A 3*)
+lemma ack_succ_succ:
+ "[| i\<in>nat;  j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
+by (simp add: CONST PREC_succ COMP_1 PROJ_0)
+
+declare ack_0 [simp] ack_succ_0 [simp] ack_succ_succ [simp] ack_type [simp]
+declare ACK_0 [simp del] ACK_succ [simp del]
+
+
+(*PROPERTY A 4*)
+lemma lt_ack2 [rule_format]: "i \<in> nat ==> \<forall>j \<in> nat. j < ack(i,j)"
+apply (induct_tac "i")
+apply simp
+apply (rule ballI)
+apply (induct_tac "j")
+apply (erule_tac [2] succ_leI [THEN lt_trans1])
+apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])
+apply auto
+done
+
+(*PROPERTY A 5-, the single-step lemma*)
+lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"
+by (induct_tac "i", simp_all add: lt_ack2)
+
+(*PROPERTY A 5, monotonicity for < *)
+lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"
+apply (frule lt_nat_in_nat , assumption)
+apply (erule succ_lt_induct)
+apply assumption
+apply (rule_tac [2] lt_trans)
+apply (auto intro: ack_lt_ack_succ2)
+done
+
+(*PROPERTY A 5', monotonicity for\<le>*)
+lemma ack_le_mono2: "[|j\<le>k;  i\<in>nat;  k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)"
+apply (rule_tac f = "%j. ack (i,j) " in Ord_lt_mono_imp_le_mono)
+apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+;
+done
+
+(*PROPERTY A 6*)
+lemma ack2_le_ack1:
+     "[| i\<in>nat;  j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"
+apply (induct_tac "j")
+apply (simp_all)
+apply (rule ack_le_mono2)
+apply (rule lt_ack2 [THEN succ_leI, THEN le_trans])
+apply auto
+done
+
+(*PROPERTY A 7-, the single-step lemma*)
+lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)"
+apply (rule ack_lt_mono2 [THEN lt_trans2])
+apply (rule_tac [4] ack2_le_ack1)
+apply auto
+done
+
+(*PROPERTY A 7, monotonicity for < *)
+lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)"
+apply (frule lt_nat_in_nat , assumption)
+apply (erule succ_lt_induct)
+apply assumption
+apply (rule_tac [2] lt_trans)
+apply (auto intro: ack_lt_ack_succ1)
+done
+
+(*PROPERTY A 7', monotonicity for\<le>*)
+lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)"
+apply (rule_tac f = "%j. ack (j,k) " in Ord_lt_mono_imp_le_mono)
+apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+;
+done
+
+(*PROPERTY A 8*)
+lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"
+by (induct_tac "j", simp_all)
+
+(*PROPERTY A 9*)
+lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
+by (induct_tac "j", simp_all add: ack_1)
+
+(*PROPERTY A 10*)
+lemma ack_nest_bound:
+     "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |] 
+      ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
+apply (rule lt_trans2 [OF _ ack2_le_ack1]) 
+apply simp
+apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
+apply auto
+apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2])
+done
+
+(*PROPERTY A 11*)
+lemma ack_add_bound:
+     "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |] 
+      ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
+apply (rule_tac j = "ack (succ (1) , ack (i1 #+ i2, j))" in lt_trans)
+apply (simp add: ack_2)
+apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
+apply (rule add_le_mono [THEN leI, THEN leI])
+apply (auto intro: add_le_self add_le_self2 ack_le_mono1)
+done
+
+(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
+  used k#+4.  Quantified version must be nested \<exists>k'. \<forall>i,j... *)
+lemma ack_add_bound2:
+     "[| i < ack(k,j);  j \<in> nat;  k \<in> nat |] 
+      ==> i#+j < ack(succ(succ(succ(succ(k)))), j)"
+apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
+apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
+apply (rule add_lt_mono)
+apply auto
+done
+
+(*** MAIN RESULT ***)
+
+declare list_add_type [simp]
+
+lemma SC_case: "l \<in> list(nat) ==> SC ` l < ack(1, list_add(l))"
+apply (unfold SC_def)
+apply (erule list.cases)
+apply (simp add: succ_iff)
+apply (simp add: ack_1 add_le_self)
+done
+
+(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
+lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
+apply (induct_tac "i")
+apply (simp add: nat_0_le)
+apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
+apply auto
+done
+
+lemma CONST_case: 
+    "[| l \<in> list(nat);  k \<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))"
+by (simp add: CONST_def lt_ack1)
+
+lemma PROJ_case [rule_format]: 
+    "l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
+apply (unfold PROJ_def)
+apply simp
+apply (erule list.induct)
+apply (simp add: nat_0_le)
+apply simp
+apply (rule ballI)
+apply (erule_tac n = "x" in natE)
+apply (simp add: add_le_self)
+apply simp
+apply (erule bspec [THEN lt_trans2])
+apply (rule_tac [2] add_le_self2 [THEN succ_leI])
+apply auto
+done
+
+(** COMP case **)
+
+lemma COMP_map_lemma:
+     "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))"
+apply (erule list.induct)
+apply (rule_tac x = "0" in bexI)
+apply (simp_all add: lt_ack1 nat_0_le)
+apply clarify
+apply (rule ballI [THEN bexI])
+apply (rule add_lt_mono [THEN lt_trans])
+apply (rule_tac [5] ack_add_bound)
+apply blast
+apply auto
+done
+
+lemma COMP_case: 
+ "[| kg\<in>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))"
+apply (simp add: COMP_def)
+apply (frule list_CollectD)
+apply (erule COMP_map_lemma [THEN bexE])
+apply (rule ballI [THEN bexI])
+apply (erule bspec [THEN lt_trans])
+apply (rule_tac [2] lt_trans)
+apply (rule_tac [3] ack_nest_bound)
+apply (erule_tac [2] bspec [THEN ack_lt_mono2])
+apply auto
+done
+
+(** PREC case **)
+
+lemma PREC_case_lemma: 
+ "[| \<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\<in>nat;                                        
+     g \<in> prim_rec;  kg\<in>nat;                                        
+     l \<in> list(nat) |]
+  ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"
+apply (unfold PREC_def)
+apply (erule list.cases) 
+apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
+apply simp
+apply (erule ssubst) (*get rid of the needless assumption*)
+apply (induct_tac "a")
+apply simp_all 
+(*base case*)
+apply (rule lt_trans, erule bspec, assumption); 
+apply (simp add: add_le_self [THEN ack_lt_mono1]) 
+(*ind step*)
+apply (rule succ_leI [THEN lt_trans1])
+apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
+apply (erule_tac [2] bspec)
+apply (rule nat_le_refl [THEN add_le_mono])
+apply typecheck
+apply (simp add: add_le_self2)
+(*final part of the simplification*)
+apply simp
+apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1])
+apply (erule_tac [4] ack_lt_mono2)
+apply auto
+done
+
+lemma PREC_case:
+     "[| f \<in> prim_rec;  kf\<in>nat;                                
+         g \<in> prim_rec;  kg\<in>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))"
+apply (rule ballI [THEN bexI])
+apply (rule lt_trans1 [OF add_le_self PREC_case_lemma])
+apply typecheck
+apply (blast intro: ack_add_bound2 list_add_type)+ 
+done
+
+lemma ack_bounds_prim_rec:
+     "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
+apply (erule prim_rec.induct)
+apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
+done
+
+lemma ack_not_prim_rec:
+     "~ (\<lambda>l \<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \<in> prim_rec"
+apply (rule notI)
+apply (drule ack_bounds_prim_rec)
+apply force
+done
 
 end
+
+
+
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Primrec_defs.ML
--- a/src/ZF/Induct/Primrec_defs.ML	Thu Dec 20 15:00:02 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";
-
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Primrec_defs.thy
--- a/src/ZF/Induct/Primrec_defs.thy	Thu Dec 20 15:00:02 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
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/PropLog.ML
--- a/src/ZF/Induct/PropLog.ML	Thu Dec 20 15:00:02 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.";
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/PropLog.thy	Thu Dec 20 15:17:48 2001 +0100
@@ -1,68 +1,297 @@
-(*  Title:      ZF/ex/PropLog.thy
+(*  Title:      ZF/Induct/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.
+
+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)
 *)
 
-PropLog = Main +
+theory PropLog = Main:
 
 (** The datatype of propositions; note mixfix syntax **)
 consts
-  prop     :: i
+  propn     :: "i"
 
 datatype
-  "prop" = Fls
-         | Var ("n \\<in> nat")                       ("#_" [100] 100)
-         | "=>" ("p \\<in> prop", "q \\<in> prop")          (infixr 90)
+  "propn" = Fls
+         | Var ("n \<in> nat")                       ("#_" [100] 100)
+         | "=>" ("p \<in> propn", "q \<in> propn")          (infixr 90)
 
 (** The proof system **)
 consts
-  thms     :: i => i
+  thms     :: "i => i"
 
 syntax
-  "|-"     :: [i,i] => o                        (infixl 50)
+  "|-"     :: "[i,i] => o"                        (infixl 50)
 
 translations
-  "H |- p" == "p \\<in> thms(H)"
+  "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"
+  domains "thms(H)" <= "propn"
+  intros
+    H:  "[| p \<in> H;  p \<in> propn |] ==> H |- p"
+    K:  "[| p \<in> propn;  q \<in> propn |] ==> H |- p=>q=>p"
+    S:  "[| p \<in> propn;  q \<in> propn;  r \<in> propn |] 
+         ==> H |- (p=>q=>r) => (p=>q) => p=>r"
+    DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p"
+    MP: "[| H |- p=>q;  H |- p;  p \<in> propn;  q \<in> propn |] ==> H |- q"
+  type_intros "propn.intros"
 
 
 (** The semantics **)
 consts
-  "|="        :: [i,i] => o                        (infixl 50)
-  hyps        :: [i,i] => i
-  is_true_fun :: [i,i] => i
+  "|="        :: "[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     :: "[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)"
+  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(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(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)"
 
+declare propn.intros [simp]
+
+(*** Semantics of propositional logic ***)
+
+(** The function is_true **)
+
+lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False"
+by (simp add: is_true_def)
+
+lemma is_true_Var [simp]: "is_true(#v,t) <-> v \<in> t"
+by (simp add: is_true_def)
+
+lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"
+by (simp add: is_true_def)
+
+
+(*** Proof theory of propositional logic ***)
+
+lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)"
+apply (unfold thms.defs )
+apply (rule lfp_mono)
+apply (rule thms.bnd_mono)+
+apply (assumption | rule univ_mono basic_monos)+
+done
+
+lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
+
+inductive_cases ImpE: "p=>q \<in> propn"
+
+(*Stronger Modus Ponens rule: no typechecking!*)
+lemma thms_MP: "[| H |- p=>q;  H |- p |] ==> H |- q"
+apply (rule thms.MP)
+apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
+done
+
+(*Rule is called I for Identity Combinator, not for Introduction*)
+lemma thms_I: "p \<in> propn ==> H |- p=>p"
+apply (rule thms.S [THEN thms_MP, THEN thms_MP])
+apply (rule_tac [5] thms.K)
+apply (rule_tac [4] thms.K)
+apply (simp_all add: propn.intros ) 
+done
+
+(** Weakening, left and right **)
+
+(* [| G \<subseteq> H;  G|-p |] ==> H|-p   Order of premises is convenient with RS*)
+lemmas weaken_left = thms_mono [THEN subsetD, standard]
+
+(* H |- p ==> cons(a,H) |- p *)
+lemmas weaken_left_cons = subset_consI [THEN weaken_left]
+
+lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
+lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
+
+lemma weaken_right: "[| H |- q;  p \<in> propn |] ==> H |- p=>q"
+by (simp_all add:  thms.K [THEN thms_MP] thms_in_pl) 
+
+
+(*The deduction theorem*)
+lemma deduction: "[| cons(p,H) |- q;  p \<in> propn |] ==>  H |- p=>q"
+apply (erule thms.induct)
+    apply (blast intro: thms_I thms.H [THEN weaken_right])
+   apply (blast intro: thms.K [THEN weaken_right])
+  apply (blast intro: thms.S [THEN weaken_right])
+ apply (blast intro: thms.DN [THEN weaken_right])
+apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
+done
+
+
+(*The cut rule*)
+lemma cut: "[| H|-p;  cons(p,H) |- q |] ==>  H |- q"
+apply (rule deduction [THEN thms_MP])
+apply (simp_all add: thms_in_pl)
+done
+
+lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p"
+apply (rule thms.DN [THEN thms_MP])
+apply (rule_tac [2] weaken_right)
+apply (simp_all add: propn.intros)
+done
+
+(* [| H |- p=>Fls;  H |- p;  q \<in> propn |] ==> H |- q *)
+lemmas thms_notE = thms_MP [THEN thms_FlsE, standard]
+
+(*Soundness of the rules wrt truth-table semantics*)
+lemma soundness: "H |- p ==> H |= p"
+apply (unfold logcon_def)
+apply (erule thms.induct)
+apply auto
+done
+
+(*** Towards the completeness proof ***)
+
+lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q"
+apply (frule thms_in_pl)
+apply (rule deduction)
+apply (rule weaken_left_cons [THEN thms_notE]) 
+apply (blast intro: thms.H elim: ImpE)+
+done
+
+lemma Imp_Fls: "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
+apply (frule thms_in_pl)
+apply (frule thms_in_pl [of concl: "q=>Fls"])
+apply (rule deduction)
+apply (erule weaken_left_cons [THEN thms_MP])
+apply (rule consI1 [THEN thms.H, THEN thms_MP])
+apply (blast intro: weaken_left_cons elim: ImpE)+
+done
+
+(*Typical example of strengthening the induction formula*)
+lemma hyps_thms_if:
+     "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
+apply (simp (no_asm))
+apply (induct_tac "p")
+apply (simp_all (no_asm_simp) add: thms_I thms.H)
+apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] 
+                   Fls_Imp [THEN weaken_left_Un2])
+apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
+done
+
+(*Key lemma for completeness; yields a set of assumptions satisfying p*)
+lemma logcon_thms_p: "[| p \<in> propn;  0 |= p |] ==> hyps(p,t) |- p"
+apply (unfold logcon_def)
+apply (drule hyps_thms_if)
+apply simp
+done
+
+
+(*For proving certain theorems in our new propositional logic*)
+lemmas propn_SIs = propn.intros deduction
+lemmas propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
+
+
+(*The excluded middle in the form of an elimination rule*)
+lemma thms_excluded_middle:
+     "[| p \<in> propn;  q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
+apply (rule deduction [THEN deduction])
+apply (rule thms.DN [THEN thms_MP])
+apply (best intro!: propn_SIs intro: propn_Is)+
+done
+
+(*Hard to prove directly because it requires cuts*)
+lemma thms_excluded_middle_rule:
+     "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \<in> propn |] ==> H |- q"
+apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
+apply (blast intro!: propn_SIs intro: propn_Is)+
+done
+
+
+(*** 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}) *)
+lemma hyps_Diff:
+     "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
+by (induct_tac "p", auto)
+
+(*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)) *)
+lemma hyps_cons:
+     "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
+by (induct_tac "p", auto)
+
+(** Two lemmas for use with weaken_left **)
+
+lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
+by blast
+
+lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
+by blast
+
+(*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))*)
+lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
+by (induct_tac "p", auto)
+
+lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
+
+(*Induction on the finite set of assumptions hyps(p,t0).
+  We may repeatedly subtract assumptions until none are left!*)
+lemma completeness_0_lemma [rule_format]:
+    "[| p \<in> propn;  0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
+apply (frule hyps_finite)
+apply (erule Fin_induct)
+apply (simp add: logcon_thms_p Diff_0)
+(*inductive step*)
+apply safe
+(*Case hyps(p,t)-cons(#v,Y) |- p *)
+ apply (rule thms_excluded_middle_rule)
+   apply (erule_tac [3] propn.intros)
+  apply (blast intro: cons_Diff_same [THEN weaken_left])
+ apply (blast intro: cons_Diff_subset2 [THEN weaken_left] 
+		     hyps_Diff [THEN Diff_weaken_left])
+(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
+apply (rule thms_excluded_middle_rule)
+  apply (erule_tac [3] propn.intros)
+ apply (blast intro: cons_Diff_subset2 [THEN weaken_left] 
+		     hyps_cons [THEN Diff_weaken_left])
+apply (blast intro: cons_Diff_same [THEN weaken_left])
+done
+
+(*The base case for completeness*)
+lemma completeness_0: "[| p \<in> propn;  0 |= p |] ==> 0 |- p"
+apply (rule Diff_cancel [THEN subst])
+apply (blast intro: completeness_0_lemma) 
+done
+
+(*A semantic analogue of the Deduction Theorem*)
+lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
+by (simp add: logcon_def)
+
+lemma completeness [rule_format]:
+     "H \<in> Fin(propn) ==> \<forall>p \<in> propn. H |= p --> H |- p"
+apply (erule Fin_induct)
+apply (safe intro!: completeness_0)
+apply (rule weaken_left_cons [THEN thms_MP])
+ apply (blast intro!: logcon_Imp propn.intros)
+apply (blast intro: propn_Is)
+done
+
+lemma thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p & p \<in> propn"
+by (blast intro: soundness completeness thms_in_pl)
+
 end
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Rmap.ML
--- a/src/ZF/Induct/Rmap.ML	Thu Dec 20 15:00:02 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";
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Rmap.thy	Thu Dec 20 15:17:48 2001 +0100
@@ -6,20 +6,66 @@
 Inductive definition of an operator to "map" a relation over a list
 *)
 
-Rmap = Main +
+theory Rmap = Main:
 
 consts
-  rmap :: i=>i
+  rmap :: "i=>i"
 
 inductive
   domains "rmap(r)" <= "list(domain(r))*list(range(r))"
-  intrs
-    NilI  "<Nil,Nil> \\<in> rmap(r)"
+  intros
+    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_intros domainI rangeI list.intros
+
+lemma rmap_mono: "r \<subseteq> s ==> rmap(r) \<subseteq> rmap(s)"
+apply (unfold rmap.defs )
+apply (rule lfp_mono)
+apply (rule rmap.bnd_mono)+
+apply (assumption | 
+       rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
+done
+
+inductive_cases Nil_rmap_case  [elim!]: "<Nil,zs> \<in> rmap(r)"
+inductive_cases Cons_rmap_case [elim!]: "<Cons(x,xs),zs> \<in> rmap(r)"
+
+declare rmap.intros [intro]
+
+lemma rmap_rel_type: "r \<subseteq> A*B ==> rmap(r) \<subseteq> list(A)*list(B)"
+apply (rule rmap.dom_subset [THEN subset_trans])
+apply (assumption | 
+       rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
+done
 
-    ConsI "[| <x,y>: r;  <xs,ys> \\<in> rmap(r) |] ==> 
-          <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)"
+lemma rmap_total: "A \<subseteq> domain(r) ==> list(A) \<subseteq> domain(rmap(r))"
+apply (rule subsetI)
+apply (erule list.induct)
+apply blast+
+done
+
+lemma rmap_functional: "function(r) ==> function(rmap(r))"
+apply (unfold function_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule rmap.induct)
+apply blast+
+done
 
-  type_intrs "[domainI,rangeI] @ list.intrs"
+
+(** If f is a function then rmap(f) behaves as expected. **)
+
+lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
+by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
+
+lemma rmap_Nil: "rmap(f)`Nil = Nil"
+by (unfold apply_def, blast)
+
+lemma rmap_Cons: "[| f \<in> A->B;  x \<in> A;  xs: list(A) |]   
+      ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
+by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
+
 
 end
   
diff -r 7fb12775ce98 -r 5820841f21fd src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/IsaMakefile	Thu Dec 20 15:17:48 2001 +0100
@@ -122,13 +122,11 @@
 
 ZF-Induct: ZF $(LOG)/ZF-Induct.gz
 
-$(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
-  Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.ML Induct/Comb.thy \
-  Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML \
+$(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.thy \
+  Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
+  Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy \
   Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
-  Induct/Ntree.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 \
+  Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
   Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/ZF Induct