# HG changeset patch # User lcp # Date 777224500 -7200 # Node ID e961b2092869f9188f3fdbe6b04631a305df2971 # Parent 164be35c8a16964092adfd5d2fe53100248d9c85 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 diff -r 164be35c8a16 -r e961b2092869 src/ZF/constructor.ML --- 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]) @ diff -r 164be35c8a16 -r e961b2092869 src/ZF/ind_syntax.ML --- 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; diff -r 164be35c8a16 -r e961b2092869 src/ZF/indrule.ML --- 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)]); diff -r 164be35c8a16 -r e961b2092869 src/ZF/intr_elim.ML --- 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...";