nominal2: Nominal/Eqvt.thy@a33e96e62a2b (annotated)

1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	1	(* Title: Nominal2_Eqvt
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1803 diff changeset	2	Author: Brian Huffman,
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1803 diff changeset	3	Author: Christian Urban
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	4
2733 5f6fefdbf055 split the library into a basics file; merged Nominal_Eqvt into Nominal_Base Christian Urban <urbanc@in.tum.de> parents: 2725 diff changeset	5	Test cases for perm_simp
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	6	*)
2734 eee5deb35aa8 included old test cases for perm_simp into ROOT.ML file Christian Urban <urbanc@in.tum.de> parents: 2733 diff changeset	7	theory Eqvt
1933 9eab1dfc14d2 moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms Christian Urban <urbanc@in.tum.de> parents: 1872 diff changeset	8	imports Nominal2_Base
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	9	begin
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	10
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	11
2009 4f7d7cbd4bc8 removed duplicate eqvt attribute Christian Urban <urbanc@in.tum.de> parents: 2002 diff changeset	12	declare [[trace_eqvt = false]]
4f7d7cbd4bc8 removed duplicate eqvt attribute Christian Urban <urbanc@in.tum.de> parents: 2002 diff changeset	13	(* declare [[trace_eqvt = true]] *)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	14
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	15	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	16	fixes B::"'a::pt"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	17	shows "p \<bullet> (B = C)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	18	apply(perm_simp)
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	19	oops
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	20
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	21	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	22	fixes B::"bool"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	23	shows "p \<bullet> (B = C)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	24	apply(perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	25	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	26
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	27	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	28	fixes B::"bool"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	29	shows "p \<bullet> (A \<longrightarrow> B = C)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	30	apply (perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	31	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	32
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	33	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	34	shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	35	apply(perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	36	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	37
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	38	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	39	shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	40	apply (perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	41	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	42
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	43	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	44	shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	45	apply (perm_simp)
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	46	oops
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	47
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	48	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	49	shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	50	apply (perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	51	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	52
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	53	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	54	fixes p q::"perm"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	55	and x::"'a::pt"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	56	shows "p \<bullet> (q \<bullet> x) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	57	apply(perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	58	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	59
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	60	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	61	fixes p q r::"perm"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	62	and x::"'a::pt"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	63	shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	64	apply(perm_simp)
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	65	oops
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	66
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	67	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	68	fixes p r::"perm"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	69	shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	70	apply (perm_simp)
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	71	oops
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	72
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	73	lemma
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	74	fixes C D::"bool"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	75	shows "B (p \<bullet> (C = D))"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	76	apply(perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	77	oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	78
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	79	declare [[trace_eqvt = false]]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	80
2200 31f1ec832d39 fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set Christian Urban <urbanc@in.tum.de> parents: 2129 diff changeset	81	text {* there is no raw eqvt-rule for The *}
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	82	lemma "p \<bullet> (THE x. P x) = foo"
1867 f4477d3fe520 preliminary parser for perm_simp metod Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	83	apply(perm_strict_simp exclude: The)
f4477d3fe520 preliminary parser for perm_simp metod Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	84	apply(perm_simp exclude: The)
1062 dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	85	oops
dfea9e739231 rollback of the test Christian Urban <urbanc@in.tum.de> parents: 1061 diff changeset	86
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2009 diff changeset	87	lemma
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2009 diff changeset	88	fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	89	shows "p \<bullet> (P The) = foo"
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2009 diff changeset	90	apply(perm_simp exclude: The)
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2009 diff changeset	91	oops
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2009 diff changeset	92
2080 0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	93	lemma
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	94	fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	95	shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	96	apply(perm_simp)
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	97	oops
0532006ec7ec added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	98
1953 186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	99	thm eqvts
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	100	thm eqvts_raw
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	101
1995 652f310f0dba reorganised eqvt-file (now uses perm_simp already) Christian Urban <urbanc@in.tum.de> parents: 1971 diff changeset	102	ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
1953 186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	103
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	104
1315 43d6e3730353 Add image_eqvt and atom_eqvt to eqvt bases. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1258 diff changeset	105	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 13 Sep 2011 09:30:34 +0200 (2011-09-13)
changeset 3011	a33e96e62a2b
parent 2734	eee5deb35aa8
permissions	-rw-r--r--