# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1311036036 -3600 # Node ID b95a2065aa10f0b3b9222a3fd90044b4ced0d9af # Parent d1038e67923a95e2fa23f4de08ceddd32a567123 generated the partial eqvt-theorem for functions diff -r d1038e67923a -r b95a2065aa10 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Jul 18 17:40:13 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Tue Jul 19 01:40:36 2011 +0100 @@ -46,13 +46,10 @@ termination (eqvt) by lexicographic_order ML {* -Item_Net.content; -Nominal_Function_Common.get_function +Item_Net.content (Nominal_Function_Common.get_function @{context}) *} -ML {* -Item_Net.content (Nominal_Function_Common.get_function @{context}) -*} +thm is_app_def lemma [eqvt]: @@ -165,6 +162,11 @@ apply(rule refl) done +thm inl_eqvt +thm var_pos_def + +thm fun_eq_iff + termination (eqvt) by lexicographic_order lemma var_pos1: diff -r d1038e67923a -r b95a2065aa10 Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Mon Jul 18 17:40:13 2011 +0100 +++ b/Nominal/Ex/LetRec.thy Tue Jul 19 01:40:36 2011 +0100 @@ -59,6 +59,16 @@ apply (simp add: permute_fun_def) done +ML {* +let + val [t1, t2] = Item_Net.content (Nominal_Function_Common.get_function @{context}) +in + (#eqvts (snd t1), + #eqvts (snd t2)) +end +*} + + thm height_trm_def height_bp_def termination (eqvt) by lexicographic_order diff -r d1038e67923a -r b95a2065aa10 Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Mon Jul 18 17:40:13 2011 +0100 +++ b/Nominal/nominal_function.ML Tue Jul 19 01:40:36 2011 +0100 @@ -156,9 +156,6 @@ 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 |> Binding.qualify true defname @@ -184,8 +181,6 @@ pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', 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 () else Specification.print_consts lthy (K false) (map fst fixes) diff -r d1038e67923a -r b95a2065aa10 Nominal/nominal_function_common.ML --- a/Nominal/nominal_function_common.ML Mon Jul 18 17:40:13 2011 +0100 +++ b/Nominal/nominal_function_common.ML Tue Jul 19 01:40:36 2011 +0100 @@ -58,7 +58,7 @@ 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 } + defname = name defname, is_partial=is_partial, eqvts = fact eqvts } end structure NominalFunctionData = Generic_Data diff -r d1038e67923a -r b95a2065aa10 Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Mon Jul 18 17:40:13 2011 +0100 +++ b/Nominal/nominal_function_core.ML Tue Jul 19 01:40:36 2011 +0100 @@ -1053,16 +1053,15 @@ let val newthy = theory_of_thm provedgoal (*FIXME*) - val (graph_is_function, complete_thm) = + val ((graph_is_function, complete_thm), graph_is_eqvt) = provedgoal - |> fst o Conjunction.elim - |> fst o Conjunction.elim |> Conjunction.elim - |> apfst (Thm.forall_elim_vars 0) + |>> fst o Conjunction.elim + |>> Conjunction.elim + |>> apfst (Thm.forall_elim_vars 0) 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 f_eqvt = graph_is_function RS (graph_is_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 diff -r d1038e67923a -r b95a2065aa10 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Jul 18 17:40:13 2011 +0100 +++ b/Nominal/nominal_mutual.ML Tue Jul 19 01:40:36 2011 +0100 @@ -38,7 +38,6 @@ fvar : string * typ, cargTs: typ list, f_def: term, - f: term option, f_defthm : thm option} @@ -184,14 +183,13 @@ import (export : thm -> thm) sum_psimp_eq = let val (MutualPart {f=SOME f, ...}) = get_part fname parts - + val psimp = import sum_psimp_eq val (simp, restore_cond) = case cprems_of psimp of [] => (psimp, I) | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) | _ => raise General.Fail "Too many conditions" - in Goal.prove ctxt [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) @@ -202,6 +200,31 @@ |> export end +fun mk_meqvts ctxt eqvt_thm f_defs = + let + val ctrm1 = eqvt_thm + |> cprop_of + |> snd o Thm.dest_implies + |> Thm.dest_arg + |> Thm.dest_arg1 + |> Thm.dest_arg + + fun resolve f_def = + let + val ctrm2 = f_def + |> cprop_of + |> Thm.dest_equals_lhs + in + eqvt_thm + |> Thm.instantiate (Thm.match (ctrm1, ctrm2)) + |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps})) + |> Local_Defs.unfold ctxt [f_def] + end + in + map resolve f_defs + end + + fun mk_applied_form ctxt caTs thm = let val thy = ProofContext.theory_of ctxt @@ -256,14 +279,7 @@ let val result = inner_cont proof 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)) - *) + termination, domintros, eqvts=[eqvt],...} = result val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => @@ -282,17 +298,12 @@ 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 + val meqvts = mk_meqvts lthy eqvt all_f_defs + in NominalFunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, cases=cases, termination=mtermination, - domintros=mdomintros, eqvts=eqvts } + domintros=mdomintros, eqvts=meqvts } end (* nominal *)