--- a/src/HOL/Tools/Function/function.ML Mon Jun 17 13:36:09 2013 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Jun 17 17:30:54 2013 +0200
@@ -94,7 +94,7 @@
fun afterqed [[proof]] lthy =
let
- val FunctionResult {fs, R, psimps, simple_pinducts,
+ val FunctionResult {fs, R, dom, psimps, simple_pinducts,
termination, domintros, cases, ...} =
cont (Thm.close_derivation proof)
@@ -105,7 +105,7 @@
val addsmps = add_simps fnames post sort_cont
- val (((psimps', [pinducts']), (_, [termination'])), lthy) =
+ val ((((psimps', [pinducts']), [termination']), [cases']), lthy) =
lthy
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
@@ -114,15 +114,15 @@
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
Attrib.internal (K (Induct.induct_pred ""))])))]
- ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
- ||> (snd o Local_Theory.note ((qualify "cases",
+ ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
+ ||>> (apfst snd o Local_Theory.note ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
||> (case domintros of NONE => I | SOME thms =>
Local_Theory.note ((qualify "domintros", []), thms) #> snd)
val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
- fs=fs, R=R, defname=defname, is_partial=true }
+ fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=cases'}
val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
in
@@ -180,7 +180,7 @@
| NONE => error "Not a function"))
val { termination, fs, R, add_simps, case_names, psimps,
- pinducts, defname, ...} = info
+ pinducts, defname, cases, dom, ...} = info
val domT = domain_type (fastype_of R)
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
fun afterqed [[totality]] lthy =
@@ -203,8 +203,8 @@
tinduct)
|-> (fn (simps, (_, inducts)) => fn lthy =>
let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
- case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
- simps=SOME simps, inducts=SOME inducts, termination=termination }
+ case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
+ simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases }
in
(info',
lthy
--- a/src/HOL/Tools/Function/function_common.ML Mon Jun 17 13:36:09 2013 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Mon Jun 17 17:30:54 2013 +0200
@@ -16,11 +16,13 @@
case_names : string list,
fs : term list,
R : term,
+ dom: term,
psimps: thm list,
pinducts: thm list,
simps : thm list option,
inducts : thm list option,
- termination: thm}
+ termination : thm,
+ cases : thm}
end
@@ -36,11 +38,13 @@
case_names : string list,
fs : term list,
R : term,
+ dom: term,
psimps: thm list,
pinducts: thm list,
simps : thm list option,
inducts : thm list option,
- termination: thm}
+ termination : thm,
+ cases : thm}
end
@@ -59,6 +63,7 @@
{fs: term list,
G: term,
R: term,
+ dom: term,
psimps : thm list,
simple_pinducts : thm list,
cases : thm,
@@ -138,14 +143,15 @@
{fs: term list,
G: term,
R: term,
+ dom: term,
psimps : thm list,
simple_pinducts : thm list,
cases : thm,
termination : thm,
domintros : thm list option}
-fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
- simps, inducts, termination, defname, is_partial} : info) phi =
+fun transform_function_data ({add_simps, case_names, fs, R, dom, psimps, pinducts,
+ simps, inducts, termination, defname, is_partial, cases} : info) phi =
let
val term = Morphism.term phi
val thm = Morphism.thm phi
@@ -153,10 +159,10 @@
val name = Binding.name_of o Morphism.binding phi o Binding.name
in
{ add_simps = add_simps, case_names = case_names,
- fs = map term fs, R = term R, psimps = fact psimps,
+ fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
pinducts = fact pinducts, simps = Option.map fact simps,
inducts = Option.map fact inducts, termination = thm termination,
- defname = name defname, is_partial=is_partial }
+ defname = name defname, is_partial=is_partial, cases = thm cases }
end
(* FIXME just one data slot (record) per program unit *)
--- a/src/HOL/Tools/Function/function_core.ML Mon Jun 17 13:36:09 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Mon Jun 17 17:30:54 2013 +0200
@@ -863,8 +863,9 @@
val ((R, RIntro_thmss, R_elim), lthy) =
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
+ val dom = mk_acc domT R
val (_, lthy) =
- Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+ Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), dom) lthy
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
@@ -914,7 +915,7 @@
(map (mk_domain_intro lthy globals R R_elim)) xclauses)
else NONE
in
- FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+ FunctionResult {fs=[f], G=G, R=R, dom=dom, cases=complete_thm,
psimps=psimps, simple_pinducts=[simple_pinduct],
termination=total_intro, domintros=dom_intros}
end
--- a/src/HOL/Tools/Function/mutual.ML Mon Jun 17 13:36:09 2013 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Mon Jun 17 17:30:54 2013 +0200
@@ -252,7 +252,7 @@
let
val result = inner_cont proof
val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
- termination, domintros, ...} = result
+ termination, domintros, dom, ...} = result
val (all_f_defs, fs) =
map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -272,7 +272,7 @@
val mtermination = full_simplify rew_simpset termination
val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros
in
- FunctionResult { fs=fs, G=G, R=R,
+ FunctionResult { fs=fs, G=G, R=R, dom=dom,
psimps=mpsimps, simple_pinducts=minducts,
cases=cases, termination=mtermination,
domintros=mdomintros}