ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
authorlcp
Thu Sep 30 10:54:01 1993 +0100 (1993-09-30)
changeset 160b033d50ca1c
parent 15 6c6d2f6e3185
child 17 b35851cafd3e
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
called expandshort
src/ZF/ex/Bin.ML
src/ZF/ex/Comb.ML
src/ZF/ex/Contract0.ML
src/ZF/ex/Contract0.thy
src/ZF/ex/Integ.ML
src/ZF/ex/LList.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Primrec0.ML
src/ZF/ex/Primrec0.thy
src/ZF/ex/Prop.ML
src/ZF/ex/PropLog.ML
src/ZF/ex/ROOT.ML
src/ZF/ex/Rmap.ML
src/ZF/ex/Term.ML
src/ZF/ex/bin.ML
src/ZF/ex/comb.ML
src/ZF/ex/contract0.ML
src/ZF/ex/contract0.thy
src/ZF/ex/integ.ML
src/ZF/ex/listn.ML
src/ZF/ex/llist.ML
src/ZF/ex/misc.ML
src/ZF/ex/primrec0.ML
src/ZF/ex/primrec0.thy
src/ZF/ex/prop.ML
src/ZF/ex/proplog.ML
src/ZF/ex/rmap.ML
src/ZF/ex/term.ML
     1.1 --- a/src/ZF/ex/Bin.ML	Thu Sep 30 10:26:38 1993 +0100
     1.2 +++ b/src/ZF/ex/Bin.ML	Thu Sep 30 10:54:01 1993 +0100
     1.3 @@ -14,18 +14,7 @@
     1.4  	  [(["Plus", "Minus"],	"i"),
     1.5  	   (["op $$"],		"[i,i]=>i")])];
     1.6    val rec_styp = "i";
     1.7 -  val ext = Some (NewSext {
     1.8 -	     mixfix =
     1.9 -	      [Infixl("$$", "[i,i] => i", 60)],
    1.10 -	     xrules = [],
    1.11 -	     parse_ast_translation = [],
    1.12 -	     parse_preproc = None,
    1.13 -	     parse_postproc = None,
    1.14 -	     parse_translation = [],
    1.15 -	     print_translation = [],
    1.16 -	     print_preproc = None,
    1.17 -	     print_postproc = None,
    1.18 -	     print_ast_translation = []});
    1.19 +  val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
    1.20    val sintrs = 
    1.21  	  ["Plus : bin",
    1.22  	   "Minus : bin",
     2.1 --- a/src/ZF/ex/Comb.ML	Thu Sep 30 10:26:38 1993 +0100
     2.2 +++ b/src/ZF/ex/Comb.ML	Thu Sep 30 10:54:01 1993 +0100
     2.3 @@ -19,18 +19,7 @@
     2.4  	  [(["K","S"],	"i"),
     2.5  	   (["op #"],	"[i,i]=>i")])];
     2.6    val rec_styp = "i";
     2.7 -  val ext = Some (NewSext {
     2.8 -	     mixfix =
     2.9 -	      [Infixl("#", "[i,i] => i", 90)],
    2.10 -	     xrules = [],
    2.11 -	     parse_ast_translation = [],
    2.12 -	     parse_preproc = None,
    2.13 -	     parse_postproc = None,
    2.14 -	     parse_translation = [],
    2.15 -	     print_translation = [],
    2.16 -	     print_preproc = None,
    2.17 -	     print_postproc = None,
    2.18 -	     print_ast_translation = []});
    2.19 +  val ext = Some (Syntax.simple_sext [Infixl("#", "[i,i] => i", 90)]);
    2.20    val sintrs = 
    2.21  	  ["K : comb",
    2.22  	   "S : comb",
     3.1 --- a/src/ZF/ex/Contract0.ML	Thu Sep 30 10:26:38 1993 +0100
     3.2 +++ b/src/ZF/ex/Contract0.ML	Thu Sep 30 10:54:01 1993 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title: 	ZF/ex/contract.ML
     3.5      ID:         $Id$
     3.6 -    Author: 	Tobias Nipkow & Lawrence C Paulson
     3.7 -    Copyright   1992  University of Cambridge
     3.8 +    Author: 	Lawrence C Paulson
     3.9 +    Copyright   1993  University of Cambridge
    3.10  
    3.11  For ex/contract.thy.
    3.12  *)
     4.1 --- a/src/ZF/ex/Contract0.thy	Thu Sep 30 10:26:38 1993 +0100
     4.2 +++ b/src/ZF/ex/Contract0.thy	Thu Sep 30 10:54:01 1993 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  (*  Title: 	ZF/ex/contract.thy
     4.5      ID:         $Id$
     4.6 -    Author: 	Tobias Nipkow & Lawrence C Paulson
     4.7 +    Author: 	Lawrence C Paulson
     4.8      Copyright   1993  University of Cambridge
     4.9  
    4.10  Inductive definition of (1-step) contractions and (mult-step) reductions
     5.1 --- a/src/ZF/ex/Integ.ML	Thu Sep 30 10:26:38 1993 +0100
     5.2 +++ b/src/ZF/ex/Integ.ML	Thu Sep 30 10:54:01 1993 +0100
     5.3 @@ -185,7 +185,7 @@
     5.4      "n: nat ==> znegative($~ $# succ(n))";
     5.5  by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
     5.6  by (REPEAT 
     5.7 -    (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
     5.8 +    (resolve_tac [refl, exI, conjI, nat_0_in_succ,
     5.9  		  refl RS intrelI RS imageI, consI1, nnat, nat_0I,
    5.10  		  nat_succI] 1));
    5.11  val znegative_zminus_znat = result();
    5.12 @@ -377,7 +377,7 @@
    5.13  by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
    5.14  val zmult_0 = result();
    5.15  
    5.16 -goalw Integ.thy [integ_def,znat_def,one_def]
    5.17 +goalw Integ.thy [integ_def,znat_def]
    5.18      "!!z. z : integ ==> $#1 $* z = z";
    5.19  by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
    5.20  by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
     6.1 --- a/src/ZF/ex/LList.ML	Thu Sep 30 10:26:38 1993 +0100
     6.2 +++ b/src/ZF/ex/LList.ML	Thu Sep 30 10:54:01 1993 +0100
     6.3 @@ -55,10 +55,10 @@
     6.4  goal LList.thy
     6.5     "!!i. i : nat ==> 	\
     6.6  \        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
     6.7 -be complete_induct 1;
     6.8 -br ballI 1;
     6.9 -be LList.elim 1;
    6.10 -bws ([QInl_def,QInr_def]@LList.con_defs);
    6.11 +by (etac complete_induct 1);
    6.12 +by (rtac ballI 1);
    6.13 +by (etac LList.elim 1);
    6.14 +by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    6.15  by (fast_tac quniv_cs 1);
    6.16  by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
    6.17  by (fast_tac quniv_cs 1);
    6.18 @@ -66,9 +66,9 @@
    6.19  val llist_quniv_lemma = result();
    6.20  
    6.21  goal LList.thy "llist(quniv(A)) <= quniv(A)";
    6.22 -br subsetI 1;
    6.23 -br quniv_Int_Vfrom 1;
    6.24 -be (LList.dom_subset RS subsetD) 1;
    6.25 +by (rtac subsetI 1);
    6.26 +by (rtac quniv_Int_Vfrom 1);
    6.27 +by (etac (LList.dom_subset RS subsetD) 1);
    6.28  by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
    6.29  val llist_quniv = result();
    6.30  
    6.31 @@ -102,20 +102,20 @@
    6.32  (*Keep unfolding the lazy list until the induction hypothesis applies*)
    6.33  goal LList_Eq.thy
    6.34     "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
    6.35 -be trans_induct 1;
    6.36 +by (etac trans_induct 1);
    6.37  by (safe_tac subset_cs);
    6.38 -be LList_Eq.elim 1;
    6.39 +by (etac LList_Eq.elim 1);
    6.40  by (safe_tac (subset_cs addSEs [QPair_inject]));
    6.41 -bws LList.con_defs;
    6.42 +by (rewrite_goals_tac LList.con_defs);
    6.43  by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    6.44  (*0 case*)
    6.45  by (fast_tac lleq_cs 1);
    6.46  (*succ(j) case*)
    6.47 -bw QInr_def;
    6.48 +by (rewtac QInr_def);
    6.49  by (fast_tac lleq_cs 1);
    6.50  (*Limit(i) case*)
    6.51 -be (Limit_Vfrom_eq RS ssubst) 1;
    6.52 -br (Int_UN_distrib RS ssubst) 1;
    6.53 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
    6.54 +by (rtac (Int_UN_distrib RS ssubst) 1);
    6.55  by (fast_tac lleq_cs 1);
    6.56  val lleq_Int_Vset_subset_lemma = result();
    6.57  
    6.58 @@ -125,15 +125,15 @@
    6.59  
    6.60  (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    6.61  val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
    6.62 -br (prem RS qconverseI RS LList_Eq.co_induct) 1;
    6.63 -br (LList_Eq.dom_subset RS qconverse_type) 1;
    6.64 +by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
    6.65 +by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
    6.66  by (safe_tac qconverse_cs);
    6.67 -be LList_Eq.elim 1;
    6.68 +by (etac LList_Eq.elim 1);
    6.69  by (ALLGOALS (fast_tac qconverse_cs));
    6.70  val lleq_symmetric = result();
    6.71  
    6.72  goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
    6.73 -br equalityI 1;
    6.74 +by (rtac equalityI 1);
    6.75  by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    6.76       ORELSE etac lleq_symmetric 1));
    6.77  val lleq_implies_equal = result();
    6.78 @@ -141,9 +141,9 @@
    6.79  val [eqprem,lprem] = goal LList_Eq.thy
    6.80      "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
    6.81  by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
    6.82 -br (lprem RS RepFunI RS (eqprem RS subst)) 1;
    6.83 +by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
    6.84  by (safe_tac qpair_cs);
    6.85 -be LList.elim 1;
    6.86 +by (etac LList.elim 1);
    6.87  by (ALLGOALS (fast_tac qpair_cs));
    6.88  val equal_llist_implies_leq = result();
    6.89  
     7.1 --- a/src/ZF/ex/ListN.ML	Thu Sep 30 10:26:38 1993 +0100
     7.2 +++ b/src/ZF/ex/ListN.ML	Thu Sep 30 10:54:01 1993 +0100
     7.3 @@ -41,3 +41,9 @@
     7.4  by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
     7.5  val listn_image_eq = result();
     7.6  
     7.7 +goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
     7.8 +by (rtac lfp_mono 1);
     7.9 +by (REPEAT (rtac ListN.bnd_mono 1));
    7.10 +by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
    7.11 +val listn_mono = result();
    7.12 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/ex/Primrec0.ML	Thu Sep 30 10:54:01 1993 +0100
     8.3 @@ -0,0 +1,414 @@
     8.4 +(*  Title: 	ZF/ex/primrec
     8.5 +    ID:         $Id$
     8.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Copyright   1993  University of Cambridge
     8.8 +
     8.9 +Primitive Recursive Functions
    8.10 +
    8.11 +Proof adopted from
    8.12 +Nora Szasz, 
    8.13 +A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    8.14 +In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    8.15 +*)
    8.16 +
    8.17 +open Primrec0;
    8.18 +
    8.19 +val pr0_typechecks = 
    8.20 +    nat_typechecks @ List.intrs @ 
    8.21 +    [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
    8.22 +
    8.23 +(** Useful special cases of evaluation ***)
    8.24 +
    8.25 +val pr0_ss = arith_ss 
    8.26 +    addsimps List.case_eqns
    8.27 +    addsimps [list_rec_Nil, list_rec_Cons, 
    8.28 +	      drop_0, drop_Nil, drop_succ_Cons,
    8.29 +	      map_Nil, map_Cons]
    8.30 +    setsolver (type_auto_tac pr0_typechecks);
    8.31 +
    8.32 +goalw Primrec0.thy [SC_def]
    8.33 +    "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
    8.34 +by (asm_simp_tac pr0_ss 1);
    8.35 +val SC = result();
    8.36 +
    8.37 +goalw Primrec0.thy [CONST_def]
    8.38 +    "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
    8.39 +by (asm_simp_tac pr0_ss 1);
    8.40 +val CONST = result();
    8.41 +
    8.42 +goalw Primrec0.thy [PROJ_def]
    8.43 +    "!!l. [| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
    8.44 +by (asm_simp_tac pr0_ss 1);
    8.45 +val PROJ_0 = result();
    8.46 +
    8.47 +goalw Primrec0.thy [COMP_def]
    8.48 +    "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
    8.49 +by (asm_simp_tac pr0_ss 1);
    8.50 +val COMP_1 = result();
    8.51 +
    8.52 +goalw Primrec0.thy [PREC_def]
    8.53 +    "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
    8.54 +by (asm_simp_tac pr0_ss 1);
    8.55 +val PREC_0 = result();
    8.56 +
    8.57 +goalw Primrec0.thy [PREC_def]
    8.58 +    "!!l. [| x:nat;  l: list(nat) |] ==>  \
    8.59 +\         PREC(f,g) ` (Cons(succ(x),l)) = \
    8.60 +\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
    8.61 +by (asm_simp_tac pr0_ss 1);
    8.62 +val PREC_succ = result();
    8.63 +
    8.64 +(*** Inductive definition of the PR functions ***)
    8.65 +
    8.66 +structure Primrec = Inductive_Fun
    8.67 + (val thy = Primrec0.thy;
    8.68 +  val rec_doms = [("primrec", "list(nat)->nat")];
    8.69 +  val ext = None
    8.70 +  val sintrs = 
    8.71 +      ["SC : primrec",
    8.72 +       "k: nat ==> CONST(k) : primrec",
    8.73 +       "i: nat ==> PROJ(i) : primrec",
    8.74 +       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
    8.75 +       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
    8.76 +  val monos = [list_mono];
    8.77 +  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
    8.78 +  val type_intrs = pr0_typechecks
    8.79 +  val type_elims = []);
    8.80 +
    8.81 +(* c: primrec ==> c: list(nat) -> nat *)
    8.82 +val primrec_into_fun = Primrec.dom_subset RS subsetD;
    8.83 +
    8.84 +val pr_ss = pr0_ss 
    8.85 +    setsolver (type_auto_tac ([primrec_into_fun] @ 
    8.86 +			      pr0_typechecks @ Primrec.intrs));
    8.87 +
    8.88 +goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
    8.89 +by (etac nat_induct 1);
    8.90 +by (ALLGOALS (asm_simp_tac pr_ss));
    8.91 +val ACK_in_primrec = result();
    8.92 +
    8.93 +val ack_typechecks =
    8.94 +    [ACK_in_primrec, primrec_into_fun RS apply_type,
    8.95 +     add_type, list_add_type, naturals_are_ordinals] @ 
    8.96 +    nat_typechecks @ List.intrs @ Primrec.intrs;
    8.97 +
    8.98 +(*strict typechecking for the Ackermann proof; instantiates no vars*)
    8.99 +fun tc_tac rls =
   8.100 +    REPEAT
   8.101 +      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
   8.102 +
   8.103 +goal Primrec.thy "!!i j. [| i:nat;  j:nat |] ==>  ack(i,j): nat";
   8.104 +by (tc_tac []);
   8.105 +val ack_type = result();
   8.106 +
   8.107 +(** Ackermann's function cases **)
   8.108 +
   8.109 +(*PROPERTY A 1*)
   8.110 +goalw Primrec0.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
   8.111 +by (asm_simp_tac (pr0_ss addsimps [SC]) 1);
   8.112 +val ack_0 = result();
   8.113 +
   8.114 +(*PROPERTY A 2*)
   8.115 +goalw Primrec0.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
   8.116 +by (asm_simp_tac (pr0_ss addsimps [CONST,PREC_0]) 1);
   8.117 +val ack_succ_0 = result();
   8.118 +
   8.119 +(*PROPERTY A 3*)
   8.120 +(*Could be proved in Primrec0, like the previous two cases, but using
   8.121 +  primrec_into_fun makes type-checking easier!*)
   8.122 +goalw Primrec.thy [ACK_def]
   8.123 +    "!!i j. [| i:nat;  j:nat |] ==> \
   8.124 +\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
   8.125 +by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
   8.126 +val ack_succ_succ = result();
   8.127 +
   8.128 +val ack_ss = 
   8.129 +    pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, 
   8.130 +		    ack_type, naturals_are_ordinals];
   8.131 +
   8.132 +(*PROPERTY A 4*)
   8.133 +goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j : ack(i,j)";
   8.134 +by (etac nat_induct 1);
   8.135 +by (asm_simp_tac ack_ss 1);
   8.136 +by (rtac ballI 1);
   8.137 +by (eres_inst_tac [("n","j")] nat_induct 1);
   8.138 +by (ALLGOALS (asm_simp_tac ack_ss));
   8.139 +by (rtac ([succI1, asm_rl,naturals_are_ordinals] MRS Ord_trans) 1);
   8.140 +by (rtac (succ_mem_succI RS Ord_trans1) 3);
   8.141 +by (etac bspec 5);
   8.142 +by (ALLGOALS (asm_simp_tac ack_ss));
   8.143 +val less_ack2_lemma = result();
   8.144 +val less_ack2 = standard (less_ack2_lemma RS bspec);
   8.145 +
   8.146 +(*PROPERTY A 5-, the single-step lemma*)
   8.147 +goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(i, succ(j))";
   8.148 +by (etac nat_induct 1);
   8.149 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [less_ack2])));
   8.150 +val ack_less_ack_succ2 = result();
   8.151 +
   8.152 +(*PROPERTY A 5, monotonicity for < *)
   8.153 +goal Primrec.thy "!!i j k. [| j:k; i:nat; k:nat |] ==> ack(i,j) : ack(i,k)";
   8.154 +by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
   8.155 +by (assume_tac 1);
   8.156 +by (etac succ_less_induct 1);
   8.157 +by (assume_tac 1);
   8.158 +by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
   8.159 +by (REPEAT (ares_tac ([ack_less_ack_succ2, ack_type] @ pr0_typechecks) 1));
   8.160 +val ack_less_mono2 = result();
   8.161 +
   8.162 +(*PROPERTY A 5', monotonicity for <= *)
   8.163 +goal Primrec.thy
   8.164 +    "!!i j k. [| j<=k; i:nat; j:nat; k:nat |] ==> ack(i,j) <= ack(i,k)";
   8.165 +by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_less_mono_imp_mono 1);
   8.166 +by (REPEAT (ares_tac [ack_less_mono2, ack_type, Ord_nat] 1));
   8.167 +val ack_mono2 = result();
   8.168 +
   8.169 +(*PROPERTY A 6*)
   8.170 +goal Primrec.thy
   8.171 +    "!!i j. [| i:nat;  j:nat |] ==> ack(i, succ(j)) <= ack(succ(i), j)";
   8.172 +by (nat_ind_tac "j" [] 1);
   8.173 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [subset_refl])));
   8.174 +by (rtac ack_mono2 1);
   8.175 +by (rtac (less_ack2 RS Ord_succ_subsetI RS subset_trans) 1);
   8.176 +by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type] @ pr0_typechecks) 1));
   8.177 +val ack2_leq_ack1 = result();
   8.178 +
   8.179 +(*PROPERTY A 7-, the single-step lemma*)
   8.180 +goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(succ(i),j)";
   8.181 +by (rtac (ack_less_mono2 RS Ord_trans2) 1);
   8.182 +by (rtac (ack2_leq_ack1 RS member_succI) 4);
   8.183 +by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type, succI1] @ 
   8.184 +		      pr0_typechecks) 1));
   8.185 +val ack_less_ack_succ1 = result();
   8.186 +
   8.187 +(*PROPERTY A 7, monotonicity for < *)
   8.188 +goal Primrec.thy "!!i j k. [| i:j; j:nat; k:nat |] ==> ack(i,k) : ack(j,k)";
   8.189 +by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
   8.190 +by (assume_tac 1);
   8.191 +by (etac succ_less_induct 1);
   8.192 +by (assume_tac 1);
   8.193 +by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
   8.194 +by (REPEAT (ares_tac ([ack_less_ack_succ1, ack_type] @ pr0_typechecks) 1));
   8.195 +val ack_less_mono1 = result();
   8.196 +
   8.197 +(*PROPERTY A 7', monotonicity for <= *)
   8.198 +goal Primrec.thy
   8.199 +    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> ack(i,k) <= ack(j,k)";
   8.200 +by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_less_mono_imp_mono 1);
   8.201 +by (REPEAT (ares_tac [ack_less_mono1, ack_type, Ord_nat] 1));
   8.202 +val ack_mono1 = result();
   8.203 +
   8.204 +(*PROPERTY A 8*)
   8.205 +goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
   8.206 +by (etac nat_induct 1);
   8.207 +by (ALLGOALS (asm_simp_tac ack_ss));
   8.208 +val ack_1 = result();
   8.209 +
   8.210 +(*PROPERTY A 9*)
   8.211 +goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
   8.212 +by (etac nat_induct 1);
   8.213 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
   8.214 +val ack_2 = result();
   8.215 +
   8.216 +(*PROPERTY A 10*)
   8.217 +goal Primrec.thy
   8.218 +    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
   8.219 +\               ack(i1, ack(i2,j)) : ack(succ(succ(i1#+i2)), j)";
   8.220 +by (rtac Ord_trans2 1);
   8.221 +by (rtac (ack2_leq_ack1 RS member_succI) 2);
   8.222 +by (asm_simp_tac ack_ss 1);
   8.223 +by (rtac ([ack_mono1 RS member_succI, ack_less_mono2] MRS Ord_trans1) 1);
   8.224 +by (rtac add_leq_self 1);
   8.225 +by (tc_tac []);
   8.226 +by (rtac (add_commute RS ssubst) 1);
   8.227 +by (rtac (add_less_succ_self RS ack_less_mono1) 3);
   8.228 +by (tc_tac []);
   8.229 +val ack_nest_bound = result();
   8.230 +
   8.231 +(*PROPERTY A 11*)
   8.232 +goal Primrec.thy
   8.233 +    "!!i1 i2. [| i1:nat; i2:nat |] ==> \
   8.234 +\             EX k:nat. ALL j:nat. ack(i1,j) #+ ack(i2,j) : ack(k,j)";
   8.235 +by (rtac (Ord_trans RS ballI RS bexI) 1);
   8.236 +by (res_inst_tac [("i1.0", "succ(1)"), ("i2.0", "i1#+i2")] ack_nest_bound 2);
   8.237 +by (rtac (ack_2 RS ssubst) 1);
   8.238 +by (tc_tac []);
   8.239 +by (rtac (member_succI RS succI2 RS succI2) 1);
   8.240 +by (rtac (add_leq_self RS ack_mono1 RS add_mono) 1);
   8.241 +by (tc_tac []);
   8.242 +by (rtac (add_commute RS ssubst) 1);
   8.243 +by (rtac (add_leq_self RS ack_mono1) 3);
   8.244 +by (tc_tac []);
   8.245 +val ack_add_bound = result();
   8.246 +
   8.247 +(*PROPERTY A 12 -- note quantifier nesting
   8.248 +  Article uses existential quantifier but the ALF proof used a concrete
   8.249 +  expression, namely k#+4. *)
   8.250 +goal Primrec.thy
   8.251 +    "!!k. k: nat ==> \
   8.252 +\         EX k':nat. ALL i:nat. ALL j:nat. i : ack(k,j) --> i#+j : ack(k',j)";
   8.253 +by (res_inst_tac [("i1.1", "k"), ("i2.1", "0")] (ack_add_bound RS bexE) 1);
   8.254 +by (rtac (Ord_trans RS impI RS ballI RS ballI RS bexI) 3);
   8.255 +by (etac bspec 4);
   8.256 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [add_less_mono])));
   8.257 +val ack_add_bound2 = result();
   8.258 +
   8.259 +(*** MAIN RESULT ***)
   8.260 +
   8.261 +val ack2_ss =
   8.262 +    ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, 
   8.263 +		     naturals_are_ordinals];
   8.264 +
   8.265 +goalw Primrec.thy [SC_def]
   8.266 +    "!!l. l: list(nat) ==> SC ` l : ack(1, list_add(l))";
   8.267 +by (etac List.elim 1);
   8.268 +by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
   8.269 +by (asm_simp_tac (ack2_ss addsimps 
   8.270 +		  [ack_1, add_less_succ_self RS succ_mem_succI]) 1);
   8.271 +val SC_case = result();
   8.272 +
   8.273 +(*PROPERTY A 4'?? Extra lemma needed for CONST case, constant functions*)
   8.274 +goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i : ack(i,j)";
   8.275 +by (etac nat_induct 1);
   8.276 +by (asm_simp_tac (ack_ss addsimps [nat_0_in_succ]) 1);
   8.277 +by (etac ([succ_mem_succI, ack_less_ack_succ1] MRS Ord_trans1) 1);
   8.278 +by (tc_tac []);
   8.279 +val less_ack1 = result();
   8.280 +
   8.281 +goalw Primrec.thy [CONST_def]
   8.282 +    "!!l. [| l: list(nat);  k: nat |] ==> CONST(k) ` l : ack(k, list_add(l))";
   8.283 +by (asm_simp_tac (ack2_ss addsimps [less_ack1]) 1);
   8.284 +val CONST_case = result();
   8.285 +
   8.286 +goalw Primrec.thy [PROJ_def]
   8.287 +    "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l : ack(0, list_add(l))";
   8.288 +by (asm_simp_tac ack2_ss 1);
   8.289 +by (etac List.induct 1);
   8.290 +by (asm_simp_tac (ack2_ss addsimps [nat_0_in_succ]) 1);
   8.291 +by (asm_simp_tac ack2_ss 1);
   8.292 +by (rtac ballI 1);
   8.293 +by (eres_inst_tac [("n","x")] natE 1);
   8.294 +by (asm_simp_tac (ack2_ss addsimps [add_less_succ_self]) 1);
   8.295 +by (asm_simp_tac ack2_ss 1);
   8.296 +by (etac (bspec RS Ord_trans2) 1);
   8.297 +by (assume_tac 1);
   8.298 +by (rtac (add_commute RS ssubst) 1);
   8.299 +by (rtac (add_less_succ_self RS succ_mem_succI) 3);
   8.300 +by (tc_tac [list_add_type]);
   8.301 +val PROJ_case_lemma = result();
   8.302 +val PROJ_case = PROJ_case_lemma RS bspec;
   8.303 +
   8.304 +(** COMP case **)
   8.305 +
   8.306 +goal Primrec.thy
   8.307 + "!!fs. fs : list({f: primrec .					\
   8.308 +\              	   EX kf:nat. ALL l:list(nat). 			\
   8.309 +\		    	      f`l : ack(kf, list_add(l))})	\
   8.310 +\      ==> EX k:nat. ALL l: list(nat). 				\
   8.311 +\                list_add(map(%f. f ` l, fs)) : ack(k, list_add(l))";
   8.312 +by (etac List.induct 1);
   8.313 +by (DO_GOAL [res_inst_tac [("x","0")] bexI,
   8.314 +	     asm_simp_tac (ack2_ss addsimps [less_ack1,nat_0_in_succ]),
   8.315 +	     resolve_tac nat_typechecks] 1);
   8.316 +by (safe_tac ZF_cs);
   8.317 +by (asm_simp_tac ack2_ss 1);
   8.318 +by (res_inst_tac [("i1.1", "kf"), ("i2.1", "k")] (ack_add_bound RS bexE) 1
   8.319 +    THEN REPEAT (assume_tac 1));
   8.320 +by (rtac (ballI RS bexI) 1);
   8.321 +by (etac (bspec RS add_less_mono RS Ord_trans) 1);
   8.322 +by (REPEAT (FIRSTGOAL (etac bspec)));
   8.323 +by (tc_tac [list_add_type]);
   8.324 +val COMP_map_lemma = result();
   8.325 +
   8.326 +goalw Primrec.thy [COMP_def]
   8.327 + "!!g. [| g: primrec;  kg: nat;					\
   8.328 +\         ALL l:list(nat). g`l : ack(kg, list_add(l));		\
   8.329 +\         fs : list({f: primrec .				\
   8.330 +\                    EX kf:nat. ALL l:list(nat). 		\
   8.331 +\		    	f`l : ack(kf, list_add(l))}) 		\
   8.332 +\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l : ack(k, list_add(l))";
   8.333 +by (asm_simp_tac ZF_ss 1);
   8.334 +by (forward_tac [list_CollectD] 1);
   8.335 +by (etac (COMP_map_lemma RS bexE) 1);
   8.336 +by (rtac (ballI RS bexI) 1);
   8.337 +by (etac (bspec RS Ord_trans) 1);
   8.338 +by (rtac Ord_trans 2);
   8.339 +by (rtac ack_nest_bound 3);
   8.340 +by (etac (bspec RS ack_less_mono2) 2);
   8.341 +by (tc_tac [map_type]);
   8.342 +val COMP_case = result();
   8.343 +
   8.344 +(** PREC case **)
   8.345 +
   8.346 +goalw Primrec.thy [PREC_def]
   8.347 + "!!f g. [| f: primrec;  kf: nat;					\
   8.348 +\           g: primrec;  kg: nat;					\
   8.349 +\           ALL l:list(nat). f`l #+ list_add(l) : ack(kf, list_add(l));	\
   8.350 +\           ALL l:list(nat). g`l #+ list_add(l) : ack(kg, list_add(l));	\
   8.351 +\           l: list(nat)						\
   8.352 +\        |] ==> PREC(f,g)`l #+ list_add(l) : ack(succ(kf#+kg), list_add(l))";
   8.353 +by (etac List.elim 1);
   8.354 +by (asm_simp_tac (ack2_ss addsimps [[succI1, less_ack2] MRS Ord_trans]) 1);
   8.355 +by (asm_simp_tac ack2_ss 1);
   8.356 +be ssubst 1;  (*get rid of the needless assumption*)
   8.357 +by (eres_inst_tac [("n","a")] nat_induct 1);
   8.358 +by (asm_simp_tac ack2_ss 1);
   8.359 +by (rtac Ord_trans 1);
   8.360 +by (etac bspec 1);
   8.361 +by (assume_tac 1);
   8.362 +by (rtac ack_less_mono1 1);
   8.363 +by (rtac add_less_succ_self 1);
   8.364 +by (tc_tac [list_add_type]);
   8.365 +(*ind step -- level 13*)
   8.366 +by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
   8.367 +by (rtac (succ_mem_succI RS Ord_trans1) 1);
   8.368 +by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] Ord_trans1 1);
   8.369 +by (etac bspec 2);
   8.370 +by (rtac (subset_refl RS add_mono RS member_succI) 1);
   8.371 +by (tc_tac []);
   8.372 +by (asm_simp_tac (ack2_ss addsimps [add_leq_self2]) 1);
   8.373 +by (asm_simp_tac ack2_ss 1);
   8.374 +(*final part of the simplification*)
   8.375 +by (rtac (member_succI RS Ord_trans1) 1);
   8.376 +by (rtac (add_leq_self2 RS ack_mono1) 1);
   8.377 +by (etac ack_less_mono2 8);
   8.378 +by (tc_tac []);
   8.379 +val PREC_case_lemma = result();
   8.380 +
   8.381 +goal Primrec.thy
   8.382 + "!!f g. [| f: primrec;  kf: nat;				\
   8.383 +\           g: primrec;  kg: nat;				\
   8.384 +\           ALL l:list(nat). f`l : ack(kf, list_add(l));	\
   8.385 +\           ALL l:list(nat). g`l : ack(kg, list_add(l)) 	\
   8.386 +\        |] ==> EX k:nat. ALL l: list(nat). 			\
   8.387 +\		    PREC(f,g)`l: ack(k, list_add(l))";
   8.388 +by (etac (ack_add_bound2 RS bexE) 1);
   8.389 +by (etac (ack_add_bound2 RS bexE) 1);
   8.390 +by (rtac (ballI RS bexI) 1);
   8.391 +by (rtac ([add_leq_self RS member_succI, PREC_case_lemma] MRS Ord_trans1) 1);
   8.392 +by (DEPTH_SOLVE
   8.393 +    (SOMEGOAL
   8.394 +     (FIRST' [test_assume_tac,
   8.395 +	      match_tac (ballI::ack_typechecks),
   8.396 +	      eresolve_tac [bspec, bspec RS bspec RS mp]])));
   8.397 +val PREC_case = result();
   8.398 +
   8.399 +goal Primrec.thy
   8.400 +    "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l : ack(k, list_add(l))";
   8.401 +by (etac Primrec.induct 1);
   8.402 +by (safe_tac ZF_cs);
   8.403 +by (DEPTH_SOLVE
   8.404 +    (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
   8.405 +		       bexI, ballI] @ nat_typechecks) 1));
   8.406 +val ack_bounds_primrec = result();
   8.407 +
   8.408 +goal Primrec.thy
   8.409 +    "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
   8.410 +by (rtac notI 1);
   8.411 +by (etac (ack_bounds_primrec RS bexE) 1);
   8.412 +by (rtac mem_anti_refl 1);
   8.413 +by (dres_inst_tac [("x", "[x]")] bspec 1);
   8.414 +by (asm_simp_tac ack2_ss 1);
   8.415 +by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
   8.416 +val ack_not_primrec = result();
   8.417 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/ZF/ex/Primrec0.thy	Thu Sep 30 10:54:01 1993 +0100
     9.3 @@ -0,0 +1,46 @@
     9.4 +(*  Title: 	ZF/ex/primrec.thy
     9.5 +    ID:         $Id$
     9.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   1993  University of Cambridge
     9.8 +
     9.9 +Primitive Recursive Functions
    9.10 +
    9.11 +Proof adopted from
    9.12 +Nora Szasz, 
    9.13 +A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    9.14 +In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    9.15 +*)
    9.16 +
    9.17 +Primrec0 = ListFn +
    9.18 +consts
    9.19 +    SC      :: "i"
    9.20 +    CONST   :: "i=>i"
    9.21 +    PROJ    :: "i=>i"
    9.22 +    COMP    :: "[i,i]=>i"
    9.23 +    PREC    :: "[i,i]=>i"
    9.24 +    primrec :: "i"
    9.25 +    ACK	    :: "i=>i"
    9.26 +    ack	    :: "[i,i]=>i"
    9.27 +
    9.28 +translations
    9.29 +  "ack(x,y)"  == "ACK(x) ` [y]"
    9.30 +
    9.31 +rules
    9.32 +
    9.33 +  SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
    9.34 +
    9.35 +  CONST_def "CONST(k) == lam l:list(nat).k"
    9.36 +
    9.37 +  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
    9.38 +
    9.39 +  COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
    9.40 +
    9.41 +  (*Note that g is applied first to PREC(f,g)`y and then to y!*)
    9.42 +  PREC_def  "PREC(f,g) == \
    9.43 +\            lam l:list(nat). list_case(0, \
    9.44 +\                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
    9.45 +  
    9.46 +  ACK_def   "ACK(i) == rec(i, SC, \
    9.47 +\                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
    9.48 +
    9.49 +end
    10.1 --- a/src/ZF/ex/Prop.ML	Thu Sep 30 10:26:38 1993 +0100
    10.2 +++ b/src/ZF/ex/Prop.ML	Thu Sep 30 10:54:01 1993 +0100
    10.3 @@ -16,19 +16,9 @@
    10.4  	   (["Var"],	"i=>i"),
    10.5  	   (["op =>"],	"[i,i]=>i")])];
    10.6    val rec_styp = "i";
    10.7 -  val ext = Some (NewSext {
    10.8 -	     mixfix =
    10.9 -	      [Mixfix("#_", "i => i", "Var", [100], 100),
   10.10 -	       Infixr("=>", "[i,i] => i", 90)],
   10.11 -	     xrules = [],
   10.12 -	     parse_ast_translation = [],
   10.13 -	     parse_preproc = None,
   10.14 -	     parse_postproc = None,
   10.15 -	     parse_translation = [],
   10.16 -	     print_translation = [],
   10.17 -	     print_preproc = None,
   10.18 -	     print_postproc = None,
   10.19 -	     print_ast_translation = []});
   10.20 +  val ext = Some (Syntax.simple_sext
   10.21 +		    [Mixfix("#_", "i => i", "Var", [100], 100),
   10.22 +		     Infixr("=>", "[i,i] => i", 90)]);
   10.23    val sintrs = 
   10.24  	  ["Fls : prop",
   10.25  	   "n: nat ==> #n : prop",
    11.1 --- a/src/ZF/ex/PropLog.ML	Thu Sep 30 10:26:38 1993 +0100
    11.2 +++ b/src/ZF/ex/PropLog.ML	Thu Sep 30 10:54:01 1993 +0100
    11.3 @@ -190,9 +190,10 @@
    11.4  by (rtac (expand_if RS iffD2) 1);
    11.5  by (rtac (major RS Prop.induct) 1);
    11.6  by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
    11.7 -by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
    11.8 -			   weaken_right, Imp_Fls]
    11.9 -                    addSEs [Fls_Imp]) 1);
   11.10 +by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, 
   11.11 +			    Fls_Imp RS weaken_left_Un2]));
   11.12 +by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
   11.13 +				     weaken_right, Imp_Fls])));
   11.14  val hyps_thms_if = result();
   11.15  
   11.16  (*Key lemma for completeness; yields a set of assumptions satisfying p*)
   11.17 @@ -264,7 +265,7 @@
   11.18  val [major] = goal PropThms.thy
   11.19      "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
   11.20  by (rtac (major RS Prop.induct) 1);
   11.21 -by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I] 
   11.22 +by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I, cons_iff]
   11.23  		  setloop (split_tac [expand_if])) 2);
   11.24  by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
   11.25  val hyps_finite = result();
   11.26 @@ -324,5 +325,3 @@
   11.27  val thms_iff = result();
   11.28  
   11.29  writeln"Reached end of file.";
   11.30 -
   11.31 -
    12.1 --- a/src/ZF/ex/ROOT.ML	Thu Sep 30 10:26:38 1993 +0100
    12.2 +++ b/src/ZF/ex/ROOT.ML	Thu Sep 30 10:54:01 1993 +0100
    12.3 @@ -6,7 +6,7 @@
    12.4  Executes all examples for Zermelo-Fraenkel Set Theory
    12.5  *)
    12.6  
    12.7 -ZF_build_completed;	(*Cause examples to fail if ZF did*)
    12.8 +ZF_build_completed;	(*Make examples fail if ZF did*)
    12.9  
   12.10  writeln"Root file for ZF Set Theory examples";
   12.11  proof_timing := true;
   12.12 @@ -36,6 +36,8 @@
   12.13  time_use     "ex/enum.ML";
   12.14  
   12.15  (** Inductive definitions **)
   12.16 +(*mapping a relation over a list*)
   12.17 +time_use     "ex/rmap.ML";
   12.18  (*completeness of propositional logic*)
   12.19  time_use     "ex/prop.ML";
   12.20  time_use_thy "ex/prop-log";
   12.21 @@ -46,6 +48,7 @@
   12.22  time_use     "ex/comb.ML";
   12.23  time_use_thy "ex/contract";
   12.24  time_use     "ex/parcontract.ML";
   12.25 +time_use_thy "ex/primrec";
   12.26  
   12.27  (** Co-Datatypes **)
   12.28  time_use     "ex/llist.ML";
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/ZF/ex/Rmap.ML	Thu Sep 30 10:54:01 1993 +0100
    13.3 @@ -0,0 +1,82 @@
    13.4 +(*  Title: 	ZF/ex/rmap
    13.5 +    ID:         $Id$
    13.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   1993  University of Cambridge
    13.8 +
    13.9 +Inductive definition of an operator to "map" a relation over a list
   13.10 +*)
   13.11 +
   13.12 +structure Rmap = Inductive_Fun
   13.13 + (val thy = List.thy addconsts [(["rmap"],"i=>i")];
   13.14 +  val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
   13.15 +  val sintrs = 
   13.16 +      ["<Nil,Nil> : rmap(r)",
   13.17 +
   13.18 +       "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
   13.19 +\       <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
   13.20 +  val monos = [];
   13.21 +  val con_defs = [];
   13.22 +  val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI]
   13.23 +  val type_elims = [SigmaE2]);
   13.24 +
   13.25 +goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
   13.26 +by (rtac lfp_mono 1);
   13.27 +by (REPEAT (rtac Rmap.bnd_mono 1));
   13.28 +by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
   13.29 +		      basic_monos) 1));
   13.30 +val rmap_mono = result();
   13.31 +
   13.32 +val rmap_induct = standard 
   13.33 +    (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
   13.34 +
   13.35 +val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)"
   13.36 +and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)";
   13.37 +
   13.38 +val rmap_cs = ZF_cs addIs  Rmap.intrs
   13.39 +		    addSEs [Nil_rmap_case, Cons_rmap_case];
   13.40 +
   13.41 +goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
   13.42 +by (rtac (Rmap.dom_subset RS subset_trans) 1);
   13.43 +by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
   13.44 +		      Sigma_mono, list_mono] 1));
   13.45 +val rmap_rel_type = result();
   13.46 +
   13.47 +goal Rmap.thy
   13.48 +    "!!r. [| ALL x:A. EX y. <x,y>: r;  xs: list(A) |] ==> \
   13.49 +\         EX y. <xs, y> : rmap(r)";
   13.50 +by (etac List.induct 1);
   13.51 +by (ALLGOALS (fast_tac rmap_cs));
   13.52 +val rmap_total = result();
   13.53 +
   13.54 +goal Rmap.thy
   13.55 +    "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z;    \
   13.56 +\            <xs, ys> : rmap(r) |] ==>                    \
   13.57 +\          ALL zs. <xs, zs> : rmap(r) --> ys=zs";
   13.58 +by (etac rmap_induct 1);
   13.59 +by (ALLGOALS (fast_tac rmap_cs));
   13.60 +val rmap_functional_lemma = result();
   13.61 +val rmap_functional = standard (rmap_functional_lemma RS spec RS mp);
   13.62 +
   13.63 +(** If f is a function then rmap(f) behaves as expected. **)
   13.64 +
   13.65 +goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
   13.66 +by (etac PiE 1);
   13.67 +by (rtac PiI 1);
   13.68 +by (etac rmap_rel_type 1);
   13.69 +by (rtac (rmap_total RS ex_ex1I) 1);
   13.70 +by (assume_tac 2);
   13.71 +by (fast_tac (ZF_cs addSEs [bspec RS ex1E]) 1);
   13.72 +by (rtac rmap_functional 1);
   13.73 +by (REPEAT (assume_tac 2));
   13.74 +by (fast_tac (ZF_cs addSEs [bspec RS ex1_equalsE]) 1);
   13.75 +val rmap_fun_type = result();
   13.76 +
   13.77 +goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
   13.78 +by (fast_tac (rmap_cs addIs [the_equality]) 1);
   13.79 +val rmap_Nil = result();
   13.80 +
   13.81 +goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
   13.82 +\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
   13.83 +by (rtac apply_equality 1);
   13.84 +by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1));
   13.85 +val rmap_Cons = result();
    14.1 --- a/src/ZF/ex/Term.ML	Thu Sep 30 10:26:38 1993 +0100
    14.2 +++ b/src/ZF/ex/Term.ML	Thu Sep 30 10:54:01 1993 +0100
    14.3 @@ -16,7 +16,7 @@
    14.4    val ext = None
    14.5    val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
    14.6    val monos = [list_mono];
    14.7 -  val type_intrs = [SigmaI,Pair_in_univ, list_univ RS subsetD, A_into_univ];
    14.8 +  val type_intrs = [list_univ RS subsetD] @ data_typechecks;
    14.9    val type_elims = []);
   14.10  
   14.11  val [ApplyI] = Term.intrs;
    15.1 --- a/src/ZF/ex/bin.ML	Thu Sep 30 10:26:38 1993 +0100
    15.2 +++ b/src/ZF/ex/bin.ML	Thu Sep 30 10:54:01 1993 +0100
    15.3 @@ -14,18 +14,7 @@
    15.4  	  [(["Plus", "Minus"],	"i"),
    15.5  	   (["op $$"],		"[i,i]=>i")])];
    15.6    val rec_styp = "i";
    15.7 -  val ext = Some (NewSext {
    15.8 -	     mixfix =
    15.9 -	      [Infixl("$$", "[i,i] => i", 60)],
   15.10 -	     xrules = [],
   15.11 -	     parse_ast_translation = [],
   15.12 -	     parse_preproc = None,
   15.13 -	     parse_postproc = None,
   15.14 -	     parse_translation = [],
   15.15 -	     print_translation = [],
   15.16 -	     print_preproc = None,
   15.17 -	     print_postproc = None,
   15.18 -	     print_ast_translation = []});
   15.19 +  val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
   15.20    val sintrs = 
   15.21  	  ["Plus : bin",
   15.22  	   "Minus : bin",
    16.1 --- a/src/ZF/ex/comb.ML	Thu Sep 30 10:26:38 1993 +0100
    16.2 +++ b/src/ZF/ex/comb.ML	Thu Sep 30 10:54:01 1993 +0100
    16.3 @@ -19,18 +19,7 @@
    16.4  	  [(["K","S"],	"i"),
    16.5  	   (["op #"],	"[i,i]=>i")])];
    16.6    val rec_styp = "i";
    16.7 -  val ext = Some (NewSext {
    16.8 -	     mixfix =
    16.9 -	      [Infixl("#", "[i,i] => i", 90)],
   16.10 -	     xrules = [],
   16.11 -	     parse_ast_translation = [],
   16.12 -	     parse_preproc = None,
   16.13 -	     parse_postproc = None,
   16.14 -	     parse_translation = [],
   16.15 -	     print_translation = [],
   16.16 -	     print_preproc = None,
   16.17 -	     print_postproc = None,
   16.18 -	     print_ast_translation = []});
   16.19 +  val ext = Some (Syntax.simple_sext [Infixl("#", "[i,i] => i", 90)]);
   16.20    val sintrs = 
   16.21  	  ["K : comb",
   16.22  	   "S : comb",
    17.1 --- a/src/ZF/ex/contract0.ML	Thu Sep 30 10:26:38 1993 +0100
    17.2 +++ b/src/ZF/ex/contract0.ML	Thu Sep 30 10:54:01 1993 +0100
    17.3 @@ -1,7 +1,7 @@
    17.4  (*  Title: 	ZF/ex/contract.ML
    17.5      ID:         $Id$
    17.6 -    Author: 	Tobias Nipkow & Lawrence C Paulson
    17.7 -    Copyright   1992  University of Cambridge
    17.8 +    Author: 	Lawrence C Paulson
    17.9 +    Copyright   1993  University of Cambridge
   17.10  
   17.11  For ex/contract.thy.
   17.12  *)
    18.1 --- a/src/ZF/ex/contract0.thy	Thu Sep 30 10:26:38 1993 +0100
    18.2 +++ b/src/ZF/ex/contract0.thy	Thu Sep 30 10:54:01 1993 +0100
    18.3 @@ -1,6 +1,6 @@
    18.4  (*  Title: 	ZF/ex/contract.thy
    18.5      ID:         $Id$
    18.6 -    Author: 	Tobias Nipkow & Lawrence C Paulson
    18.7 +    Author: 	Lawrence C Paulson
    18.8      Copyright   1993  University of Cambridge
    18.9  
   18.10  Inductive definition of (1-step) contractions and (mult-step) reductions
    19.1 --- a/src/ZF/ex/integ.ML	Thu Sep 30 10:26:38 1993 +0100
    19.2 +++ b/src/ZF/ex/integ.ML	Thu Sep 30 10:54:01 1993 +0100
    19.3 @@ -185,7 +185,7 @@
    19.4      "n: nat ==> znegative($~ $# succ(n))";
    19.5  by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
    19.6  by (REPEAT 
    19.7 -    (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
    19.8 +    (resolve_tac [refl, exI, conjI, nat_0_in_succ,
    19.9  		  refl RS intrelI RS imageI, consI1, nnat, nat_0I,
   19.10  		  nat_succI] 1));
   19.11  val znegative_zminus_znat = result();
   19.12 @@ -377,7 +377,7 @@
   19.13  by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
   19.14  val zmult_0 = result();
   19.15  
   19.16 -goalw Integ.thy [integ_def,znat_def,one_def]
   19.17 +goalw Integ.thy [integ_def,znat_def]
   19.18      "!!z. z : integ ==> $#1 $* z = z";
   19.19  by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   19.20  by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
    20.1 --- a/src/ZF/ex/listn.ML	Thu Sep 30 10:26:38 1993 +0100
    20.2 +++ b/src/ZF/ex/listn.ML	Thu Sep 30 10:54:01 1993 +0100
    20.3 @@ -41,3 +41,9 @@
    20.4  by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
    20.5  val listn_image_eq = result();
    20.6  
    20.7 +goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
    20.8 +by (rtac lfp_mono 1);
    20.9 +by (REPEAT (rtac ListN.bnd_mono 1));
   20.10 +by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
   20.11 +val listn_mono = result();
   20.12 +
    21.1 --- a/src/ZF/ex/llist.ML	Thu Sep 30 10:26:38 1993 +0100
    21.2 +++ b/src/ZF/ex/llist.ML	Thu Sep 30 10:54:01 1993 +0100
    21.3 @@ -55,10 +55,10 @@
    21.4  goal LList.thy
    21.5     "!!i. i : nat ==> 	\
    21.6  \        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
    21.7 -be complete_induct 1;
    21.8 -br ballI 1;
    21.9 -be LList.elim 1;
   21.10 -bws ([QInl_def,QInr_def]@LList.con_defs);
   21.11 +by (etac complete_induct 1);
   21.12 +by (rtac ballI 1);
   21.13 +by (etac LList.elim 1);
   21.14 +by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
   21.15  by (fast_tac quniv_cs 1);
   21.16  by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
   21.17  by (fast_tac quniv_cs 1);
   21.18 @@ -66,9 +66,9 @@
   21.19  val llist_quniv_lemma = result();
   21.20  
   21.21  goal LList.thy "llist(quniv(A)) <= quniv(A)";
   21.22 -br subsetI 1;
   21.23 -br quniv_Int_Vfrom 1;
   21.24 -be (LList.dom_subset RS subsetD) 1;
   21.25 +by (rtac subsetI 1);
   21.26 +by (rtac quniv_Int_Vfrom 1);
   21.27 +by (etac (LList.dom_subset RS subsetD) 1);
   21.28  by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
   21.29  val llist_quniv = result();
   21.30  
   21.31 @@ -102,20 +102,20 @@
   21.32  (*Keep unfolding the lazy list until the induction hypothesis applies*)
   21.33  goal LList_Eq.thy
   21.34     "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
   21.35 -be trans_induct 1;
   21.36 +by (etac trans_induct 1);
   21.37  by (safe_tac subset_cs);
   21.38 -be LList_Eq.elim 1;
   21.39 +by (etac LList_Eq.elim 1);
   21.40  by (safe_tac (subset_cs addSEs [QPair_inject]));
   21.41 -bws LList.con_defs;
   21.42 +by (rewrite_goals_tac LList.con_defs);
   21.43  by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   21.44  (*0 case*)
   21.45  by (fast_tac lleq_cs 1);
   21.46  (*succ(j) case*)
   21.47 -bw QInr_def;
   21.48 +by (rewtac QInr_def);
   21.49  by (fast_tac lleq_cs 1);
   21.50  (*Limit(i) case*)
   21.51 -be (Limit_Vfrom_eq RS ssubst) 1;
   21.52 -br (Int_UN_distrib RS ssubst) 1;
   21.53 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
   21.54 +by (rtac (Int_UN_distrib RS ssubst) 1);
   21.55  by (fast_tac lleq_cs 1);
   21.56  val lleq_Int_Vset_subset_lemma = result();
   21.57  
   21.58 @@ -125,15 +125,15 @@
   21.59  
   21.60  (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
   21.61  val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
   21.62 -br (prem RS qconverseI RS LList_Eq.co_induct) 1;
   21.63 -br (LList_Eq.dom_subset RS qconverse_type) 1;
   21.64 +by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
   21.65 +by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
   21.66  by (safe_tac qconverse_cs);
   21.67 -be LList_Eq.elim 1;
   21.68 +by (etac LList_Eq.elim 1);
   21.69  by (ALLGOALS (fast_tac qconverse_cs));
   21.70  val lleq_symmetric = result();
   21.71  
   21.72  goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
   21.73 -br equalityI 1;
   21.74 +by (rtac equalityI 1);
   21.75  by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
   21.76       ORELSE etac lleq_symmetric 1));
   21.77  val lleq_implies_equal = result();
   21.78 @@ -141,9 +141,9 @@
   21.79  val [eqprem,lprem] = goal LList_Eq.thy
   21.80      "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
   21.81  by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
   21.82 -br (lprem RS RepFunI RS (eqprem RS subst)) 1;
   21.83 +by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
   21.84  by (safe_tac qpair_cs);
   21.85 -be LList.elim 1;
   21.86 +by (etac LList.elim 1);
   21.87  by (ALLGOALS (fast_tac qpair_cs));
   21.88  val equal_llist_implies_leq = result();
   21.89  
    22.1 --- a/src/ZF/ex/misc.ML	Thu Sep 30 10:26:38 1993 +0100
    22.2 +++ b/src/ZF/ex/misc.ML	Thu Sep 30 10:54:01 1993 +0100
    22.3 @@ -62,7 +62,7 @@
    22.4  \    X - lfp(X, %W. X - g``(Y - f``W)) ";
    22.5  by (res_inst_tac [("P", "%u. ?v = X-u")] 
    22.6       (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
    22.7 -by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, Diff_subset,
    22.8 +by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,
    22.9  			     gfun RS fun_is_rel RS image_subset]) 1);
   22.10  val Banach_last_equation = result();
   22.11  
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/ZF/ex/primrec0.ML	Thu Sep 30 10:54:01 1993 +0100
    23.3 @@ -0,0 +1,414 @@
    23.4 +(*  Title: 	ZF/ex/primrec
    23.5 +    ID:         $Id$
    23.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7 +    Copyright   1993  University of Cambridge
    23.8 +
    23.9 +Primitive Recursive Functions
   23.10 +
   23.11 +Proof adopted from
   23.12 +Nora Szasz, 
   23.13 +A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
   23.14 +In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
   23.15 +*)
   23.16 +
   23.17 +open Primrec0;
   23.18 +
   23.19 +val pr0_typechecks = 
   23.20 +    nat_typechecks @ List.intrs @ 
   23.21 +    [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
   23.22 +
   23.23 +(** Useful special cases of evaluation ***)
   23.24 +
   23.25 +val pr0_ss = arith_ss 
   23.26 +    addsimps List.case_eqns
   23.27 +    addsimps [list_rec_Nil, list_rec_Cons, 
   23.28 +	      drop_0, drop_Nil, drop_succ_Cons,
   23.29 +	      map_Nil, map_Cons]
   23.30 +    setsolver (type_auto_tac pr0_typechecks);
   23.31 +
   23.32 +goalw Primrec0.thy [SC_def]
   23.33 +    "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
   23.34 +by (asm_simp_tac pr0_ss 1);
   23.35 +val SC = result();
   23.36 +
   23.37 +goalw Primrec0.thy [CONST_def]
   23.38 +    "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
   23.39 +by (asm_simp_tac pr0_ss 1);
   23.40 +val CONST = result();
   23.41 +
   23.42 +goalw Primrec0.thy [PROJ_def]
   23.43 +    "!!l. [| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
   23.44 +by (asm_simp_tac pr0_ss 1);
   23.45 +val PROJ_0 = result();
   23.46 +
   23.47 +goalw Primrec0.thy [COMP_def]
   23.48 +    "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
   23.49 +by (asm_simp_tac pr0_ss 1);
   23.50 +val COMP_1 = result();
   23.51 +
   23.52 +goalw Primrec0.thy [PREC_def]
   23.53 +    "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
   23.54 +by (asm_simp_tac pr0_ss 1);
   23.55 +val PREC_0 = result();
   23.56 +
   23.57 +goalw Primrec0.thy [PREC_def]
   23.58 +    "!!l. [| x:nat;  l: list(nat) |] ==>  \
   23.59 +\         PREC(f,g) ` (Cons(succ(x),l)) = \
   23.60 +\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
   23.61 +by (asm_simp_tac pr0_ss 1);
   23.62 +val PREC_succ = result();
   23.63 +
   23.64 +(*** Inductive definition of the PR functions ***)
   23.65 +
   23.66 +structure Primrec = Inductive_Fun
   23.67 + (val thy = Primrec0.thy;
   23.68 +  val rec_doms = [("primrec", "list(nat)->nat")];
   23.69 +  val ext = None
   23.70 +  val sintrs = 
   23.71 +      ["SC : primrec",
   23.72 +       "k: nat ==> CONST(k) : primrec",
   23.73 +       "i: nat ==> PROJ(i) : primrec",
   23.74 +       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
   23.75 +       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
   23.76 +  val monos = [list_mono];
   23.77 +  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
   23.78 +  val type_intrs = pr0_typechecks
   23.79 +  val type_elims = []);
   23.80 +
   23.81 +(* c: primrec ==> c: list(nat) -> nat *)
   23.82 +val primrec_into_fun = Primrec.dom_subset RS subsetD;
   23.83 +
   23.84 +val pr_ss = pr0_ss 
   23.85 +    setsolver (type_auto_tac ([primrec_into_fun] @ 
   23.86 +			      pr0_typechecks @ Primrec.intrs));
   23.87 +
   23.88 +goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
   23.89 +by (etac nat_induct 1);
   23.90 +by (ALLGOALS (asm_simp_tac pr_ss));
   23.91 +val ACK_in_primrec = result();
   23.92 +
   23.93 +val ack_typechecks =
   23.94 +    [ACK_in_primrec, primrec_into_fun RS apply_type,
   23.95 +     add_type, list_add_type, naturals_are_ordinals] @ 
   23.96 +    nat_typechecks @ List.intrs @ Primrec.intrs;
   23.97 +
   23.98 +(*strict typechecking for the Ackermann proof; instantiates no vars*)
   23.99 +fun tc_tac rls =
  23.100 +    REPEAT
  23.101 +      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
  23.102 +
  23.103 +goal Primrec.thy "!!i j. [| i:nat;  j:nat |] ==>  ack(i,j): nat";
  23.104 +by (tc_tac []);
  23.105 +val ack_type = result();
  23.106 +
  23.107 +(** Ackermann's function cases **)
  23.108 +
  23.109 +(*PROPERTY A 1*)
  23.110 +goalw Primrec0.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
  23.111 +by (asm_simp_tac (pr0_ss addsimps [SC]) 1);
  23.112 +val ack_0 = result();
  23.113 +
  23.114 +(*PROPERTY A 2*)
  23.115 +goalw Primrec0.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
  23.116 +by (asm_simp_tac (pr0_ss addsimps [CONST,PREC_0]) 1);
  23.117 +val ack_succ_0 = result();
  23.118 +
  23.119 +(*PROPERTY A 3*)
  23.120 +(*Could be proved in Primrec0, like the previous two cases, but using
  23.121 +  primrec_into_fun makes type-checking easier!*)
  23.122 +goalw Primrec.thy [ACK_def]
  23.123 +    "!!i j. [| i:nat;  j:nat |] ==> \
  23.124 +\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
  23.125 +by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
  23.126 +val ack_succ_succ = result();
  23.127 +
  23.128 +val ack_ss = 
  23.129 +    pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, 
  23.130 +		    ack_type, naturals_are_ordinals];
  23.131 +
  23.132 +(*PROPERTY A 4*)
  23.133 +goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j : ack(i,j)";
  23.134 +by (etac nat_induct 1);
  23.135 +by (asm_simp_tac ack_ss 1);
  23.136 +by (rtac ballI 1);
  23.137 +by (eres_inst_tac [("n","j")] nat_induct 1);
  23.138 +by (ALLGOALS (asm_simp_tac ack_ss));
  23.139 +by (rtac ([succI1, asm_rl,naturals_are_ordinals] MRS Ord_trans) 1);
  23.140 +by (rtac (succ_mem_succI RS Ord_trans1) 3);
  23.141 +by (etac bspec 5);
  23.142 +by (ALLGOALS (asm_simp_tac ack_ss));
  23.143 +val less_ack2_lemma = result();
  23.144 +val less_ack2 = standard (less_ack2_lemma RS bspec);
  23.145 +
  23.146 +(*PROPERTY A 5-, the single-step lemma*)
  23.147 +goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(i, succ(j))";
  23.148 +by (etac nat_induct 1);
  23.149 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [less_ack2])));
  23.150 +val ack_less_ack_succ2 = result();
  23.151 +
  23.152 +(*PROPERTY A 5, monotonicity for < *)
  23.153 +goal Primrec.thy "!!i j k. [| j:k; i:nat; k:nat |] ==> ack(i,j) : ack(i,k)";
  23.154 +by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
  23.155 +by (assume_tac 1);
  23.156 +by (etac succ_less_induct 1);
  23.157 +by (assume_tac 1);
  23.158 +by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
  23.159 +by (REPEAT (ares_tac ([ack_less_ack_succ2, ack_type] @ pr0_typechecks) 1));
  23.160 +val ack_less_mono2 = result();
  23.161 +
  23.162 +(*PROPERTY A 5', monotonicity for <= *)
  23.163 +goal Primrec.thy
  23.164 +    "!!i j k. [| j<=k; i:nat; j:nat; k:nat |] ==> ack(i,j) <= ack(i,k)";
  23.165 +by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_less_mono_imp_mono 1);
  23.166 +by (REPEAT (ares_tac [ack_less_mono2, ack_type, Ord_nat] 1));
  23.167 +val ack_mono2 = result();
  23.168 +
  23.169 +(*PROPERTY A 6*)
  23.170 +goal Primrec.thy
  23.171 +    "!!i j. [| i:nat;  j:nat |] ==> ack(i, succ(j)) <= ack(succ(i), j)";
  23.172 +by (nat_ind_tac "j" [] 1);
  23.173 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [subset_refl])));
  23.174 +by (rtac ack_mono2 1);
  23.175 +by (rtac (less_ack2 RS Ord_succ_subsetI RS subset_trans) 1);
  23.176 +by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type] @ pr0_typechecks) 1));
  23.177 +val ack2_leq_ack1 = result();
  23.178 +
  23.179 +(*PROPERTY A 7-, the single-step lemma*)
  23.180 +goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(succ(i),j)";
  23.181 +by (rtac (ack_less_mono2 RS Ord_trans2) 1);
  23.182 +by (rtac (ack2_leq_ack1 RS member_succI) 4);
  23.183 +by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type, succI1] @ 
  23.184 +		      pr0_typechecks) 1));
  23.185 +val ack_less_ack_succ1 = result();
  23.186 +
  23.187 +(*PROPERTY A 7, monotonicity for < *)
  23.188 +goal Primrec.thy "!!i j k. [| i:j; j:nat; k:nat |] ==> ack(i,k) : ack(j,k)";
  23.189 +by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
  23.190 +by (assume_tac 1);
  23.191 +by (etac succ_less_induct 1);
  23.192 +by (assume_tac 1);
  23.193 +by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
  23.194 +by (REPEAT (ares_tac ([ack_less_ack_succ1, ack_type] @ pr0_typechecks) 1));
  23.195 +val ack_less_mono1 = result();
  23.196 +
  23.197 +(*PROPERTY A 7', monotonicity for <= *)
  23.198 +goal Primrec.thy
  23.199 +    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> ack(i,k) <= ack(j,k)";
  23.200 +by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_less_mono_imp_mono 1);
  23.201 +by (REPEAT (ares_tac [ack_less_mono1, ack_type, Ord_nat] 1));
  23.202 +val ack_mono1 = result();
  23.203 +
  23.204 +(*PROPERTY A 8*)
  23.205 +goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
  23.206 +by (etac nat_induct 1);
  23.207 +by (ALLGOALS (asm_simp_tac ack_ss));
  23.208 +val ack_1 = result();
  23.209 +
  23.210 +(*PROPERTY A 9*)
  23.211 +goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
  23.212 +by (etac nat_induct 1);
  23.213 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
  23.214 +val ack_2 = result();
  23.215 +
  23.216 +(*PROPERTY A 10*)
  23.217 +goal Primrec.thy
  23.218 +    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
  23.219 +\               ack(i1, ack(i2,j)) : ack(succ(succ(i1#+i2)), j)";
  23.220 +by (rtac Ord_trans2 1);
  23.221 +by (rtac (ack2_leq_ack1 RS member_succI) 2);
  23.222 +by (asm_simp_tac ack_ss 1);
  23.223 +by (rtac ([ack_mono1 RS member_succI, ack_less_mono2] MRS Ord_trans1) 1);
  23.224 +by (rtac add_leq_self 1);
  23.225 +by (tc_tac []);
  23.226 +by (rtac (add_commute RS ssubst) 1);
  23.227 +by (rtac (add_less_succ_self RS ack_less_mono1) 3);
  23.228 +by (tc_tac []);
  23.229 +val ack_nest_bound = result();
  23.230 +
  23.231 +(*PROPERTY A 11*)
  23.232 +goal Primrec.thy
  23.233 +    "!!i1 i2. [| i1:nat; i2:nat |] ==> \
  23.234 +\             EX k:nat. ALL j:nat. ack(i1,j) #+ ack(i2,j) : ack(k,j)";
  23.235 +by (rtac (Ord_trans RS ballI RS bexI) 1);
  23.236 +by (res_inst_tac [("i1.0", "succ(1)"), ("i2.0", "i1#+i2")] ack_nest_bound 2);
  23.237 +by (rtac (ack_2 RS ssubst) 1);
  23.238 +by (tc_tac []);
  23.239 +by (rtac (member_succI RS succI2 RS succI2) 1);
  23.240 +by (rtac (add_leq_self RS ack_mono1 RS add_mono) 1);
  23.241 +by (tc_tac []);
  23.242 +by (rtac (add_commute RS ssubst) 1);
  23.243 +by (rtac (add_leq_self RS ack_mono1) 3);
  23.244 +by (tc_tac []);
  23.245 +val ack_add_bound = result();
  23.246 +
  23.247 +(*PROPERTY A 12 -- note quantifier nesting
  23.248 +  Article uses existential quantifier but the ALF proof used a concrete
  23.249 +  expression, namely k#+4. *)
  23.250 +goal Primrec.thy
  23.251 +    "!!k. k: nat ==> \
  23.252 +\         EX k':nat. ALL i:nat. ALL j:nat. i : ack(k,j) --> i#+j : ack(k',j)";
  23.253 +by (res_inst_tac [("i1.1", "k"), ("i2.1", "0")] (ack_add_bound RS bexE) 1);
  23.254 +by (rtac (Ord_trans RS impI RS ballI RS ballI RS bexI) 3);
  23.255 +by (etac bspec 4);
  23.256 +by (ALLGOALS (asm_simp_tac (ack_ss addsimps [add_less_mono])));
  23.257 +val ack_add_bound2 = result();
  23.258 +
  23.259 +(*** MAIN RESULT ***)
  23.260 +
  23.261 +val ack2_ss =
  23.262 +    ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, 
  23.263 +		     naturals_are_ordinals];
  23.264 +
  23.265 +goalw Primrec.thy [SC_def]
  23.266 +    "!!l. l: list(nat) ==> SC ` l : ack(1, list_add(l))";
  23.267 +by (etac List.elim 1);
  23.268 +by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
  23.269 +by (asm_simp_tac (ack2_ss addsimps 
  23.270 +		  [ack_1, add_less_succ_self RS succ_mem_succI]) 1);
  23.271 +val SC_case = result();
  23.272 +
  23.273 +(*PROPERTY A 4'?? Extra lemma needed for CONST case, constant functions*)
  23.274 +goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i : ack(i,j)";
  23.275 +by (etac nat_induct 1);
  23.276 +by (asm_simp_tac (ack_ss addsimps [nat_0_in_succ]) 1);
  23.277 +by (etac ([succ_mem_succI, ack_less_ack_succ1] MRS Ord_trans1) 1);
  23.278 +by (tc_tac []);
  23.279 +val less_ack1 = result();
  23.280 +
  23.281 +goalw Primrec.thy [CONST_def]
  23.282 +    "!!l. [| l: list(nat);  k: nat |] ==> CONST(k) ` l : ack(k, list_add(l))";
  23.283 +by (asm_simp_tac (ack2_ss addsimps [less_ack1]) 1);
  23.284 +val CONST_case = result();
  23.285 +
  23.286 +goalw Primrec.thy [PROJ_def]
  23.287 +    "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l : ack(0, list_add(l))";
  23.288 +by (asm_simp_tac ack2_ss 1);
  23.289 +by (etac List.induct 1);
  23.290 +by (asm_simp_tac (ack2_ss addsimps [nat_0_in_succ]) 1);
  23.291 +by (asm_simp_tac ack2_ss 1);
  23.292 +by (rtac ballI 1);
  23.293 +by (eres_inst_tac [("n","x")] natE 1);
  23.294 +by (asm_simp_tac (ack2_ss addsimps [add_less_succ_self]) 1);
  23.295 +by (asm_simp_tac ack2_ss 1);
  23.296 +by (etac (bspec RS Ord_trans2) 1);
  23.297 +by (assume_tac 1);
  23.298 +by (rtac (add_commute RS ssubst) 1);
  23.299 +by (rtac (add_less_succ_self RS succ_mem_succI) 3);
  23.300 +by (tc_tac [list_add_type]);
  23.301 +val PROJ_case_lemma = result();
  23.302 +val PROJ_case = PROJ_case_lemma RS bspec;
  23.303 +
  23.304 +(** COMP case **)
  23.305 +
  23.306 +goal Primrec.thy
  23.307 + "!!fs. fs : list({f: primrec .					\
  23.308 +\              	   EX kf:nat. ALL l:list(nat). 			\
  23.309 +\		    	      f`l : ack(kf, list_add(l))})	\
  23.310 +\      ==> EX k:nat. ALL l: list(nat). 				\
  23.311 +\                list_add(map(%f. f ` l, fs)) : ack(k, list_add(l))";
  23.312 +by (etac List.induct 1);
  23.313 +by (DO_GOAL [res_inst_tac [("x","0")] bexI,
  23.314 +	     asm_simp_tac (ack2_ss addsimps [less_ack1,nat_0_in_succ]),
  23.315 +	     resolve_tac nat_typechecks] 1);
  23.316 +by (safe_tac ZF_cs);
  23.317 +by (asm_simp_tac ack2_ss 1);
  23.318 +by (res_inst_tac [("i1.1", "kf"), ("i2.1", "k")] (ack_add_bound RS bexE) 1
  23.319 +    THEN REPEAT (assume_tac 1));
  23.320 +by (rtac (ballI RS bexI) 1);
  23.321 +by (etac (bspec RS add_less_mono RS Ord_trans) 1);
  23.322 +by (REPEAT (FIRSTGOAL (etac bspec)));
  23.323 +by (tc_tac [list_add_type]);
  23.324 +val COMP_map_lemma = result();
  23.325 +
  23.326 +goalw Primrec.thy [COMP_def]
  23.327 + "!!g. [| g: primrec;  kg: nat;					\
  23.328 +\         ALL l:list(nat). g`l : ack(kg, list_add(l));		\
  23.329 +\         fs : list({f: primrec .				\
  23.330 +\                    EX kf:nat. ALL l:list(nat). 		\
  23.331 +\		    	f`l : ack(kf, list_add(l))}) 		\
  23.332 +\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l : ack(k, list_add(l))";
  23.333 +by (asm_simp_tac ZF_ss 1);
  23.334 +by (forward_tac [list_CollectD] 1);
  23.335 +by (etac (COMP_map_lemma RS bexE) 1);
  23.336 +by (rtac (ballI RS bexI) 1);
  23.337 +by (etac (bspec RS Ord_trans) 1);
  23.338 +by (rtac Ord_trans 2);
  23.339 +by (rtac ack_nest_bound 3);
  23.340 +by (etac (bspec RS ack_less_mono2) 2);
  23.341 +by (tc_tac [map_type]);
  23.342 +val COMP_case = result();
  23.343 +
  23.344 +(** PREC case **)
  23.345 +
  23.346 +goalw Primrec.thy [PREC_def]
  23.347 + "!!f g. [| f: primrec;  kf: nat;					\
  23.348 +\           g: primrec;  kg: nat;					\
  23.349 +\           ALL l:list(nat). f`l #+ list_add(l) : ack(kf, list_add(l));	\
  23.350 +\           ALL l:list(nat). g`l #+ list_add(l) : ack(kg, list_add(l));	\
  23.351 +\           l: list(nat)						\
  23.352 +\        |] ==> PREC(f,g)`l #+ list_add(l) : ack(succ(kf#+kg), list_add(l))";
  23.353 +by (etac List.elim 1);
  23.354 +by (asm_simp_tac (ack2_ss addsimps [[succI1, less_ack2] MRS Ord_trans]) 1);
  23.355 +by (asm_simp_tac ack2_ss 1);
  23.356 +be ssubst 1;  (*get rid of the needless assumption*)
  23.357 +by (eres_inst_tac [("n","a")] nat_induct 1);
  23.358 +by (asm_simp_tac ack2_ss 1);
  23.359 +by (rtac Ord_trans 1);
  23.360 +by (etac bspec 1);
  23.361 +by (assume_tac 1);
  23.362 +by (rtac ack_less_mono1 1);
  23.363 +by (rtac add_less_succ_self 1);
  23.364 +by (tc_tac [list_add_type]);
  23.365 +(*ind step -- level 13*)
  23.366 +by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
  23.367 +by (rtac (succ_mem_succI RS Ord_trans1) 1);
  23.368 +by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] Ord_trans1 1);
  23.369 +by (etac bspec 2);
  23.370 +by (rtac (subset_refl RS add_mono RS member_succI) 1);
  23.371 +by (tc_tac []);
  23.372 +by (asm_simp_tac (ack2_ss addsimps [add_leq_self2]) 1);
  23.373 +by (asm_simp_tac ack2_ss 1);
  23.374 +(*final part of the simplification*)
  23.375 +by (rtac (member_succI RS Ord_trans1) 1);
  23.376 +by (rtac (add_leq_self2 RS ack_mono1) 1);
  23.377 +by (etac ack_less_mono2 8);
  23.378 +by (tc_tac []);
  23.379 +val PREC_case_lemma = result();
  23.380 +
  23.381 +goal Primrec.thy
  23.382 + "!!f g. [| f: primrec;  kf: nat;				\
  23.383 +\           g: primrec;  kg: nat;				\
  23.384 +\           ALL l:list(nat). f`l : ack(kf, list_add(l));	\
  23.385 +\           ALL l:list(nat). g`l : ack(kg, list_add(l)) 	\
  23.386 +\        |] ==> EX k:nat. ALL l: list(nat). 			\
  23.387 +\		    PREC(f,g)`l: ack(k, list_add(l))";
  23.388 +by (etac (ack_add_bound2 RS bexE) 1);
  23.389 +by (etac (ack_add_bound2 RS bexE) 1);
  23.390 +by (rtac (ballI RS bexI) 1);
  23.391 +by (rtac ([add_leq_self RS member_succI, PREC_case_lemma] MRS Ord_trans1) 1);
  23.392 +by (DEPTH_SOLVE
  23.393 +    (SOMEGOAL
  23.394 +     (FIRST' [test_assume_tac,
  23.395 +	      match_tac (ballI::ack_typechecks),
  23.396 +	      eresolve_tac [bspec, bspec RS bspec RS mp]])));
  23.397 +val PREC_case = result();
  23.398 +
  23.399 +goal Primrec.thy
  23.400 +    "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l : ack(k, list_add(l))";
  23.401 +by (etac Primrec.induct 1);
  23.402 +by (safe_tac ZF_cs);
  23.403 +by (DEPTH_SOLVE
  23.404 +    (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
  23.405 +		       bexI, ballI] @ nat_typechecks) 1));
  23.406 +val ack_bounds_primrec = result();
  23.407 +
  23.408 +goal Primrec.thy
  23.409 +    "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
  23.410 +by (rtac notI 1);
  23.411 +by (etac (ack_bounds_primrec RS bexE) 1);
  23.412 +by (rtac mem_anti_refl 1);
  23.413 +by (dres_inst_tac [("x", "[x]")] bspec 1);
  23.414 +by (asm_simp_tac ack2_ss 1);
  23.415 +by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
  23.416 +val ack_not_primrec = result();
  23.417 +
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/ZF/ex/primrec0.thy	Thu Sep 30 10:54:01 1993 +0100
    24.3 @@ -0,0 +1,46 @@
    24.4 +(*  Title: 	ZF/ex/primrec.thy
    24.5 +    ID:         $Id$
    24.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7 +    Copyright   1993  University of Cambridge
    24.8 +
    24.9 +Primitive Recursive Functions
   24.10 +
   24.11 +Proof adopted from
   24.12 +Nora Szasz, 
   24.13 +A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
   24.14 +In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
   24.15 +*)
   24.16 +
   24.17 +Primrec0 = ListFn +
   24.18 +consts
   24.19 +    SC      :: "i"
   24.20 +    CONST   :: "i=>i"
   24.21 +    PROJ    :: "i=>i"
   24.22 +    COMP    :: "[i,i]=>i"
   24.23 +    PREC    :: "[i,i]=>i"
   24.24 +    primrec :: "i"
   24.25 +    ACK	    :: "i=>i"
   24.26 +    ack	    :: "[i,i]=>i"
   24.27 +
   24.28 +translations
   24.29 +  "ack(x,y)"  == "ACK(x) ` [y]"
   24.30 +
   24.31 +rules
   24.32 +
   24.33 +  SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
   24.34 +
   24.35 +  CONST_def "CONST(k) == lam l:list(nat).k"
   24.36 +
   24.37 +  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
   24.38 +
   24.39 +  COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
   24.40 +
   24.41 +  (*Note that g is applied first to PREC(f,g)`y and then to y!*)
   24.42 +  PREC_def  "PREC(f,g) == \
   24.43 +\            lam l:list(nat). list_case(0, \
   24.44 +\                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
   24.45 +  
   24.46 +  ACK_def   "ACK(i) == rec(i, SC, \
   24.47 +\                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
   24.48 +
   24.49 +end
    25.1 --- a/src/ZF/ex/prop.ML	Thu Sep 30 10:26:38 1993 +0100
    25.2 +++ b/src/ZF/ex/prop.ML	Thu Sep 30 10:54:01 1993 +0100
    25.3 @@ -16,19 +16,9 @@
    25.4  	   (["Var"],	"i=>i"),
    25.5  	   (["op =>"],	"[i,i]=>i")])];
    25.6    val rec_styp = "i";
    25.7 -  val ext = Some (NewSext {
    25.8 -	     mixfix =
    25.9 -	      [Mixfix("#_", "i => i", "Var", [100], 100),
   25.10 -	       Infixr("=>", "[i,i] => i", 90)],
   25.11 -	     xrules = [],
   25.12 -	     parse_ast_translation = [],
   25.13 -	     parse_preproc = None,
   25.14 -	     parse_postproc = None,
   25.15 -	     parse_translation = [],
   25.16 -	     print_translation = [],
   25.17 -	     print_preproc = None,
   25.18 -	     print_postproc = None,
   25.19 -	     print_ast_translation = []});
   25.20 +  val ext = Some (Syntax.simple_sext
   25.21 +		    [Mixfix("#_", "i => i", "Var", [100], 100),
   25.22 +		     Infixr("=>", "[i,i] => i", 90)]);
   25.23    val sintrs = 
   25.24  	  ["Fls : prop",
   25.25  	   "n: nat ==> #n : prop",
    26.1 --- a/src/ZF/ex/proplog.ML	Thu Sep 30 10:26:38 1993 +0100
    26.2 +++ b/src/ZF/ex/proplog.ML	Thu Sep 30 10:54:01 1993 +0100
    26.3 @@ -190,9 +190,10 @@
    26.4  by (rtac (expand_if RS iffD2) 1);
    26.5  by (rtac (major RS Prop.induct) 1);
    26.6  by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
    26.7 -by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
    26.8 -			   weaken_right, Imp_Fls]
    26.9 -                    addSEs [Fls_Imp]) 1);
   26.10 +by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, 
   26.11 +			    Fls_Imp RS weaken_left_Un2]));
   26.12 +by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
   26.13 +				     weaken_right, Imp_Fls])));
   26.14  val hyps_thms_if = result();
   26.15  
   26.16  (*Key lemma for completeness; yields a set of assumptions satisfying p*)
   26.17 @@ -264,7 +265,7 @@
   26.18  val [major] = goal PropThms.thy
   26.19      "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
   26.20  by (rtac (major RS Prop.induct) 1);
   26.21 -by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I] 
   26.22 +by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I, cons_iff]
   26.23  		  setloop (split_tac [expand_if])) 2);
   26.24  by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
   26.25  val hyps_finite = result();
   26.26 @@ -324,5 +325,3 @@
   26.27  val thms_iff = result();
   26.28  
   26.29  writeln"Reached end of file.";
   26.30 -
   26.31 -
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/ZF/ex/rmap.ML	Thu Sep 30 10:54:01 1993 +0100
    27.3 @@ -0,0 +1,82 @@
    27.4 +(*  Title: 	ZF/ex/rmap
    27.5 +    ID:         $Id$
    27.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    27.7 +    Copyright   1993  University of Cambridge
    27.8 +
    27.9 +Inductive definition of an operator to "map" a relation over a list
   27.10 +*)
   27.11 +
   27.12 +structure Rmap = Inductive_Fun
   27.13 + (val thy = List.thy addconsts [(["rmap"],"i=>i")];
   27.14 +  val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
   27.15 +  val sintrs = 
   27.16 +      ["<Nil,Nil> : rmap(r)",
   27.17 +
   27.18 +       "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
   27.19 +\       <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
   27.20 +  val monos = [];
   27.21 +  val con_defs = [];
   27.22 +  val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI]
   27.23 +  val type_elims = [SigmaE2]);
   27.24 +
   27.25 +goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
   27.26 +by (rtac lfp_mono 1);
   27.27 +by (REPEAT (rtac Rmap.bnd_mono 1));
   27.28 +by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
   27.29 +		      basic_monos) 1));
   27.30 +val rmap_mono = result();
   27.31 +
   27.32 +val rmap_induct = standard 
   27.33 +    (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
   27.34 +
   27.35 +val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)"
   27.36 +and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)";
   27.37 +
   27.38 +val rmap_cs = ZF_cs addIs  Rmap.intrs
   27.39 +		    addSEs [Nil_rmap_case, Cons_rmap_case];
   27.40 +
   27.41 +goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
   27.42 +by (rtac (Rmap.dom_subset RS subset_trans) 1);
   27.43 +by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
   27.44 +		      Sigma_mono, list_mono] 1));
   27.45 +val rmap_rel_type = result();
   27.46 +
   27.47 +goal Rmap.thy
   27.48 +    "!!r. [| ALL x:A. EX y. <x,y>: r;  xs: list(A) |] ==> \
   27.49 +\         EX y. <xs, y> : rmap(r)";
   27.50 +by (etac List.induct 1);
   27.51 +by (ALLGOALS (fast_tac rmap_cs));
   27.52 +val rmap_total = result();
   27.53 +
   27.54 +goal Rmap.thy
   27.55 +    "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z;    \
   27.56 +\            <xs, ys> : rmap(r) |] ==>                    \
   27.57 +\          ALL zs. <xs, zs> : rmap(r) --> ys=zs";
   27.58 +by (etac rmap_induct 1);
   27.59 +by (ALLGOALS (fast_tac rmap_cs));
   27.60 +val rmap_functional_lemma = result();
   27.61 +val rmap_functional = standard (rmap_functional_lemma RS spec RS mp);
   27.62 +
   27.63 +(** If f is a function then rmap(f) behaves as expected. **)
   27.64 +
   27.65 +goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
   27.66 +by (etac PiE 1);
   27.67 +by (rtac PiI 1);
   27.68 +by (etac rmap_rel_type 1);
   27.69 +by (rtac (rmap_total RS ex_ex1I) 1);
   27.70 +by (assume_tac 2);
   27.71 +by (fast_tac (ZF_cs addSEs [bspec RS ex1E]) 1);
   27.72 +by (rtac rmap_functional 1);
   27.73 +by (REPEAT (assume_tac 2));
   27.74 +by (fast_tac (ZF_cs addSEs [bspec RS ex1_equalsE]) 1);
   27.75 +val rmap_fun_type = result();
   27.76 +
   27.77 +goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
   27.78 +by (fast_tac (rmap_cs addIs [the_equality]) 1);
   27.79 +val rmap_Nil = result();
   27.80 +
   27.81 +goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
   27.82 +\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
   27.83 +by (rtac apply_equality 1);
   27.84 +by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1));
   27.85 +val rmap_Cons = result();
    28.1 --- a/src/ZF/ex/term.ML	Thu Sep 30 10:26:38 1993 +0100
    28.2 +++ b/src/ZF/ex/term.ML	Thu Sep 30 10:54:01 1993 +0100
    28.3 @@ -16,7 +16,7 @@
    28.4    val ext = None
    28.5    val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
    28.6    val monos = [list_mono];
    28.7 -  val type_intrs = [SigmaI,Pair_in_univ, list_univ RS subsetD, A_into_univ];
    28.8 +  val type_intrs = [list_univ RS subsetD] @ data_typechecks;
    28.9    val type_elims = []);
   28.10  
   28.11  val [ApplyI] = Term.intrs;