7 ML {* val _ = cheat_fv_rsp := false *} |
7 ML {* val _ = cheat_fv_rsp := false *} |
8 ML {* val _ = cheat_const_rsp := false *} |
8 ML {* val _ = cheat_const_rsp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
11 ML {* val _ = cheat_alpha_eqvt := false *} |
11 ML {* val _ = cheat_alpha_eqvt := false *} |
12 |
|
13 lemma permute_rsp_fset[quot_respect]: |
|
14 "(op = ===> op \<approx> ===> op \<approx>) permute permute" |
|
15 apply (simp add: eqvts[symmetric]) |
|
16 apply clarify |
|
17 apply (subst permute_minus_cancel(1)[symmetric, of "xb"]) |
|
18 apply (subst mem_eqvt[symmetric]) |
|
19 apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |
|
20 apply (subst mem_eqvt[symmetric]) |
|
21 apply (erule_tac x="- x \<bullet> xb" in allE) |
|
22 apply simp |
|
23 done |
|
24 |
|
25 instantiation FSet.fset :: (pt) pt |
|
26 begin |
|
27 |
|
28 term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
29 |
|
30 quotient_definition |
|
31 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
32 is |
|
33 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
34 |
|
35 lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x" |
|
36 by (rule permute_zero) |
|
37 |
|
38 lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x" |
|
39 by (lifting permute_list_zero) |
|
40 |
|
41 lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x" |
|
42 by (rule permute_plus) |
|
43 |
|
44 lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x" |
|
45 by (lifting permute_list_plus) |
|
46 |
|
47 instance |
|
48 apply default |
|
49 apply (rule permute_fset_zero) |
|
50 apply (rule permute_fset_plus) |
|
51 done |
|
52 |
|
53 end |
|
54 |
|
55 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
|
56 by (lifting set_eqvt) |
|
57 |
|
58 thm list_induct2'[no_vars] |
|
59 |
|
60 lemma fset_induct2: |
|
61 "Pa {||} {||} \<Longrightarrow> |
|
62 (\<forall>x xs. Pa (finsert x xs) {||}) \<Longrightarrow> |
|
63 (\<forall>y ys. Pa {||} (finsert y ys)) \<Longrightarrow> |
|
64 (\<forall>x xs y ys. Pa xs ys \<longrightarrow> Pa (finsert x xs) (finsert y ys)) \<Longrightarrow> |
|
65 Pa xsa ysa" |
|
66 by (lifting list_induct2') |
|
67 |
|
68 lemma set_cong: "(set x = set y) = (x \<approx> y)" |
|
69 apply rule |
|
70 apply simp_all |
|
71 apply (induct x y rule: list_induct2') |
|
72 apply simp_all |
|
73 apply auto |
|
74 done |
|
75 |
|
76 lemma fset_cong: |
|
77 "(fset_to_set x = fset_to_set y) = (x = y)" |
|
78 by (lifting set_cong) |
|
79 |
|
80 lemma supp_fset_to_set: |
|
81 "supp (fset_to_set x) = supp x" |
|
82 apply (simp add: supp_def) |
|
83 apply (simp add: eqvts) |
|
84 apply (simp add: fset_cong) |
|
85 done |
|
86 |
|
87 lemma inj_map_eq_iff: |
|
88 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
|
89 by (simp add: Set.expand_set_eq[symmetric] inj_image_eq_iff) |
|
90 |
|
91 lemma inj_fmap_eq_iff: |
|
92 "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)" |
|
93 by (lifting inj_map_eq_iff) |
|
94 |
|
95 lemma atom_fmap_cong: |
|
96 shows "(fmap atom x = fmap atom y) = (x = y)" |
|
97 apply(rule inj_fmap_eq_iff) |
|
98 apply(simp add: inj_on_def) |
|
99 done |
|
100 |
|
101 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)" |
|
102 apply (induct l) |
|
103 apply (simp_all) |
|
104 apply (simp only: eqvt_apply) |
|
105 done |
|
106 |
|
107 lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)" |
|
108 by (lifting map_eqvt) |
|
109 |
|
110 lemma supp_fmap_atom: |
|
111 "supp (fmap atom x) = supp x" |
|
112 apply (simp add: supp_def) |
|
113 apply (simp add: eqvts eqvts_raw atom_fmap_cong) |
|
114 done |
|
115 |
12 |
116 nominal_datatype t = |
13 nominal_datatype t = |
117 Var "name" |
14 Var "name" |
118 | Fun "t" "t" |
15 | Fun "t" "t" |
119 and tyS = |
16 and tyS = |
123 thm t_tyS.eq_iff |
20 thm t_tyS.eq_iff |
124 thm t_tyS.bn |
21 thm t_tyS.bn |
125 thm t_tyS.perm |
22 thm t_tyS.perm |
126 thm t_tyS.inducts |
23 thm t_tyS.inducts |
127 thm t_tyS.distinct |
24 thm t_tyS.distinct |
|
25 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
128 |
26 |
129 lemma finite_fv_t_tyS: |
27 lemma finite_fv_t_tyS: |
130 shows "finite (fv_t t)" "finite (fv_tyS ts)" |
28 shows "finite (fv_t t)" "finite (fv_tyS ts)" |
131 by (induct rule: t_tyS.inducts) (simp_all) |
29 by (induct rule: t_tyS.inducts) (simp_all) |
132 |
30 |
133 lemma infinite_Un: |
|
134 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
135 by simp |
|
136 |
|
137 lemma supp_fv_t_tyS: |
31 lemma supp_fv_t_tyS: |
138 shows "fv_t t = supp t" "fv_tyS ts = supp ts" |
32 shows "fv_t t = supp t" "fv_tyS ts = supp ts" |
139 apply(induct rule: t_tyS.inducts) |
33 apply(induct rule: t_tyS.inducts) |
140 apply(simp_all only: t_tyS.fv) |
34 apply(simp_all only: t_tyS.fv) |
141 prefer 3 |
35 prefer 3 |
142 apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) |
36 apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) |
143 prefer 2 |
37 prefer 2 |
144 apply(subst finite_supp_Abs) |
38 apply(subst finite_supp_Abs) |
145 apply(drule sym) |
39 apply(drule sym) |
146 apply(simp add: finite_fv_t_tyS(1)) |
40 apply(simp add: finite_fv_t_tyS(1)) |
147 apply(simp) |
41 apply(simp) |
148 apply(simp_all (no_asm) only: supp_def) |
42 apply(simp_all (no_asm) only: supp_def) |
149 apply(simp_all only: t_tyS.perm) |
43 apply(simp_all only: t_tyS.perm) |
150 apply(simp_all only: permute_ABS) |
44 apply(simp_all only: permute_ABS) |
151 apply(simp_all only: t_tyS.eq_iff Abs_eq_iff) |
45 apply(simp_all only: t_tyS.eq_iff Abs_eq_iff) |
152 apply(simp_all only: alpha_gen) |
46 apply(simp_all only: alpha_gen) |
153 apply(simp_all only: eqvts[symmetric]) |
47 apply(simp_all only: eqvts[symmetric]) |
154 apply(simp_all only: eqvts eqvts_raw) |
48 apply(simp_all only: eqvts eqvts_raw) |
155 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
49 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
156 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
50 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
157 apply(simp_all only: de_Morgan_conj[symmetric]) |
51 apply(simp_all only: de_Morgan_conj[symmetric]) |
158 done |
52 done |
159 |
53 |
160 instance t and tyS :: fs |
54 instance t and tyS :: fs |
161 apply default |
55 apply default |
162 apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS) |
56 apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS) |
163 done |
57 done |
164 |
58 |
165 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS] |
59 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS] |
166 |
60 |
167 lemma induct: |
61 lemma induct: |
168 "\<lbrakk>\<And>name b. P b (Var name); |
62 "\<lbrakk>\<And>name b. P b (Var name); |
169 \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2); |
63 \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2); |
170 \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t) |
64 \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t) |
171 \<rbrakk> \<Longrightarrow> P a t" |
65 \<rbrakk> \<Longrightarrow> P a t" |
172 |
66 oops |
173 |
67 |
174 |
68 |
175 lemma |
69 lemma |
176 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
70 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
177 apply(simp add: t_tyS.eq_iff) |
71 apply(simp add: t_tyS.eq_iff) |