# HG changeset patch # User wenzelm # Date 1564056066 -7200 # Node ID c533bec6e92d4ae56204ede744334ae0d8563844 # Parent cafffcb7d383c7523ea17ad2b07e05d57f3bf86d more accurate proof definitions (PThm nodes); diff -r cafffcb7d383 -r c533bec6e92d src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Wed Jul 24 15:41:24 2019 +0200 +++ b/src/ZF/Tools/datatype_package.ML Thu Jul 25 14:01:06 2019 +0200 @@ -293,13 +293,20 @@ val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]); - val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs); + val ([case_eqns], thy2) = thy1 + |> Sign.add_path big_rec_base_name + |> Global_Theory.add_thmss + [((Binding.name "case_eqns", + map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs)), [])] + ||> Sign.parent_path; + (*** Prove the recursor theorems ***) - val recursor_eqns = case try (Misc_Legacy.get_def thy1) recursor_base_name of + val (recursor_eqns, thy3) = + case try (Misc_Legacy.get_def thy2) recursor_base_name of NONE => (writeln " [ No recursion operator ]"; - []) + ([], thy2)) | SOME recursor_def => let (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *) @@ -316,22 +323,28 @@ FOLogic.mk_Trueprop (FOLogic.mk_eq (recursor_tm $ - (list_comb (Const (Sign.intern_const thy1 name,T), + (list_comb (Const (Sign.intern_const thy2 name,T), args)), subst_rec (Term.betapplys (recursor_case, args)))); val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS @{thm trans}; fun prove_recursor_eqn arg = - Goal.prove_global thy1 [] [] - (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg)) + Goal.prove_global thy2 [] [] + (Ind_Syntax.traceIt "next recursor equation = " thy2 (mk_recursor_eqn arg)) (*Proves a single recursor equation.*) (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt [recursor_trans] 1, simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1, IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]); in - map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases) + thy2 + |> Sign.add_path big_rec_base_name + |> Global_Theory.add_thmss + [((Binding.name "recursor_eqns", + map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)), [])] + ||> Sign.parent_path + |>> the_single end val constructors = @@ -375,17 +388,13 @@ in (*Updating theory components: simprules and datatype info*) - (thy1 |> Sign.add_path big_rec_base_name + (thy3 |> Sign.add_path big_rec_base_name |> Global_Theory.add_thmss - [((Binding.name "case_eqns", case_eqns), []), - ((Binding.name "recursor_eqns", recursor_eqns), []), + [((Binding.name "simps", case_eqns @ recursor_eqns), [Simplifier.simp_add]), ((Binding.empty, intrs), [Cla.safe_intro NONE]), ((Binding.name "con_defs", con_defs), []), ((Binding.name "free_iffs", free_iffs), []), - ((Binding.name "free_elims", free_SEs), [])] - |-> (fn simps1 :: simps2 :: _ => - Global_Theory.add_thmss - [((Binding.name "simps", simps1 @ simps2), [Simplifier.simp_add])]) |> #2 + ((Binding.name "free_elims", free_SEs), [])] |> #2 |> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) |> ConstructorsData.map (fold Symtab.update con_pairs) |> Sign.parent_path, diff -r cafffcb7d383 -r c533bec6e92d src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Wed Jul 24 15:41:24 2019 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu Jul 25 14:01:06 2019 +0200 @@ -172,8 +172,6 @@ |> Sign.add_path big_rec_base_name |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs); - val ctxt1 = Proof_Context.init_global thy1; - (*fetch fp definitions from the theory*) val big_rec_def::part_rec_defs = @@ -185,12 +183,15 @@ (********) val dummy = writeln " Proving monotonicity..."; - val bnd_mono = + val bnd_mono0 = Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1, REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]); + val (bnd_mono, thy2) = thy1 + |> Global_Theory.add_thm ((Binding.name "bnd_mono", bnd_mono0), []) + val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs); val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski); @@ -241,12 +242,18 @@ right = fn rl => rl RS @{thm disjI2}, init = @{thm asm_rl}}; - val intrs = + val intrs0 = (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms))) |> ListPair.map (fn (t, tacs) => - Goal.prove_global thy1 [] [] t + Goal.prove_global thy2 [] [] t (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt))); + val ([intrs], thy3) = thy2 + |> Global_Theory.add_thmss [((Binding.name "intros", intrs0), [])]; + + val ctxt3 = Proof_Context.init_global thy3; + + (********) val dummy = writeln " Proving the elimination rule..."; @@ -259,8 +266,12 @@ THEN (PRIMITIVE (fold_rule ctxt part_rec_defs)); (*Elimination*) - val elim = - rule_by_tactic ctxt1 (basic_elim_tac ctxt1) (unfold RS Ind_Syntax.equals_CollectD) + val (elim, thy4) = thy3 + |> Global_Theory.add_thm + ((Binding.name "elim", + rule_by_tactic ctxt3 (basic_elim_tac ctxt3) (unfold RS Ind_Syntax.equals_CollectD)), []); + + val ctxt4 = Proof_Context.init_global thy4; (*Applies freeness of the given constructors, which *must* be unfolded by the given defs. Cannot simply use the local con_defs because @@ -272,7 +283,7 @@ (Thm.assume A RS elim) |> Drule.export_without_context_open; - fun induction_rules raw_induct thy = + fun induction_rules raw_induct = let val dummy = writeln " Proving the induction rule..."; @@ -318,15 +329,15 @@ val dummy = if ! Ind_Syntax.trace then writeln (cat_lines - (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @ - ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct])) + (["ind_prems:"] @ map (Syntax.string_of_term ctxt4) ind_prems @ + ["raw_induct:", Thm.string_of_thm ctxt4 raw_induct])) else (); (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. If the premises get simplified, then the proofs could fail.*) val min_ss = - (empty_simpset (Proof_Context.init_global thy) + (empty_simpset (Proof_Context.init_global thy4) |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)) setSolver (mk_solver "minimal" (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) @@ -334,7 +345,7 @@ ORELSE' eresolve_tac ctxt @{thms FalseE})); val quant_induct = - Goal.prove_global thy [] ind_prems + Goal.prove_global thy4 [] ind_prems (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred))) (fn {context = ctxt, prems} => EVERY [rewrite_goals_tac ctxt part_rec_defs, @@ -352,7 +363,7 @@ val dummy = if ! Ind_Syntax.trace then - writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct) + writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt4 quant_induct) else (); @@ -404,9 +415,9 @@ val dummy = if !Ind_Syntax.trace then (writeln ("induct_concl = " ^ - Syntax.string_of_term ctxt1 induct_concl); + Syntax.string_of_term ctxt4 induct_concl); writeln ("mutual_induct_concl = " ^ - Syntax.string_of_term ctxt1 mutual_induct_concl)) + Syntax.string_of_term ctxt4 mutual_induct_concl)) else (); @@ -420,7 +431,7 @@ val lemma = (*makes the link between the two induction rules*) if need_mutual then (writeln " Proving the mutual induction rule..."; - Goal.prove_global thy [] [] + Goal.prove_global thy4 [] [] (Logic.mk_implies (induct_concl, mutual_induct_concl)) (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt part_rec_defs, @@ -429,7 +440,7 @@ val dummy = if ! Ind_Syntax.trace then - writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma) + writeln ("lemma: " ^ Thm.string_of_thm ctxt4 lemma) else (); @@ -480,7 +491,7 @@ val mutual_induct_fsplit = if need_mutual then - Goal.prove_global thy [] (map (induct_prem (rec_tms~~preds)) intr_tms) + Goal.prove_global thy4 [] (map (induct_prem (rec_tms~~preds)) intr_tms) mutual_induct_concl (fn {context = ctxt, prems} => EVERY [resolve_tac ctxt [quant_induct RS lemma] 1, @@ -495,7 +506,7 @@ val inst = case elem_frees of [_] => I | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)), - Thm.global_cterm_of thy elem_tuple)]); + Thm.global_cterm_of thy4 elem_tuple)]); (*strip quantifier and the implication*) val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp})); @@ -503,50 +514,47 @@ val Const (\<^const_name>\Trueprop\, _) $ (pred_var $ _) = Thm.concl_of induct0 val induct = - CP.split_rule_var (Proof_Context.init_global thy) + CP.split_rule_var (Proof_Context.init_global thy4) (pred_var, elem_type-->FOLogic.oT, induct0) |> Drule.export_without_context - and mutual_induct = CP.remove_split (Proof_Context.init_global thy) mutual_induct_fsplit + and mutual_induct = CP.remove_split (Proof_Context.init_global thy4) mutual_induct_fsplit val ([induct', mutual_induct'], thy') = - thy + thy4 |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct), [case_names, Induct.induct_pred big_rec_name]), ((Binding.name "mutual_induct", mutual_induct), [case_names])]; - in ((thy', induct'), mutual_induct') + in ((induct', mutual_induct'), thy') end; (*of induction_rules*) val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct) - val ((thy2, induct), mutual_induct) = - if not coind then induction_rules raw_induct thy1 + val ((induct, mutual_induct), thy5) = + if not coind then induction_rules raw_induct else - (thy1 + thy4 |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])] - |> apfst hd |> Library.swap, @{thm TrueI}) + |> apfst (hd #> pair @{thm TrueI}) and defs = big_rec_def :: part_rec_defs - val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) = - thy2 + val (([dom_subset', elim'], [defs']), thy6) = + thy5 |> IndCases.declare big_rec_name make_cases |> Global_Theory.add_thms - [((Binding.name "bnd_mono", bnd_mono), []), - ((Binding.name "dom_subset", dom_subset), []), + [((Binding.name "dom_subset", dom_subset), []), ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])] - ||>> (Global_Theory.add_thmss o map Thm.no_attributes) - [(Binding.name "defs", defs), - (Binding.name "intros", intrs)]; - val (intrs'', thy4) = - thy3 - |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs) + ||>> (Global_Theory.add_thmss o map Thm.no_attributes) [(Binding.name "defs", defs)]; + val (intrs', thy7) = + thy6 + |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs) ~~ map #2 intr_specs) ||> Sign.parent_path; in - (thy4, + (thy7, {defs = defs', - bnd_mono = bnd_mono', + bnd_mono = bnd_mono, dom_subset = dom_subset', - intrs = intrs'', + intrs = intrs', elim = elim', induct = induct, mutual_induct = mutual_induct})