ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted
ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify
--- a/src/ZF/constructor.ML Thu Aug 18 12:56:57 1994 +0200
+++ b/src/ZF/constructor.ML Thu Aug 18 17:41:40 1994 +0200
@@ -41,7 +41,7 @@
(*Get the case term from its definition*)
val Const("==",_) $ big_case_tm $ _ =
- hd con_defs |> rep_thm |> #prop |> unvarify;
+ hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
val (_, big_case_args) = strip_comb big_case_tm;
@@ -62,8 +62,9 @@
Su.case_inr RS trans] 1)];
fun prove_case_equation (arg,con_def) =
- prove_term (sign_of thy) []
- (mk_case_equation arg, case_tacsf con_def);
+ prove_goalw_cterm []
+ (cterm_of (sign_of thy) (mk_case_equation arg))
+ (case_tacsf con_def);
val free_iffs =
map standard (con_defs RL [def_swap_iff]) @
--- a/src/ZF/ind_syntax.ML Thu Aug 18 12:56:57 1994 +0200
+++ b/src/ZF/ind_syntax.ML Thu Aug 18 17:41:40 1994 +0200
@@ -14,28 +14,12 @@
(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
fun mk_defpair (lhs, rhs) =
let val Const(name, _) = head_of lhs
- val dummy = assert (term_vars rhs subset term_vars lhs
- andalso
- term_frees rhs subset term_frees lhs
- andalso
- term_tvars rhs subset term_tvars lhs
- andalso
- term_tfrees rhs subset term_tfrees lhs)
- ("Extra variables on RHS in definition of " ^ name)
in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
fun get_def thy s = get_axiom thy (s^"_def");
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
-(*export to Pure/library? *)
-fun assert_all pred l msg_fn =
- let fun asl [] = ()
- | asl (x::xs) = if pred x then asl xs
- else error (msg_fn x)
- in asl l end;
-
-
(** Abstract syntax definitions for FOL and ZF **)
val iT = Type("i",[])
@@ -78,15 +62,6 @@
val Trueprop = Const("Trueprop",oT-->propT);
fun mk_tprop P = Trueprop $ P;
-(*Prove a goal stated as a term, with exception handling*)
-fun prove_term sign defs (P,tacsf) =
- let val ct = cterm_of sign P
- in prove_goalw_cterm defs ct tacsf
- handle e => (writeln ("Exception in proof of\n" ^
- string_of_cterm ct);
- raise e)
- end;
-
(*Read an assumption in the given theory*)
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
@@ -127,21 +102,6 @@
| chk_prem rec_hd t =
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
-
-(*Inverse of varifyT. Move to Pure/type.ML?*)
-fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
- | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
- | unvarifyT T = T;
-
-(*Inverse of varify. Move to Pure/logic.ML?*)
-fun unvarify (Const(a,T)) = Const(a, unvarifyT T)
- | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
- | unvarify (Var(ixn,T)) = Var(ixn, unvarifyT T) (*non-zero index!*)
- | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
- | unvarify (f$t) = unvarify f $ unvarify t
- | unvarify t = t;
-
-
(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []
| mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
--- a/src/ZF/indrule.ML Thu Aug 18 12:56:57 1994 +0200
+++ b/src/ZF/indrule.ML Thu Aug 18 17:41:40 1994 +0200
@@ -69,9 +69,10 @@
val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
val quant_induct =
- prove_term sign part_rec_defs
- (list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),
- fn prems =>
+ prove_goalw_cterm part_rec_defs
+ (cterm_of sign (list_implies (ind_prems,
+ mk_tprop (mk_all_imp(big_rec_tm,pred)))))
+ (fn prems =>
[rtac (impI RS allI) 1,
etac raw_induct 1,
REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])),
@@ -118,9 +119,9 @@
and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
val lemma = (*makes the link between the two induction rules*)
- prove_term sign part_rec_defs
- (mk_implies (induct_concl,mutual_induct_concl),
- fn prems =>
+ prove_goalw_cterm part_rec_defs
+ (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
+ (fn prems =>
[cut_facts_tac prems 1,
REPEAT (eresolve_tac [asm_rl,conjE,PartE,mp] 1
ORELSE resolve_tac [allI,impI,conjI,Part_eqI] 1
@@ -145,10 +146,11 @@
i THEN mutual_ind_tac prems (i-1);
val mutual_induct_fsplit =
- prove_term sign []
- (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
- mutual_induct_concl),
- fn prems =>
+ prove_goalw_cterm []
+ (cterm_of sign
+ (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
+ mutual_induct_concl)))
+ (fn prems =>
[rtac (quant_induct RS lemma) 1,
mutual_ind_tac (rev prems) (length prems)]);
--- a/src/ZF/intr_elim.ML Thu Aug 18 12:56:57 1994 +0200
+++ b/src/ZF/intr_elim.ML Thu Aug 18 17:41:40 1994 +0200
@@ -60,11 +60,12 @@
val _ = writeln " Proving monotonicity...";
val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
- big_rec_def |> rep_thm |> #prop |> unvarify;
+ big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
val bnd_mono =
- prove_term sign [] (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs),
- fn _ =>
+ prove_goalw_cterm []
+ (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
+ (fn _ =>
[rtac (Collect_subset RS bnd_monoI) 1,
REPEAT (ares_tac (basic_monos @ monos) 1)]);
@@ -102,8 +103,9 @@
and g rl = rl RS disjI2
in accesses_bal(f, g, asm_rl) end;
-val intrs = map (prove_term sign part_rec_defs)
- (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
+val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
+ (map (cterm_of sign) intr_tms ~~
+ map intro_tacsf (mk_disj_rls(length intr_tms)));
(********)
val _ = writeln " Proving the elimination rule...";