# HG changeset patch # User Christian Urban # Date 1311007213 -3600 # Node ID d1038e67923a95e2fa23f4de08ceddd32a567123 # Parent 84afb941df53a7877aa71d9b4365251bf5b3a084 added a flag (eqvt) to termination proofs arising fron nominal_primrecs diff -r 84afb941df53 -r d1038e67923a Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/Ex/Classical.thy Mon Jul 18 17:40:13 2011 +0100 @@ -216,7 +216,7 @@ apply(blast) done -termination +termination (eqvt) by lexicographic_order nominal_primrec @@ -379,7 +379,7 @@ apply(blast) done -termination +termination (eqvt) by lexicographic_order lemma crename_name_eqvt[eqvt]: diff -r 84afb941df53 -r d1038e67923a Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Mon Jul 18 17:40:13 2011 +0100 @@ -43,7 +43,17 @@ apply(all_trivials) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order + +ML {* +Item_Net.content; +Nominal_Function_Common.get_function +*} + +ML {* +Item_Net.content (Nominal_Function_Common.get_function @{context}) +*} + lemma [eqvt]: shows "(p \ (is_app t)) = is_app (p \ t)" @@ -65,7 +75,7 @@ apply(simp_all) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order lemma [eqvt]: shows "(p \ (rator t)) = rator (p \ t)" @@ -87,7 +97,7 @@ apply(simp_all) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order lemma [eqvt]: shows "(p \ (rand t)) = rand (p \ t)" @@ -118,7 +128,7 @@ apply(rule refl) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order nominal_datatype path = Left | Right | In @@ -155,7 +165,7 @@ apply(rule refl) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order lemma var_pos1: assumes "atom y \ supp t" @@ -195,7 +205,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order section {* free name function *} @@ -221,7 +231,7 @@ apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) done -termination by lexicographic_order +termination (eqvt) by lexicographic_order text {* a small test lemma *} lemma shows "supp t = set (frees_lst t)" @@ -249,7 +259,7 @@ apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) done -termination +termination (eqvt) by lexicographic_order lemma "frees_set t = supp t" @@ -272,7 +282,7 @@ apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) done -termination +termination (eqvt) by lexicographic_order thm height.simps @@ -300,7 +310,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination +termination (eqvt) by lexicographic_order lemma subst_eqvt[eqvt]: @@ -486,7 +496,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination +termination (eqvt) by lexicographic_order @@ -513,7 +523,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination +termination (eqvt) by lexicographic_order @@ -543,7 +553,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination +termination (eqvt) by lexicographic_order section {* De Bruijn Terms *} @@ -594,7 +604,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ done -termination +termination (eqvt) by lexicographic_order lemma transdb_eqvt[eqvt]: @@ -665,7 +675,7 @@ (* a small test -termination sorry +termination (eqvt) sorry lemma assumes "x \ y" @@ -719,7 +729,7 @@ apply (simp add: eqvt_def permute_fun_app_eq) done -termination +termination (eqvt) by lexicographic_order diff -r 84afb941df53 -r d1038e67923a Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/Ex/LetRec.thy Mon Jul 18 17:40:13 2011 +0100 @@ -59,7 +59,9 @@ apply (simp add: permute_fun_def) done -termination by lexicographic_order +thm height_trm_def height_bp_def + +termination (eqvt) by lexicographic_order end diff -r 84afb941df53 -r d1038e67923a Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/Ex/TypeSchemes.thy Mon Jul 18 17:40:13 2011 +0100 @@ -322,7 +322,7 @@ apply(simp_all add: ty2.distinct) done -termination +termination (eqvt) by lexicographic_order lemma subst_eqvt[eqvt]: diff -r 84afb941df53 -r d1038e67923a Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/Nominal2.thy Mon Jul 18 17:40:13 2011 +0100 @@ -10,6 +10,7 @@ ("nominal_function_core.ML") ("nominal_mutual.ML") ("nominal_function.ML") + ("nominal_termination.ML") ("nominal_dt_data.ML") begin @@ -44,6 +45,7 @@ use "nominal_function_core.ML" use "nominal_mutual.ML" use "nominal_function.ML" +use "nominal_termination.ML" ML {* val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) diff -r 84afb941df53 -r d1038e67923a Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/nominal_function.ML Mon Jul 18 17:40:13 2011 +0100 @@ -9,15 +9,15 @@ signature NOMINAL_FUNCTION = sig - include FUNCTION_DATA + include NOMINAL_FUNCTION_DATA val add_nominal_function: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> - (Proof.context -> tactic) -> local_theory -> info * local_theory + (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory val add_nominal_function_cmd: (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> - (Proof.context -> tactic) -> local_theory -> info * local_theory + (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory val nominal_function: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> @@ -30,7 +30,7 @@ val setup : theory -> theory val get_congs : Proof.context -> thm list - val get_info : Proof.context -> term -> info + val get_info : Proof.context -> term -> nominal_info end @@ -152,9 +152,12 @@ fun afterqed [[proof]] lthy = let - val FunctionResult {fs, R, psimps, simple_pinducts, - termination, domintros, cases, ...} = + val NominalFunctionResult {fs, R, psimps, simple_pinducts, + termination, domintros, cases, eqvts, ...} = cont (Thm.close_derivation proof) + + val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps)) + val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts)) val fnames = map (fst o fst) fixes fun qualify n = Binding.name n @@ -179,7 +182,9 @@ 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, defname=defname, is_partial=true, eqvts=eqvts} + + val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps')) val _ = if not is_external then () diff -r 84afb941df53 -r d1038e67923a Nominal/nominal_function_common.ML --- a/Nominal/nominal_function_common.ML Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/nominal_function_common.ML Mon Jul 18 17:40:13 2011 +0100 @@ -7,11 +7,110 @@ Redefinition of config datatype *) +signature NOMINAL_FUNCTION_DATA = +sig + +type nominal_info = + {is_partial : bool, + defname : string, + (* contains no logical entities: invariant under morphisms: *) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, + fs : term list, + R : term, + psimps: thm list, + pinducts: thm list, + simps : thm list option, + inducts : thm list option, + termination: thm, + eqvts: thm list} + +end structure Nominal_Function_Common = struct +type nominal_info = + {is_partial : bool, + defname : string, + (* contains no logical entities: invariant under morphisms: *) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, + fs : term list, + R : term, + psimps: thm list, + pinducts: thm list, + simps : thm list option, + inducts : thm list option, + termination: thm, + eqvts: thm list} + +fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, + simps, inducts, termination, defname, is_partial, eqvts} : nominal_info) phi = + let + val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi + 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, + pinducts = fact pinducts, simps = Option.map fact simps, + inducts = Option.map fact inducts, termination = thm termination, + defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts } + end + +structure NominalFunctionData = Generic_Data +( + type T = (term * nominal_info) Item_Net.T; + val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); + val extend = I; + fun merge tabs : T = Item_Net.merge tabs; +) + +val get_function = NominalFunctionData.get o Context.Proof; + + +fun lift_morphism thy f = + let + val term = Drule.term_rule thy f + in + Morphism.thm_morphism f $> Morphism.term_morphism term + $> Morphism.typ_morphism (Logic.type_map term) + end + +fun import_function_data t ctxt = + let + val thy = Proof_Context.theory_of ctxt + val ct = cterm_of thy t + val inst_morph = lift_morphism thy o Thm.instantiate + + fun match (trm, data) = + SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) + handle Pattern.MATCH => NONE + in + get_first match (Item_Net.retrieve (get_function ctxt) t) + end + +fun import_last_function ctxt = + case Item_Net.content (get_function ctxt) of + [] => NONE + | (t, data) :: _ => + let + val ([t'], ctxt') = Variable.import_terms true [t] ctxt + in + import_function_data t' ctxt' + end + +val all_function_data = Item_Net.content o get_function + +fun add_function_data (data : nominal_info as {fs, termination, ...}) = + NominalFunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) + #> Function_Common.store_termination_rule termination + + + (* Configuration management *) datatype nominal_function_opt @@ -48,4 +147,15 @@ NominalFunctionConfig { sequential=false, default=NONE, domintros=false, partials=true, inv=NONE} +datatype nominal_function_result = NominalFunctionResult of + {fs: term list, + G: term, + R: term, + psimps : thm list, + simple_pinducts : thm list, + cases : thm, + termination : thm, + domintros : thm list option, + eqvts : thm list} + end diff -r 84afb941df53 -r d1038e67923a Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/nominal_function_core.ML Mon Jul 18 17:40:13 2011 +0100 @@ -19,7 +19,7 @@ -> local_theory -> (term (* f *) * thm (* goalstate *) - * (thm -> Function_Common.function_result) (* continuation *) + * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *) ) * local_theory end @@ -1062,6 +1062,8 @@ val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) + val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) + val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function @@ -1077,9 +1079,9 @@ else NONE in - FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, + NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm, psimps=psimps, simple_pinducts=[simple_pinduct], - termination=total_intro, domintros=dom_intros} + termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]} end in ((f, goalstate, mk_partial_rules), lthy) diff -r 84afb941df53 -r d1038e67923a Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Jul 18 10:50:21 2011 +0100 +++ b/Nominal/nominal_mutual.ML Mon Jul 18 17:40:13 2011 +0100 @@ -17,7 +17,7 @@ -> term list -> local_theory -> ((thm (* goalstate *) - * (thm -> Function_Common.function_result) (* proof continuation *) + * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *) ) * local_theory) end @@ -255,8 +255,15 @@ fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = let val result = inner_cont proof - val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], - termination, domintros, ...} = result + val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], + termination, domintros, eqvts,...} = result + + (* + val _ = tracing ("premutual induct:\n" ^ @{make_string} simple_pinduct) + val _ = tracing ("premutual termination:\n" ^ @{make_string} termination) + val _ = tracing ("premutual psimps:\n" ^ cat_lines (map @{make_string} psimps)) + val _ = tracing ("premutual eqvts:\n" ^ cat_lines (map @{make_string} eqvts)) + *) val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => @@ -275,11 +282,17 @@ val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m val mtermination = full_simplify rew_ss termination val mdomintros = Option.map (map (full_simplify rew_ss)) domintros + + (* + val _ = tracing ("postmutual psimps:\n" ^ cat_lines (map @{make_string} mpsimps)) + val _ = tracing ("postmutual induct:\n" ^ cat_lines (map @{make_string} minducts)) + val _ = tracing ("postmutual termination:\n" ^ @{make_string} mtermination) + *) in - FunctionResult { fs=fs, G=G, R=R, + NominalFunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, cases=cases, termination=mtermination, - domintros=mdomintros} + domintros=mdomintros, eqvts=eqvts } end (* nominal *)