--- a/src/ZF/Inductive.ML Wed Dec 03 10:50:02 1997 +0100
+++ b/src/ZF/Inductive.ML Wed Dec 03 10:52:17 1997 +0100
@@ -13,7 +13,7 @@
*)
val iT = Ind_Syntax.iT
-and oT = Ind_Syntax.oT;
+and oT = FOLogic.oT;
structure Lfp =
struct
--- a/src/ZF/add_ind_def.ML Wed Dec 03 10:50:02 1997 +0100
+++ b/src/ZF/add_ind_def.ML Wed Dec 03 10:52:17 1997 +0100
@@ -119,8 +119,10 @@
let val prems = map dest_tprop (strip_imp_prems intr)
val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
val exfrees = term_frees intr \\ rec_params
- val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
- in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
+ val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
+ in foldr FOLogic.mk_exists
+ (exfrees, fold_bal (app FOLogic.conj) (zeq::prems))
+ end;
(*The Part(A,h) terms -- compose injections to make h*)
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
@@ -135,7 +137,8 @@
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
val lfp_abs = absfree(X', iT,
- mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
+ mk_Collect(z', dom_sum,
+ fold_bal (app FOLogic.disj) part_intrs));
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
--- a/src/ZF/constructor.ML Wed Dec 03 10:50:02 1997 +0100
+++ b/src/ZF/constructor.ML Wed Dec 03 10:52:17 1997 +0100
@@ -47,11 +47,12 @@
(*Each equation has the form
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) =
- Ind_Syntax.mk_tprop
- (Ind_Syntax.eq_const $
- (big_case_tm $
- (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), args))) $
- (list_comb (case_free, args)));
+ FOLogic.mk_Trueprop
+ (FOLogic.mk_eq
+ (big_case_tm $
+ (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T),
+ args)),
+ list_comb (case_free, args)));
val case_trans = hd con_defs RS Ind_Syntax.def_trans
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
--- a/src/ZF/ind_syntax.ML Wed Dec 03 10:50:02 1997 +0100
+++ b/src/ZF/ind_syntax.ML Wed Dec 03 10:52:17 1997 +0100
@@ -12,40 +12,22 @@
structure Ind_Syntax =
struct
-(** Abstract syntax definitions for FOL and ZF **)
-
-val iT = Type("i",[])
-and oT = Type("o",[]);
-
-
-(** Logical constants **)
+(** Abstract syntax definitions for ZF **)
-val conj = Const("op &", [oT,oT]--->oT)
-and disj = Const("op |", [oT,oT]--->oT)
-and imp = Const("op -->", [oT,oT]--->oT);
-
-val eq_const = Const("op =", [iT,iT]--->oT);
+val iT = Type("i",[]);
-val mem_const = Const("op :", [iT,iT]--->oT);
-
-val exists_const = Const("Ex", [iT-->oT]--->oT);
-fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
-
-val all_const = Const("All", [iT-->oT]--->oT);
-fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
+val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
- all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
+ FOLogic.all_const iT $
+ Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
-val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
+val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
-val Trueprop = Const("Trueprop",oT-->propT);
-fun mk_tprop P = Trueprop $ P;
-
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
error"Premises may not be conjuctive"
@@ -79,7 +61,7 @@
(*read a constructor specification*)
fun read_construct sign (id, sprems, syn) =
- let val prems = map (readtm sign oT) sprems
+ let val prems = map (readtm sign FOLogic.oT) sprems
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT
handle TERM _ => error
@@ -94,8 +76,10 @@
let
fun mk_intr ((id,T,syn), name, args, prems) =
Logic.list_implies
- (map mk_tprop prems,
- mk_tprop (mem_const $ list_comb (Const (Sign.full_name sg name, T), args) $ rec_tm))
+ (map FOLogic.mk_Trueprop prems,
+ FOLogic.mk_Trueprop
+ (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
+ $ rec_tm))
in map mk_intr constructs end;
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
--- a/src/ZF/indrule.ML Wed Dec 03 10:50:02 1997 +0100
+++ b/src/ZF/indrule.ML Wed Dec 03 10:52:17 1997 +0100
@@ -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 :: Ind_Syntax.mk_tprop (pred $ t) :: iprems
+ Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
| None => (*possibly membership in M(rec_tm), for M monotone*)
let fun mk_sb (rec_tm,pred) =
(rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
@@ -58,7 +58,7 @@
(Logic.strip_imp_prems intr,[])
val (t,X) = Ind_Syntax.rule_concl intr
val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
- val concl = Ind_Syntax.mk_tprop (pred $ t)
+ val concl = FOLogic.mk_Trueprop (pred $ t)
in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
handle Bind => error"Recursion term not found in conclusion";
@@ -69,7 +69,7 @@
DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
ind_tac prems (i-1);
-val pred = Free(pred_name, Ind_Syntax.iT --> Ind_Syntax.oT);
+val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms))
Inductive.intr_tms;
@@ -92,7 +92,7 @@
prove_goalw_cterm part_rec_defs
(cterm_of sign
(Logic.list_implies (ind_prems,
- Ind_Syntax.mk_tprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
+ FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
(fn prems =>
[rtac (impI RS allI) 1,
DETERM (etac Intr_elim.raw_induct 1),
@@ -120,14 +120,14 @@
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
- elem_factors ---> Ind_Syntax.oT)
+ elem_factors ---> FOLogic.oT)
val qconcl =
- foldr Ind_Syntax.mk_all
+ foldr FOLogic.mk_all
(elem_frees,
- Ind_Syntax.imp $
+ FOLogic.imp $
(Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
$ (list_comb (pfree, elem_frees)))
- in (CP.ap_split elem_type Ind_Syntax.oT pfree,
+ in (CP.ap_split elem_type FOLogic.oT pfree,
qconcl)
end;
@@ -135,19 +135,19 @@
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $
+ FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $
(pred $ Bound 0);
(*To instantiate the main induction rule*)
val induct_concl =
- Ind_Syntax.mk_tprop
+ FOLogic.mk_Trueprop
(Ind_Syntax.mk_all_imp
(big_rec_tm,
Abs("z", Ind_Syntax.iT,
- fold_bal (app Ind_Syntax.conj)
+ fold_bal (app FOLogic.conj)
(ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
and mutual_induct_concl =
- Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
+ FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
resolve_tac [allI, impI, conjI, Part_eqI],
@@ -241,7 +241,7 @@
in
struct
(*strip quantifier*)
- val induct = CP.split_rule_var(pred_var, elem_type-->Ind_Syntax.oT, induct0)
+ val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
|> standard;
(*Just "True" unless there's true mutual recursion. This saves storage.*)
--- a/src/ZF/intr_elim.ML Wed Dec 03 10:50:02 1997 +0100
+++ b/src/ZF/intr_elim.ML Wed Dec 03 10:52:17 1997 +0100
@@ -70,7 +70,7 @@
val bnd_mono =
prove_goalw_cterm []
- (cterm_of sign (Ind_Syntax.mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
+ (cterm_of sign (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
(fn _ =>
[rtac (Collect_subset RS bnd_monoI) 1,
REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);