1 theory TySch |
1 theory TySch |
2 imports "Parser" "../Attic/Prove" |
2 imports "Parser" "../Attic/Prove" "FSet" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
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 |
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 |
13 nominal_datatype t = |
67 nominal_datatype t = |
14 Var "name" |
68 Var "name" |
15 | Fun "t" "t" |
69 | Fun "t" "t" |
16 and tyS = |
70 and tyS = |
17 All xs::"name set" ty::"t" bind xs in ty |
71 All xs::"name fset" ty::"t" bind xs in ty |
18 |
72 |
19 thm t_tyS.fv |
73 thm t_tyS.fv |
20 thm t_tyS.eq_iff |
74 thm t_tyS.eq_iff |
21 thm t_tyS.bn |
75 thm t_tyS.bn |
22 thm t_tyS.perm |
76 thm t_tyS.perm |
23 thm t_tyS.induct |
77 thm t_tyS.inducts |
24 thm t_tyS.distinct |
78 thm t_tyS.distinct |
25 |
79 |
|
80 lemma finite_fv_t_tyS: |
|
81 shows "finite (fv_t t)" "finite (fv_tyS ts)" |
|
82 by (induct rule: t_tyS.inducts) (simp_all) |
|
83 |
|
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: |
|
89 shows "fv_t t = supp t" "fv_tyS ts = supp ts" |
|
90 apply(induct rule: t_tyS.inducts) |
|
91 apply(simp_all only: t_tyS.fv) |
|
92 prefer 3 |
|
93 apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) |
|
94 prefer 2 |
|
95 apply(subst finite_supp_Abs) |
|
96 apply(drule sym) |
|
97 apply(simp add: finite_fv_t_tyS(1)) |
|
98 apply(simp) |
|
99 apply(simp_all (no_asm) only: supp_def) |
|
100 apply(simp_all only: t_tyS.perm) |
|
101 apply(simp_all only: permute_ABS) |
|
102 apply(simp_all only: t_tyS.eq_iff Abs_eq_iff) |
|
103 apply(simp_all only: alpha_gen) |
|
104 apply(simp_all only: eqvts[symmetric]) |
|
105 apply(simp_all only: eqvts eqvts_raw) |
|
106 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
|
107 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
|
108 apply(simp_all only: de_Morgan_conj[symmetric]) |
|
109 done |
|
110 |
|
111 instance t and tyS :: fs |
|
112 apply default |
|
113 apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS) |
|
114 done |
|
115 |
|
116 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS] |
|
117 |
|
118 lemma induct: |
|
119 "\<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); |
|
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) |
|
122 \<rbrakk> \<Longrightarrow> P a t" |
|
123 |
|
124 |
|
125 |
26 lemma |
126 lemma |
27 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
127 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
28 apply(simp add: t_tyS.eq_iff) |
128 apply(simp add: t_tyS.eq_iff) |
29 apply(rule_tac x="0::perm" in exI) |
129 apply(rule_tac x="0::perm" in exI) |
30 apply(simp add: alpha_gen) |
130 apply(simp add: alpha_gen) |
31 apply(auto) |
131 apply(auto) |
32 apply(simp add: fresh_star_def fresh_zero_perm) |
132 apply(simp add: fresh_star_def fresh_zero_perm) |
33 done |
133 done |
34 |
134 |
35 lemma |
135 lemma |
36 shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" |
136 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
37 apply(simp add: t_tyS.eq_iff) |
137 apply(simp add: t_tyS.eq_iff) |
38 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
138 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
39 apply(simp add: alpha_gen fresh_star_def eqvts) |
139 apply(simp add: alpha_gen fresh_star_def eqvts) |
40 apply auto |
140 apply auto |
41 done |
141 done |
42 |
142 |
43 lemma |
143 lemma |
44 shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" |
144 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
45 apply(simp add: t_tyS.eq_iff) |
145 apply(simp add: t_tyS.eq_iff) |
46 apply(rule_tac x="0::perm" in exI) |
146 apply(rule_tac x="0::perm" in exI) |
47 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
147 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
48 oops |
148 oops |
49 |
149 |
50 lemma |
150 lemma |
51 assumes a: "a \<noteq> b" |
151 assumes a: "a \<noteq> b" |
52 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" |
152 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
53 using a |
153 using a |
54 apply(simp add: t_tyS.eq_iff) |
154 apply(simp add: t_tyS.eq_iff) |
55 apply(clarify) |
155 apply(clarify) |
56 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
156 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
57 apply auto |
157 apply auto |