--- 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)]\<bullet>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\<bullet>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\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). P ((rev pi)\<bullet>x))"
+apply(auto simp add: perm_bool)
+apply(drule_tac x="pi\<bullet>x" in spec)
+apply(simp add: pt_rev_pi[OF pt, OF at])
+done
lemma pt_ex_eqvt:
fixes pi :: "'x prm"
--- 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";
--- 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);
--- 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;