# HG changeset patch # User krauss # Date 1240300405 -7200 # Node ID 63b8b2b52f56d4f38e88001c703901bd37569282 # Parent 3c7a76e79898668855d22d8d39e444b7bd0bcade inlined afterqeds to improve clarity; tuned diff -r 3c7a76e79898 -r 63b8b2b52f56 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 21 09:53:24 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 21 09:53:25 2009 +0200 @@ -67,40 +67,6 @@ fold2 add_for_f fnames simps_by_f lthy) end -fun fundef_afterqed do_print fixes post defname cont sort_cont cnames [[proof]] lthy = - let - val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, domintros, cases, ...} = - cont (Thm.close_derivation proof) - - val fnames = map (fst o fst) fixes - val qualify = Long_Name.qualify defname - val addsmps = add_simps fnames post sort_cont - - val (((psimps', pinducts'), (_, [termination'])), lthy) = - lthy - |> addsmps (Binding.qualify false "partial") "psimps" - psimp_attribs psimps - ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps - ||>> note_theorem ((qualify "pinduct", - [Attrib.internal (K (RuleCases.case_names cnames)), - Attrib.internal (K (RuleCases.consumes 1)), - Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) - ||>> note_theorem ((qualify "termination", []), [termination]) - ||> (snd o note_theorem ((qualify "cases", - [Attrib.internal (K (RuleCases.case_names cnames))]), [cases])) - ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros - - val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', - pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname } - val _ = - if not do_print then () - else Specification.print_consts lthy (K false) (map fst fixes) - in - lthy - |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata) - end - - fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy = let val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) @@ -114,7 +80,40 @@ val ((goalstate, cont), lthy) = FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy - val afterqed = fundef_afterqed is_external fixes post defname cont sort_cont cnames + fun afterqed [[proof]] lthy = + let + val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, + domintros, cases, ...} = + cont (Thm.close_derivation proof) + + val fnames = map (fst o fst) fixes + val qualify = Long_Name.qualify defname + val addsmps = add_simps fnames post sort_cont + + val (((psimps', pinducts'), (_, [termination'])), lthy) = + lthy + |> addsmps (Binding.qualify false "partial") "psimps" + psimp_attribs psimps + ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps + ||>> note_theorem ((qualify "pinduct", + [Attrib.internal (K (RuleCases.case_names cnames)), + Attrib.internal (K (RuleCases.consumes 1)), + Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) + ||>> note_theorem ((qualify "termination", []), [termination]) + ||> (snd o note_theorem ((qualify "cases", + [Attrib.internal (K (RuleCases.case_names cnames))]), [cases])) + ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros + + val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', + pinducts=snd pinducts', termination=termination', + fs=fs, R=R, defname=defname } + val _ = + if not is_external then () + else Specification.print_consts lthy (K false) (map fst fixes) + in + lthy + |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata) + end in lthy |> is_external ? LocalTheory.set_group (serial_string ()) @@ -125,25 +124,6 @@ val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type" - -fun total_termination_afterqed data [[totality]] lthy = - let - val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data - - val totality = Thm.close_derivation totality - - val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) - - val tsimps = map remove_domain_condition psimps - val tinduct = map remove_domain_condition pinducts - - val qualify = Long_Name.qualify defname; - in - lthy - |> add_simps I "simps" simp_attribs tsimps |> snd - |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd - end - fun gen_termination_proof prep_term raw_term_opt lthy = let val term_opt = Option.map (prep_term lthy) raw_term_opt @@ -153,17 +133,37 @@ error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function")) - val FundefCtxData {termination, R, ...} = data + val FundefCtxData { termination, R, add_simps, case_names, psimps, + pinducts, defname, ...} = data val domT = domain_type (fastype_of R) - val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) + val goal = HOLogic.mk_Trueprop + (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) + fun afterqed [[totality]] lthy = + let + val totality = Thm.close_derivation totality + val remove_domain_condition = + full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) + val tsimps = map remove_domain_condition psimps + val tinduct = map remove_domain_condition pinducts + val qualify = Long_Name.qualify defname; + in + lthy + |> add_simps I "simps" simp_attribs tsimps |> snd + |> note_theorem + ((qualify "induct", + [Attrib.internal (K (RuleCases.case_names case_names))]), + tinduct) |> snd + end in lthy - |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" - [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]), - [([Goal.norm_result termination], [])])] |> snd - |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]] + |> ProofContext.note_thmss "" + [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd + |> ProofContext.note_thmss "" + [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd + |> ProofContext.note_thmss "" + [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]), + [([Goal.norm_result termination], [])])] |> snd + |> Proof.theorem_i NONE afterqed [[(goal, [])]] end val termination_proof = gen_termination_proof Syntax.check_term; @@ -198,8 +198,9 @@ (* setup *) val setup = - Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del) - "declaration of congruence rule for function definitions" + Attrib.setup @{binding fundef_cong} + (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del) + "declaration of congruence rule for function definitions" #> setup_case_cong #> FundefRelation.setup #> FundefCommon.TerminationSimps.setup