# HG changeset patch
# User wenzelm
# Date 785777058 -3600
# Node ID fcf8024c920d1083e4cc199656752051a9fa3b36
# Parent  6be2f3e0378617924ae8dbf43cfeb151b086417b
minor changes according to new hologic;

diff -r 6be2f3e03786 -r fcf8024c920d Inductive.ML
--- a/Inductive.ML	Fri Nov 25 14:39:13 1994 +0100
+++ b/Inductive.ML	Fri Nov 25 16:24:18 1994 +0100
@@ -16,7 +16,7 @@
 in
 
 fun gen_fp_oper a (X,T,t) = 
-    let val setT = mk_set T
+    let val setT = mk_setT T
     in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t)  end;
 
 structure Lfp_items =
diff -r 6be2f3e03786 -r fcf8024c920d add_ind_def.ML
--- a/add_ind_def.ML	Fri Nov 25 14:39:13 1994 +0100
+++ b/add_ind_def.ML	Fri Nov 25 16:24:18 1994 +0100
@@ -88,9 +88,9 @@
     val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
 
     (*Probably INCORRECT for mutual recursion!*)
-    val domTs = summands(dest_set (body_type recT));
+    val domTs = summands(dest_setT (body_type recT));
     val dom_sumT = fold_bal mk_sum domTs;
-    val dom_set   = mk_set dom_sumT;
+    val dom_set   = mk_setT dom_sumT;
 
     val freez   = Free(z, dom_sumT)
     and freeX   = Free(X, dom_set);
diff -r 6be2f3e03786 -r fcf8024c920d ind_syntax.ML
--- a/ind_syntax.ML	Fri Nov 25 14:39:13 1994 +0100
+++ b/ind_syntax.ML	Fri Nov 25 16:24:18 1994 +0100
@@ -4,7 +4,7 @@
     Copyright   1994  University of Cambridge
 
 Abstract Syntax functions for Inductive Definitions
-See also ../Pure/section-utils.ML
+See also hologic.ML and ../Pure/section-utils.ML
 *)
 
 (*The structure protects these items from redeclaration (somewhat!).  The 
@@ -15,48 +15,26 @@
 
 (** Abstract syntax definitions for HOL **)
 
-val termC: class = "term";
-val termS: sort = [termC];
-
-val termTVar = TVar(("'a",0),termS);
-
-val boolT = Type("bool",[]);
-val unitT = Type("unit",[]);
-
-val conj = Const("op &", [boolT,boolT]--->boolT)
-and disj = Const("op |", [boolT,boolT]--->boolT)
-and imp = Const("op -->", [boolT,boolT]--->boolT);
-
-fun eq_const T = Const("op =", [T,T]--->boolT);
-
-fun mk_set T = Type("set",[T]);
-
-fun dest_set (Type("set",[T])) = T
-  | dest_set _                 = error "dest_set: set type expected"
-
-fun mk_mem (x,A) = 
-  let val setT = fastype_of A
-  in  Const("op :", [dest_set setT, setT]--->boolT) $ x $ A
-  end;
+open HOLogic;
 
 fun Int_const T = 
-  let val sT = mk_set T
+  let val sT = mk_setT T
   in  Const("op Int", [sT,sT]--->sT)  end;
 
-fun exists_const T = Const("Ex", [T-->boolT]--->boolT);
 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
 
-fun all_const T = Const("All", [T-->boolT]--->boolT);
 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
 
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) = 
-  let val T = dest_set (fastype_of A)
+  let val T = dest_setT (fastype_of A)
   in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
   end;
 
 (** Cartesian product type **)
 
+val unitT = Type("unit",[]);
+
 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
 
 (*Maps the type T1*...*Tn to [T1,...,Tn], if nested to the right*)
@@ -107,11 +85,6 @@
 	     Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2))
        | _ => h);
 
-fun Collect_const T = Const("Collect", [T-->boolT] ---> mk_set T);
-fun mk_Collect (a,T,t) = Collect_const T $ absfree(a, T, t);
-
-val Trueprop = Const("Trueprop",boolT-->propT);
-fun mk_tprop P = Trueprop $ P;
 
 
 (*simple error-checking in the premises of an inductive definition*)
@@ -149,4 +122,3 @@
      (fn _ => [assume_tac 1]);
 
 end;
-
diff -r 6be2f3e03786 -r fcf8024c920d indrule.ML
--- a/indrule.ML	Fri Nov 25 14:39:13 1994 +0100
+++ b/indrule.ML	Fri Nov 25 16:24:18 1994 +0100
@@ -25,7 +25,7 @@
 
 val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
 
-val elem_type = dest_set (body_type recT);
+val elem_type = dest_setT (body_type recT);
 val domTs = summands(elem_type);
 val big_rec_name = space_implode "_" rec_names;
 val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
@@ -44,7 +44,7 @@
 fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 
 		 (Const("op :",_)$t$X), iprems) =
      (case gen_assoc (op aconv) (ind_alist, X) of
-	  Some pred => prem :: mk_tprop (pred $ t) :: iprems
+	  Some pred => prem :: mk_Trueprop (pred $ t) :: iprems
 	| None => (*possibly membership in M(rec_tm), for M monotone*)
 	    let fun mk_sb (rec_tm,pred) = 
 		 (case binder_types (fastype_of pred) of
@@ -62,7 +62,7 @@
 			 (strip_imp_prems intr,[])
       val (t,X) = rule_concl intr
       val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
-      val concl = mk_tprop (pred $ t)
+      val concl = mk_Trueprop (pred $ t)
   in list_all_free (quantfrees, list_implies (iprems,concl)) end
   handle Bind => error"Recursion term not found in conclusion";
 
@@ -79,7 +79,7 @@
 val quant_induct = 
     prove_goalw_cterm part_rec_defs 
       (cterm_of sign (list_implies (ind_prems, 
-				    mk_tprop (mk_all_imp(big_rec_tm,pred)))))
+				    mk_Trueprop (mk_all_imp(big_rec_tm,pred)))))
       (fn prems =>
        [rtac (impI RS allI) 1,
 	etac raw_induct 1,
@@ -117,11 +117,11 @@
 
 (*To instantiate the main induction rule*)
 val induct_concl = 
- mk_tprop(mk_all_imp(big_rec_tm,
+ mk_Trueprop(mk_all_imp(big_rec_tm,
 		     Abs("z", elem_type, 
 			 fold_bal (app conj) 
 			          (map mk_rec_imp (rec_tms~~preds)))))
-and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
+and mutual_induct_concl = mk_Trueprop(fold_bal (app conj) qconcls);
 
 val lemma = (*makes the link between the two induction rules*)
     prove_goalw_cterm part_rec_defs 
diff -r 6be2f3e03786 -r fcf8024c920d intr_elim.ML
--- a/intr_elim.ML	Fri Nov 25 14:39:13 1994 +0100
+++ b/intr_elim.ML	Fri Nov 25 16:24:18 1994 +0100
@@ -66,7 +66,7 @@
 
 val mono = 
     prove_goalw_cterm [] 
-      (cterm_of sign (mk_tprop (Const("mono", monoT-->boolT) $ fp_abs)))
+      (cterm_of sign (mk_Trueprop (Const("mono", monoT-->boolT) $ fp_abs)))
       (fn _ =>
        [rtac monoI 1,
 	REPEAT (ares_tac (basic_monos @ monos) 1)]);