# HG changeset patch # User wenzelm # Date 1433258821 -7200 # Node ID fd5052b1881f860b61a266fb28869ccc593eb283 # Parent 5568b16aa477e42c5e5ab42d69b596c2de052d9c cleaified context; more uniform context data; tuned; diff -r 5568b16aa477 -r fd5052b1881f src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Tue Jun 02 13:55:43 2015 +0200 +++ b/src/HOL/Tools/TFL/post.ML Tue Jun 02 17:27:01 2015 +0200 @@ -7,10 +7,10 @@ signature TFL = sig - val define_i: bool -> Proof.context -> thm list -> thm list -> xstring -> term -> term list -> - theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory - val define: bool -> Proof.context -> thm list -> thm list -> xstring -> string -> string list -> - theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory + val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context -> + {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context + val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context -> + {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context val defer_i: thm list -> xstring -> term list -> theory -> thm * theory val defer: thm list -> xstring -> string list -> theory -> thm * theory end; @@ -34,13 +34,13 @@ * non-proved termination conditions, and finally attempts to prove the * simplified termination conditions. *--------------------------------------------------------------------------*) -fun std_postprocessor strict ctxt wfs = - Prim.postprocess strict +fun std_postprocessor ctxt strict wfs = + Prim.postprocess ctxt strict {wf_tac = REPEAT (ares_tac wfs 1), terminator = asm_simp_tac ctxt 1 THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE - fast_force_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1), + fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1), simplifier = Rules.simpl_conv ctxt []}; @@ -84,13 +84,15 @@ end val gen_all = USyntax.gen_all in -fun proof_stage strict ctxt wfs theory {f, R, rules, full_pats_TCs, TCs} = +fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} = let val _ = writeln "Proving induction theorem ..." - val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} + val ind = + Prim.mk_induction (Proof_Context.theory_of ctxt) + {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} val _ = writeln "Postprocessing ..."; val {rules, induction, nested_tcs} = - std_postprocessor strict ctxt wfs theory {rules=rules, induction=ind, TCs=TCs} + std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs} in case nested_tcs of [] => {induction=induction, rules=rules,tcs=[]} @@ -134,29 +136,28 @@ fun tracing true _ = () | tracing false msg = writeln msg; -fun simplify_defn strict thy ctxt congs wfs id pats def0 = - let - val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq - val {rules,rows,TCs,full_pats_TCs} = - Prim.post_definition congs thy ctxt (def, pats) - val {lhs=f,rhs} = USyntax.dest_eq (concl def) - val (_,[R,_]) = USyntax.strip_comb rhs - val dummy = Prim.trace_thms ctxt "congs =" congs - (*the next step has caused simplifier looping in some cases*) - val {induction, rules, tcs} = - proof_stage strict ctxt wfs thy - {f = f, R = R, rules = rules, - full_pats_TCs = full_pats_TCs, - TCs = TCs} - val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt) - (Rules.CONJUNCTS rules) - in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')), - rules = ListPair.zip(rules', rows), - tcs = (termination_goals rules') @ tcs} - end +fun simplify_defn ctxt strict congs wfs id pats def0 = + let + val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq + val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats) + val {lhs=f,rhs} = USyntax.dest_eq (concl def) + val (_,[R,_]) = USyntax.strip_comb rhs + val dummy = Prim.trace_thms ctxt "congs =" congs + (*the next step has caused simplifier looping in some cases*) + val {induction, rules, tcs} = + proof_stage ctxt strict wfs + {f = f, R = R, rules = rules, + full_pats_TCs = full_pats_TCs, + TCs = TCs} + val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt) + (Rules.CONJUNCTS rules) + in + {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')), + rules = ListPair.zip(rules', rows), + tcs = (termination_goals rules') @ tcs} + end handle Utils.ERR {mesg,func,module} => - error (mesg ^ - "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); + error (mesg ^ "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); (* Derive the initial equations from the case-split rules to meet the @@ -184,21 +185,21 @@ (*--------------------------------------------------------------------------- * Defining a function with an associated termination relation. *---------------------------------------------------------------------------*) -fun define_i strict ctxt congs wfs fid R eqs thy = - let val {functional,pats} = Prim.mk_functional thy eqs - val (thy, def) = Prim.wfrec_definition0 thy fid R functional - val ctxt = Proof_Context.transfer thy ctxt - val (lhs, _) = Logic.dest_equals (Thm.prop_of def) - val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def - val rules' = - if strict then derive_init_eqs ctxt rules eqs - else rules - in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end; +fun define_i strict congs wfs fid R eqs ctxt = + let + val thy = Proof_Context.theory_of ctxt + val {functional, pats} = Prim.mk_functional thy eqs + val (def, thy') = Prim.wfrec_definition0 fid R functional thy + val ctxt' = Proof_Context.transfer thy' ctxt + val (lhs, _) = Logic.dest_equals (Thm.prop_of def) + val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs fid pats def + val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules + in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end; -fun define strict ctxt congs wfs fid R seqs thy = - define_i strict ctxt congs wfs fid - (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) thy - handle Utils.ERR {mesg,...} => error mesg; +fun define strict congs wfs fid R seqs ctxt = + define_i strict congs wfs fid + (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt + handle Utils.ERR {mesg,...} => error mesg; (*--------------------------------------------------------------------------- diff -r 5568b16aa477 -r fd5052b1881f src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 13:55:43 2015 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 17:27:01 2015 +0200 @@ -11,8 +11,8 @@ val trace_cterm: Proof.context -> string -> cterm -> unit type pattern val mk_functional: theory -> term list -> {functional: term, pats: pattern list} - val wfrec_definition0: theory -> string -> term -> term -> theory * thm - val post_definition: thm list -> theory -> Proof.context -> thm * pattern list -> + val wfrec_definition0: string -> term -> term -> theory -> thm * theory + val post_definition: Proof.context -> thm list -> thm * pattern list -> {rules: thm, rows: int list, TCs: term list list, @@ -32,9 +32,10 @@ patterns : pattern list} val mk_induction: theory -> {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm - val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} - -> theory -> {rules: thm, induction: thm, TCs: term list list} - -> {rules: thm, induction: thm, nested_tcs: thm list} + val postprocess: Proof.context -> bool -> + {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> + {rules: thm, induction: thm, TCs: term list list} -> + {rules: thm, induction: thm, nested_tcs: thm list} end; structure Prim: PRIM = @@ -364,21 +365,23 @@ | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort) | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort); -local val f_eq_wfrec_R_M = - #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY)))) - val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M - val (fname,_) = dest_Free f - val (wfrec,_) = USyntax.strip_comb rhs +local + val f_eq_wfrec_R_M = + #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY)))) + val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M + val (fname,_) = dest_Free f + val (wfrec,_) = USyntax.strip_comb rhs in -fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) = - let val def_name = Thm.def_name (Long_Name.base_name fid) - val wfrec_R_M = map_types poly_tvars - (wfrec $ map_types poly_tvars R) - $ functional - val def_term = const_def thy (fid, Ty, wfrec_R_M) - val ([def], thy') = + +fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy = + let + val def_name = Thm.def_name (Long_Name.base_name fid) + val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional + val def_term = const_def thy (fid, Ty, wfrec_R_M) + val ([def], thy') = Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy - in (thy', def) end; + in (def, thy') end; + end; @@ -415,8 +418,9 @@ fun givens pats = map pat_of (filter given pats); -fun post_definition meta_tflCongs theory ctxt (def, pats) = - let val tych = Thry.typecheck theory +fun post_definition ctxt meta_tflCongs (def, pats) = + let val thy = Proof_Context.theory_of ctxt + val tych = Thry.typecheck thy val f = #lhs(USyntax.dest_eq(concl def)) val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def val pats' = filter given pats @@ -425,9 +429,8 @@ val WFR = #ant(USyntax.dest_imp(concl corollary)) val R = #Rand(USyntax.dest_comb WFR) val corollary' = Rules.UNDISCH corollary (* put WF R on assums *) - val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') - given_pats - val (case_rewrites,context_congs) = extraction_thms theory + val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats + val (case_rewrites,context_congs) = extraction_thms thy (*case_ss causes minimal simplification: bodies of case expressions are not simplified. Otherwise large examples (Red-Black trees) are too slow.*) @@ -435,7 +438,7 @@ put_simpset HOL_basic_ss ctxt addsimps case_rewrites |> fold (Simplifier.add_cong o #case_cong_weak o snd) - (Symtab.dest (BNF_LFP_Compat.get_all theory [BNF_LFP_Compat.Keep_Nesting])) + (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting])) val corollaries' = map (Simplifier.simplify case_simpset) corollaries val extract = Rules.CONTEXT_REWRITE_RULE (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs) @@ -911,14 +914,15 @@ else (); -fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} = -let val ctxt = Proof_Context.init_global theory; - val tych = Thry.typecheck theory; +fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} = + let + val thy = Proof_Context.theory_of ctxt; + val tych = Thry.typecheck thy; (*--------------------------------------------------------------------- * Attempt to eliminate WF condition. It's the only assumption of rules *---------------------------------------------------------------------*) - val (rules1,induction1) = + val (rules1,induction1) = let val thm = Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac) in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction) @@ -947,7 +951,7 @@ (r,ind) handle Utils.ERR _ => (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq), - simplify_induction theory tc_eq ind)) + simplify_induction thy tc_eq ind)) end (*---------------------------------------------------------------------- diff -r 5568b16aa477 -r fd5052b1881f src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Tue Jun 02 13:55:43 2015 +0200 +++ b/src/HOL/Tools/recdef.ML Tue Jun 02 17:27:01 2015 +0200 @@ -85,7 +85,7 @@ type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}; -structure GlobalRecdefData = Theory_Data +structure Data = Generic_Data ( type T = recdef_info Symtab.table * hints; val empty = (Symtab.empty, mk_hints ([], [], [])): T; @@ -99,28 +99,15 @@ Thm.merge_thms (wfs1, wfs2))); ); -val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get; - -fun put_recdef name info thy = - let - val (tab, hints) = GlobalRecdefData.get thy; - val tab' = Symtab.update_new (name, info) tab - handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name); - in GlobalRecdefData.put (tab', hints) thy end; - -val get_global_hints = #2 o GlobalRecdefData.get; +val get_recdef = Symtab.lookup o #1 o Data.get o Context.Theory; - -(* proof data *) +fun put_recdef name info = + (Context.theory_map o Data.map o apfst) (fn tab => + Symtab.update_new (name, info) tab + handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name)); -structure LocalRecdefData = Proof_Data -( - type T = hints; - val init = get_global_hints; -); - -val get_hints = LocalRecdefData.get; -fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f); +val get_hints = #2 o Data.get o Context.Proof; +val map_hints = Data.map o apsnd; (* attributes *) @@ -155,25 +142,23 @@ -(** prepare_hints(_i) **) +(** prepare hints **) -fun prepare_hints thy opt_src = +fun prepare_hints opt_src ctxt = let - val ctxt0 = Proof_Context.init_global thy; - val ctxt = + val ctxt' = (case opt_src of - NONE => ctxt0 - | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0)); + NONE => ctxt + | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt)); + val {simps, congs, wfs} = get_hints ctxt'; + val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong}; + in ((rev (map snd congs), wfs), ctxt'') end; + +fun prepare_hints_i () ctxt = + let val {simps, congs, wfs} = get_hints ctxt; val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong}; - in (ctxt', rev (map snd congs), wfs) end; - -fun prepare_hints_i thy () = - let - val ctxt = Proof_Context.init_global thy; - val {simps, congs, wfs} = get_global_hints thy; - val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong}; - in (ctxt', rev (map snd congs), wfs) end; + in ((rev (map snd congs), wfs), ctxt') end; @@ -190,30 +175,30 @@ val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs); val eq_atts = map (map (prep_att thy)) raw_eq_atts; - val (ctxt, congs, wfs) = prep_hints thy hints; + val ((congs, wfs), ctxt) = prep_hints hints (Proof_Context.init_global thy); (*We must remove imp_cong to prevent looping when the induction rule is simplified. Many induction rules have nested implications that would give rise to looping conditional rewriting.*) - val ({lhs, rules = rules_idx, induct, tcs}, thy) = - tfl_fn not_permissive ctxt congs wfs name R eqs thy; + val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) = + tfl_fn not_permissive congs wfs name R eqs ctxt; val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx); val simp_att = if null tcs then [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute] else []; - val ((simps' :: rules', [induct']), thy) = - thy + val ((simps' :: rules', [induct']), thy2) = + Proof_Context.theory_of ctxt1 |> Sign.add_path bname |> Global_Theory.add_thmss (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])] ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules); val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs}; - val thy = - thy + val thy3 = + thy2 |> put_recdef name result |> Sign.parent_path; - in (thy, result) end; + in (thy3, result) end; val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints; fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();