# HG changeset patch # User paulson # Date 881142737 -3600 # Node ID 7ac9f3e8a97daff285767cf0e83b2ddeb0325998 # Parent 36b28f78ed1b906e6e9fe005a281195d1e02ee06 Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML diff -r 36b28f78ed1b -r 7ac9f3e8a97d src/ZF/Inductive.ML --- 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 diff -r 36b28f78ed1b -r 7ac9f3e8a97d src/ZF/add_ind_def.ML --- 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 diff -r 36b28f78ed1b -r 7ac9f3e8a97d src/ZF/constructor.ML --- 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; diff -r 36b28f78ed1b -r 7ac9f3e8a97d src/ZF/ind_syntax.ML --- 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); diff -r 36b28f78ed1b -r 7ac9f3e8a97d src/ZF/indrule.ML --- 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.*) diff -r 36b28f78ed1b -r 7ac9f3e8a97d src/ZF/intr_elim.ML --- 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)]);