--- 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;
(*---------------------------------------------------------------------------
--- 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
(*----------------------------------------------------------------------
--- 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 ();