nominal2: Nominal/Nominal2_FSet.thy@693562f03eee (annotated)

1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Nominal2_FSet
2467 67b3933c3190 got rid of Nominal_Atoms (folded into Nominal2_Base) Christian Urban <urbanc@in.tum.de> parents: 2466 diff changeset	2	imports "../Nominal-General/Nominal2_Base"
2302 c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2178 diff changeset	3	"../Nominal-General/Nominal2_Eqvt"
1806 90095f23fc60 tuned Christian Urban <urbanc@in.tum.de> parents: 1782 diff changeset	4	FSet
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	begin
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	lemma permute_rsp_fset[quot_respect]:
2447 76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	8	shows "(op = ===> list_eq ===> list_eq) permute permute"
76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	9	apply(simp)
76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	10	apply(clarify)
2468 7b1470b55936 moved a proof to Abs Christian Urban <urbanc@in.tum.de> parents: 2467 diff changeset	11	apply(rule_tac p="-x" in permute_boolE)
7b1470b55936 moved a proof to Abs Christian Urban <urbanc@in.tum.de> parents: 2467 diff changeset	12	apply(perm_simp add: permute_minus_cancel)
2447 76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	13	apply(simp)
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	done
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	16	instantiation fset :: (pt) pt
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	begin
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	quotient_definition
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	"permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	is
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	"permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23
1815 4135198bbb8a moved equivariance of map into Nominal2_Eqvt file Christian Urban <urbanc@in.tum.de> parents: 1806 diff changeset	24	instance
4135198bbb8a moved equivariance of map into Nominal2_Eqvt file Christian Urban <urbanc@in.tum.de> parents: 1806 diff changeset	25	proof
1782 27fec5fcfe67 simplify instance proof Brian Huffman <brianh@cs.pdx.edu> parents: 1774 diff changeset	26	fix x :: "'a fset" and p q :: "perm"
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	27	show "0 \<bullet> x = x" by (descending) (simp)
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	28	show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
1782 27fec5fcfe67 simplify instance proof Brian Huffman <brianh@cs.pdx.edu> parents: 1774 diff changeset	29	qed
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	end
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
2466 47c840599a6b cleaned a bit various thy-files in Nominal-General Christian Urban <urbanc@in.tum.de> parents: 2447 diff changeset	33	lemma permute_fset[simp, eqvt]:
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	34	fixes S::"('a::pt) fset"
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	35	shows "(p \<bullet> {\|\|}) = ({\|\|} ::('a::pt) fset)"
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	36	and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	by (lifting permute_list.simps)
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38
1815 4135198bbb8a moved equivariance of map into Nominal2_Eqvt file Christian Urban <urbanc@in.tum.de> parents: 1806 diff changeset	39	lemma fmap_eqvt[eqvt]:
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	40	shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	by (lifting map_eqvt)
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	43	lemma fset_eqvt[eqvt]:
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	44	shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	by (lifting set_eqvt)
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	47	lemma supp_fset:
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	48	shows "supp (fset S) = supp S"
2340 b1549d391ea7 removed an "eqvt"-warning Christian Urban <urbanc@in.tum.de> parents: 2302 diff changeset	49	unfolding supp_def
b1549d391ea7 removed an "eqvt"-warning Christian Urban <urbanc@in.tum.de> parents: 2302 diff changeset	50	by (perm_simp) (simp add: fset_cong)
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51
2447 76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	52	lemma supp_fempty:
76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	53	shows "supp {\|\|} = {}"
76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	54	unfolding supp_def
76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	55	by simp
76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	56
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	57	lemma supp_finsert:
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	58	fixes x::"'a::fs"
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	59	and S::"'a fset"
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	60	shows "supp (finsert x S) = supp x \<union> supp S"
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	61	apply(subst supp_fset[symmetric])
693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	62	apply(simp add: supp_fset)
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	63	apply(simp add: supp_of_fin_insert)
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	64	apply(simp add: supp_fset)
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	65	done
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	66
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	67
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	68	instance fset :: (fs) fs
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	69	apply (default)
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	70	apply (induct_tac x rule: fset_induct)
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	71	apply (simp add: supp_fempty)
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	72	apply (simp add: supp_finsert)
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	73	apply (simp add: finite_supp)
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	74	done
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	75
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76	lemma atom_fmap_cong:
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	77	shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y"
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	78	apply(rule inj_fmap_eq_iff)
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	79	apply(simp add: inj_on_def)
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	80	done
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81
984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82	lemma supp_fmap_atom:
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	83	shows "supp (fmap atom S) = supp S"
1818 37480540c1af made everything to compile Christian Urban <urbanc@in.tum.de> parents: 1815 diff changeset	84	unfolding supp_def
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	85	apply(perm_simp)
b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	86	apply(simp add: atom_fmap_cong)
1568 2311a9fc4624 Strong induction for Type Schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1542 diff changeset	87	done
2311a9fc4624 Strong induction for Type Schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1542 diff changeset	88
2311a9fc4624 Strong induction for Type Schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1542 diff changeset	89	lemma supp_at_fset:
1973 fc5ce7f22b74 use the more general type-class at_base Christian Urban <urbanc@in.tum.de> parents: 1933 diff changeset	90	fixes S::"('a::at_base) fset"
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	91	shows "supp S = fset (fmap atom S)"
1973 fc5ce7f22b74 use the more general type-class at_base Christian Urban <urbanc@in.tum.de> parents: 1933 diff changeset	92	apply (induct S)
1568 2311a9fc4624 Strong induction for Type Schemes. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1542 diff changeset	93	apply (simp add: supp_fempty)
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	94	apply (simp add: supp_finsert)
1542 63e327e95abd Showed the instance: fset::(at) fs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1534 diff changeset	95	apply (simp add: supp_at_base)
63e327e95abd Showed the instance: fset::(at) fs Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1534 diff changeset	96	done
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	97
2178 e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	98	lemma fresh_star_atom:
2447 76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	99	fixes a::"'a::at_base"
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2471 diff changeset	100	shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
2447 76be909eaf04 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2340 diff changeset	101	apply (induct S)
2178 e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	102	apply (simp add: fresh_set_empty)
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	103	apply simp
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	104	apply (unfold fresh_def)
2466 47c840599a6b cleaned a bit various thy-files in Nominal-General Christian Urban <urbanc@in.tum.de> parents: 2447 diff changeset	105	apply (simp add: supp_of_fin_insert)
2178 e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	106	apply (rule conjI)
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	107	apply (unfold fresh_star_def)
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	108	apply simp
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	109	apply (unfold fresh_def)
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	110	apply (simp add: supp_at_base supp_atom)
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	111	apply clarify
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	112	apply auto
e559513143e9 reversing the direction of fresh_star Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2004 diff changeset	113	done
2004 b96e8cf86891 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements) Christian Urban <urbanc@in.tum.de> parents: 1973 diff changeset	114
1534 984ea1299cd7 The nominal infrastructure for fset. 'fs' missing, but not needed so far. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	115	end

author	Christian Urban <urbanc@in.tum.de>
	Thu, 14 Oct 2010 04:14:22 +0100 (2010-10-14)
changeset 2524	693562f03eee
parent 2471	894599a50af3
child 2535	05f98e2ee48b
permissions	-rw-r--r--