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 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)" |
|
59 apply (induct l) |
|
60 apply (simp_all) |
|
61 apply (simp only: eqvt_apply) |
|
62 done |
|
63 |
|
64 lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)" |
|
65 by (lifting map_eqvt) |
|
66 |
12 |
67 nominal_datatype t = |
13 nominal_datatype t = |
68 Var "name" |
14 Var "name" |
69 | Fun "t" "t" |
15 | Fun "t" "t" |
70 and tyS = |
16 and tyS = |
74 thm t_tyS.eq_iff |
20 thm t_tyS.eq_iff |
75 thm t_tyS.bn |
21 thm t_tyS.bn |
76 thm t_tyS.perm |
22 thm t_tyS.perm |
77 thm t_tyS.inducts |
23 thm t_tyS.inducts |
78 thm t_tyS.distinct |
24 thm t_tyS.distinct |
|
25 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
79 |
26 |
80 lemma finite_fv_t_tyS: |
27 lemma finite_fv_t_tyS: |
81 shows "finite (fv_t t)" "finite (fv_tyS ts)" |
28 shows "finite (fv_t t)" "finite (fv_tyS ts)" |
82 by (induct rule: t_tyS.inducts) (simp_all) |
29 by (induct rule: t_tyS.inducts) (simp_all) |
83 |
30 |
84 lemma infinite_Un: |
|
85 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
86 by simp |
|
87 |
|
88 lemma supp_fv_t_tyS: |
31 lemma supp_fv_t_tyS: |
89 shows "fv_t t = supp t" "fv_tyS ts = supp ts" |
32 shows "fv_t t = supp t" "fv_tyS ts = supp ts" |
90 apply(induct rule: t_tyS.inducts) |
33 apply(induct rule: t_tyS.inducts) |
91 apply(simp_all only: t_tyS.fv) |
34 apply(simp_all only: t_tyS.fv) |
92 prefer 3 |
35 prefer 3 |
93 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) |
94 prefer 2 |
37 prefer 2 |
95 apply(subst finite_supp_Abs) |
38 apply(subst finite_supp_Abs) |
96 apply(drule sym) |
39 apply(drule sym) |
97 apply(simp add: finite_fv_t_tyS(1)) |
40 apply(simp add: finite_fv_t_tyS(1)) |
98 apply(simp) |
41 apply(simp) |
99 apply(simp_all (no_asm) only: supp_def) |
42 apply(simp_all (no_asm) only: supp_def) |
100 apply(simp_all only: t_tyS.perm) |
43 apply(simp_all only: t_tyS.perm) |
101 apply(simp_all only: permute_ABS) |
44 apply(simp_all only: permute_ABS) |
102 apply(simp_all only: t_tyS.eq_iff Abs_eq_iff) |
45 apply(simp_all only: t_tyS.eq_iff Abs_eq_iff) |
103 apply(simp_all only: alpha_gen) |
46 apply(simp_all only: alpha_gen) |
104 apply(simp_all only: eqvts[symmetric]) |
47 apply(simp_all only: eqvts[symmetric]) |
105 apply(simp_all only: eqvts eqvts_raw) |
48 apply(simp_all only: eqvts eqvts_raw) |
106 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
49 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
107 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
50 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
108 apply(simp_all only: de_Morgan_conj[symmetric]) |
51 apply(simp_all only: de_Morgan_conj[symmetric]) |
109 done |
52 done |
110 |
53 |
111 instance t and tyS :: fs |
54 instance t and tyS :: fs |
112 apply default |
55 apply default |
113 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) |
114 done |
57 done |
115 |
58 |
116 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] |
117 |
60 |
118 lemma induct: |
61 lemma induct: |
119 "\<lbrakk>\<And>name b. P b (Var name); |
62 "\<lbrakk>\<And>name b. P b (Var name); |
120 \<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); |
121 \<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) |
122 \<rbrakk> \<Longrightarrow> P a t" |
65 \<rbrakk> \<Longrightarrow> P a t" |
123 |
66 oops |
124 |
67 |
125 |
68 |
126 lemma |
69 lemma |
127 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))" |
128 apply(simp add: t_tyS.eq_iff) |
71 apply(simp add: t_tyS.eq_iff) |