|
1 theory Term5 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 datatype rtrm5 = |
|
8 rVr5 "name" |
|
9 | rAp5 "rtrm5" "rtrm5" |
|
10 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
11 and rlts = |
|
12 rLnil |
|
13 | rLcons "name" "rtrm5" "rlts" |
|
14 |
|
15 primrec |
|
16 rbv5 |
|
17 where |
|
18 "rbv5 rLnil = {}" |
|
19 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
20 |
|
21 |
|
22 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *} |
|
23 print_theorems |
|
24 |
|
25 local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
|
26 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
|
27 print_theorems |
|
28 |
|
29 (* Alternate version with additional binding of name in rlts in rLcons *) |
|
30 (*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
|
31 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
|
32 print_theorems*) |
|
33 |
|
34 notation |
|
35 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
|
36 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
|
37 thm alpha_rtrm5_alpha_rlts.intros |
|
38 |
|
39 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
|
40 thm alpha5_inj |
|
41 |
|
42 lemma rbv5_eqvt[eqvt]: |
|
43 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
|
44 apply (induct x) |
|
45 apply (simp_all add: eqvts atom_eqvt) |
|
46 done |
|
47 |
|
48 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
|
49 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
|
50 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
|
51 apply (induct x and l) |
|
52 apply (simp_all add: eqvts atom_eqvt) |
|
53 done |
|
54 |
|
55 lemma alpha5_eqvt: |
|
56 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
|
57 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
|
58 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
|
59 apply (simp_all add: alpha5_inj) |
|
60 apply (tactic {* |
|
61 ALLGOALS ( |
|
62 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
63 (etac @{thm alpha_gen_compose_eqvt}) |
|
64 ) *}) |
|
65 apply (simp_all only: eqvts atom_eqvt) |
|
66 done |
|
67 |
|
68 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
|
69 (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} |
|
70 thm alpha5_equivp |
|
71 |
|
72 quotient_type |
|
73 trm5 = rtrm5 / alpha_rtrm5 |
|
74 and |
|
75 lts = rlts / alpha_rlts |
|
76 by (auto intro: alpha5_equivp) |
|
77 |
|
78 local_setup {* |
|
79 (fn ctxt => ctxt |
|
80 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
|
81 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
|
82 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
|
83 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
|
84 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
|
85 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
|
86 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
|
87 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
|
88 *} |
|
89 print_theorems |
|
90 |
|
91 lemma alpha5_rfv: |
|
92 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
|
93 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
|
94 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
|
95 apply(simp_all add: alpha_gen) |
|
96 done |
|
97 |
|
98 lemma bv_list_rsp: |
|
99 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
|
100 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) |
|
101 apply(simp_all) |
|
102 done |
|
103 |
|
104 lemma [quot_respect]: |
|
105 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
|
106 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
|
107 "(alpha_rlts ===> op =) rbv5 rbv5" |
|
108 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
|
109 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
|
110 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
|
111 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
|
112 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
|
113 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
|
114 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
|
115 apply (clarify) apply (rule conjI) |
|
116 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
117 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
118 done |
|
119 |
|
120 lemma |
|
121 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
|
122 by (simp add: bv_list_rsp) |
|
123 |
|
124 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
|
125 |
|
126 instantiation trm5 and lts :: pt |
|
127 begin |
|
128 |
|
129 quotient_definition |
|
130 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
131 is |
|
132 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
|
133 |
|
134 quotient_definition |
|
135 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
136 is |
|
137 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
|
138 |
|
139 instance by default |
|
140 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
|
141 |
|
142 end |
|
143 |
|
144 lemmas |
|
145 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
|
146 and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
147 and bv5[simp] = rbv5.simps[quot_lifted] |
|
148 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
149 |
|
150 lemma lets_ok: |
|
151 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
152 apply (subst alpha5_INJ) |
|
153 apply (rule conjI) |
|
154 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
155 apply (simp only: alpha_gen) |
|
156 apply (simp add: permute_trm5_lts fresh_star_def) |
|
157 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
158 apply (simp only: alpha_gen) |
|
159 apply (simp add: permute_trm5_lts fresh_star_def) |
|
160 done |
|
161 |
|
162 lemma lets_ok2: |
|
163 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
164 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
165 apply (subst alpha5_INJ) |
|
166 apply (rule conjI) |
|
167 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
168 apply (simp only: alpha_gen) |
|
169 apply (simp add: permute_trm5_lts fresh_star_def) |
|
170 apply (rule_tac x="0 :: perm" in exI) |
|
171 apply (simp only: alpha_gen) |
|
172 apply (simp add: permute_trm5_lts fresh_star_def) |
|
173 done |
|
174 |
|
175 |
|
176 lemma lets_not_ok1: |
|
177 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
178 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
179 apply (simp add: alpha5_INJ(3) alpha_gen) |
|
180 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) |
|
181 done |
|
182 |
|
183 lemma distinct_helper: |
|
184 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
|
185 apply auto |
|
186 apply (erule alpha_rtrm5.cases) |
|
187 apply (simp_all only: rtrm5.distinct) |
|
188 done |
|
189 |
|
190 lemma distinct_helper2: |
|
191 shows "(Vr5 x) \<noteq> (Ap5 y z)" |
|
192 by (lifting distinct_helper) |
|
193 |
|
194 lemma lets_nok: |
|
195 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
196 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
197 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
198 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
|
199 apply (simp add: distinct_helper2) |
|
200 done |
|
201 |
|
202 |
|
203 end |