--- 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 =
--- 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);
--- 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;
-
--- 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
--- 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)]);