# HG changeset patch # User krauss # Date 1371483054 -7200 # Node ID 23acfc1f3fc4bad9fad6614a86542627a9f03442 # Parent 80c00a851de590d6314b47d803127bfa385d23ae# Parent 741d10d7f2c15e4a3fb0e8ce9db5137f0a860c03 merged diff -r 741d10d7f2c1 -r 23acfc1f3fc4 src/HOL/Tools/Function/function.ML --- 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 diff -r 741d10d7f2c1 -r 23acfc1f3fc4 src/HOL/Tools/Function/function_common.ML --- 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 *) diff -r 741d10d7f2c1 -r 23acfc1f3fc4 src/HOL/Tools/Function/function_core.ML --- 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 diff -r 741d10d7f2c1 -r 23acfc1f3fc4 src/HOL/Tools/Function/mutual.ML --- 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}