# HG changeset patch # User urbanc # Date 1189720718 -7200 # Node ID a6d0428dea8e742362c6600b480148f893482a2e # Parent 621b60b1df00d33332352964bb3c7ed6abe0f11f some cleaning up to do with contexts diff -r 621b60b1df00 -r a6d0428dea8e src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Thu Sep 13 18:11:59 2007 +0200 +++ b/src/HOL/Nominal/Nominal.thy Thu Sep 13 23:58:38 2007 +0200 @@ -1224,6 +1224,18 @@ apply(rule pt1[OF pt]) done +lemma pt_swap_bij'': + fixes a :: "'x" + and x :: "'a" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "[(a,a)]\x = x" +apply(rule trans) +apply(rule pt3[OF pt]) +apply(rule at_ds1[OF at]) +apply(rule pt1[OF pt]) +done + lemma pt_set_bij1: fixes pi :: "'x prm" and x :: "'a" @@ -1754,6 +1766,7 @@ section {* equivaraince for some connectives *} +(* lemma pt_all_eqvt: fixes pi :: "'x prm" and x :: "'a" @@ -1764,6 +1777,18 @@ apply(drule_tac x="pi\x" in spec) apply(simp add: pt_rev_pi[OF pt, OF at]) done +*) + +lemma pt_all_eqvt: + fixes pi :: "'x prm" + and x :: "'a" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "pi\(\(x::'a). P x) = (\(x::'a). P ((rev pi)\x))" +apply(auto simp add: perm_bool) +apply(drule_tac x="pi\x" in spec) +apply(simp add: pt_rev_pi[OF pt, OF at]) +done lemma pt_ex_eqvt: fixes pi :: "'x prm" diff -r 621b60b1df00 -r a6d0428dea8e src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Sep 13 18:11:59 2007 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Sep 13 23:58:38 2007 +0200 @@ -147,7 +147,7 @@ InductivePackage.the_inductive ctxt (Sign.intern_const thy s); val raw_induct = atomize_induct raw_induct; val monos = InductivePackage.get_monos ctxt; - val eqvt_thms = NominalThmDecls.get_eqvt_thms thy; + val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of [] => () | xs => error ("Missing equivariance theorem for predicate(s): " ^ @@ -461,7 +461,7 @@ end; val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp"); val eqvt_ss = HOL_basic_ss addsimps - (NominalThmDecls.get_eqvt_thms thy @ perm_pi_simp) addsimprocs + (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names]; val t = Logic.unvarify (concl_of raw_induct); val pi = Name.variant (add_term_names (t, [])) "pi"; diff -r 621b60b1df00 -r a6d0428dea8e src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Thu Sep 13 18:11:59 2007 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Sep 13 23:58:38 2007 +0200 @@ -133,7 +133,7 @@ end (* function for simplyfying permutations *) -fun perm_simp_gen dyn_thms f ss i = +fun perm_simp_gen dyn_thms eqvt_thms ss i = ("general simplification of permutations", fn st => let @@ -143,7 +143,7 @@ val perm_sp_app = Simplifier.simproc (theory_of_thm st) "perm_simproc_app" ["Nominal.perm pi x"] (perm_simproc_app st); - val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@(f st)) + val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@eqvt_thms) delcongs weak_congs addcongs strong_congs addsimprocs [perm_sp_fun, perm_sp_app] @@ -152,23 +152,21 @@ end); (* general simplification of permutations and permutation that arose from eqvt-problems *) -val perm_simp = +fun perm_simp ss = let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"] in - perm_simp_gen simps (fn st => []) + perm_simp_gen simps [] ss end; -val eqvt_simp = +fun eqvt_simp ss = let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"] - fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st); + val eqvts_thms = NominalThmDecls.get_eqvt_thms (Simplifier.the_context ss); in - perm_simp_gen simps eqvts_thms + perm_simp_gen simps eqvts_thms ss end; -(* FIXME removes the name lookup for these theorems use an ml value instead *) (* main simplification tactics for permutations *) -(* FIXME: perm_simp_tac should simplify more permutations *) fun perm_simp_tac tactical ss i = DETERM (tactical (perm_simp ss i)); fun eqvt_simp_tac tactical ss i = DETERM (tactical (eqvt_simp ss i)); @@ -384,6 +382,7 @@ val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac); val supports_meth = local_simp_meth_setup (supports_tac NO_DEBUG_tac); val supports_meth_debug = local_simp_meth_setup (supports_tac DEBUG_tac); + val finite_guess_meth = basic_simp_meth_setup false (finite_guess_tac NO_DEBUG_tac); val finite_guess_meth_debug = basic_simp_meth_setup true (finite_guess_tac DEBUG_tac); val fresh_guess_meth = basic_simp_meth_setup false (fresh_guess_tac NO_DEBUG_tac); diff -r 621b60b1df00 -r a6d0428dea8e src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Sep 13 18:11:59 2007 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Sep 13 23:58:38 2007 +0200 @@ -5,7 +5,7 @@ declaration "eqvts" "bijs" and "freshs". By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored - in a data-slot in the theory context. Possible modifiers + in a data-slot in the context. Possible modifiers are [attribute add] and [attribute del] for adding and deleting, respectively the lemma from the data-slot. *) @@ -18,9 +18,9 @@ val eqvt_force_add: attribute val eqvt_force_del: attribute val setup: theory -> theory - val get_eqvt_thms: theory -> thm list - val get_fresh_thms: theory -> thm list - val get_bij_thms: theory -> thm list + val get_eqvt_thms: Proof.context -> thm list + val get_fresh_thms: Proof.context -> thm list + val get_bij_thms: Proof.context -> thm list val NOMINAL_EQVT_DEBUG : bool ref @@ -62,18 +62,13 @@ pretty_thms "Bijection lemmas:" (#bijs data)]) end; - -val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts; -val get_fresh_thms = Context.Theory #> Data.get #> #freshs; -val get_bij_thms = Context.Theory #> Data.get #> #bijs; +val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts; +val get_fresh_thms = Context.Proof #> Data.get #> #freshs; +val get_bij_thms = Context.Proof #> Data.get #> #bijs; (* FIXME: should be a function in a library *) fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); -val perm_boolE = thm "perm_boolE"; -val perm_boolI = thm "perm_boolI"; -val perm_fun_def = thm "perm_fun_def"; - val NOMINAL_EQVT_DEBUG = ref false; fun tactic (msg,tac) = @@ -90,14 +85,12 @@ val perm_pi_simp = dynamic_thms ctx "perm_pi_simp" in EVERY [tactic ("iffI applied",rtac iffI 1), - tactic ("remove pi with perm_boolE", - (dtac perm_boolE 1)), - tactic ("solve with orig_thm", - (etac orig_thm 1)), + tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)), + tactic ("solve with orig_thm", (etac orig_thm 1)), tactic ("applies orig_thm instantiated with rev pi", dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), tactic ("getting rid of the pi on the right", - (rtac perm_boolI 1)), + (rtac @{thm perm_boolI} 1)), tactic ("getting rid of all remaining perms", full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)] end;