27 term App |
27 term App |
28 term Baz |
28 term Baz |
29 term bn |
29 term bn |
30 term fv_trm |
30 term fv_trm |
31 |
31 |
|
32 lemma a1: |
|
33 shows "alpha_trm_raw x1 y1 \<Longrightarrow> True" |
|
34 and "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2" |
|
35 and "alpha_bn_raw x3 y3 \<Longrightarrow> True" |
|
36 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
|
37 apply(simp_all) |
|
38 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
39 apply(assumption) |
|
40 done |
|
41 |
|
42 lemma a2: |
|
43 shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1" |
|
44 and "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2" |
|
45 and "alpha_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3" |
|
46 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
|
47 apply(simp_all add: alphas a1 prod_alpha_def) |
|
48 apply(auto) |
|
49 done |
|
50 |
32 lemma [quot_respect]: |
51 lemma [quot_respect]: |
33 "(op = ===> alpha_trm_raw) Var_raw Var_raw" |
52 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
34 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
53 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
|
54 "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw" |
|
55 "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw" |
|
56 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) |
|
57 Foo_raw Foo_raw" |
|
58 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
|
59 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
|
60 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
35 apply(auto) |
61 apply(auto) |
36 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
62 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
37 apply(rule refl) |
63 apply(rule refl) |
38 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
64 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
39 apply(assumption) |
65 apply(assumption) |
40 apply(assumption) |
66 apply(assumption) |
41 done |
67 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
68 apply(rule_tac x="0" in exI) |
|
69 apply(simp add: alphas fresh_star_def fresh_zero_perm a2) |
|
70 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
71 apply(rule_tac x="0" in exI) |
|
72 apply(simp add: alphas fresh_star_def fresh_zero_perm a2) |
|
73 apply(simp add: a1) |
|
74 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
75 apply(rule_tac x="0" in exI) |
|
76 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
77 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
78 apply(rule_tac x="0" in exI) |
|
79 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
80 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
81 apply(rule_tac x="0" in exI) |
|
82 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
83 apply(rule_tac x="0" in exI) |
|
84 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
85 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
86 apply(rule_tac x="0" in exI) |
|
87 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
88 apply(rule refl) |
|
89 done |
|
90 |
|
91 lemma [quot_respect]: |
|
92 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
|
93 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
|
94 "(alpha_assg_raw ===> op =) bn_raw bn_raw" |
|
95 "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" |
|
96 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
|
97 apply(simp_all add: a2 a1) |
|
98 sorry |
|
99 |
|
100 ML {* |
|
101 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
|
102 *} |
|
103 |
|
104 ML {* |
|
105 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} |
|
106 *} |
|
107 |
|
108 ML {* |
|
109 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
|
110 *} |
|
111 |
|
112 thm perm_defs[no_vars] |
|
113 |
|
114 instance trm :: pt sorry |
|
115 instance assg :: pt sorry |
|
116 |
|
117 lemma |
|
118 "p \<bullet> Var name = Var (p \<bullet> name)" |
|
119 "p \<bullet> App trm1 trm2 = App (p \<bullet> trm1) (p \<bullet> trm2)" |
|
120 "p \<bullet> Lam name trm = Lam (p \<bullet> name) (p \<bullet> trm)" |
|
121 "p \<bullet> Let assg trm = Let (p \<bullet> assg) (p \<bullet> trm)" |
|
122 "p \<bullet> Foo name1 name2 trm1 trm2 trm3 = |
|
123 Foo (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm1) (p \<bullet> trm2) (p \<bullet> trm3)" |
|
124 "p \<bullet> Bar name1 name2 trm = Bar (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm)" |
|
125 "p \<bullet> Baz name trm1 trm2 = Baz (p \<bullet> name) (p \<bullet> trm1) (p \<bullet> trm2)" |
|
126 "p \<bullet> As name1 name2 trm = As (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm)" |
|
127 sorry |
|
128 |
|
129 |
|
130 (* |
|
131 ML {* |
|
132 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_defs} |
|
133 *} |
|
134 *) |
|
135 |
|
136 local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *} |
|
137 local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *} |
|
138 local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *} |
|
139 |
|
140 thm perm_defs |
|
141 thm perm_simps |
|
142 |
|
143 instance trm :: pt sorry |
|
144 instance assg :: pt sorry |
|
145 |
|
146 lemma supp_fv: |
|
147 "supp t = fv_trm t" |
|
148 "supp b = fv_bn b" |
|
149 apply(induct t and b rule: i1) |
|
150 apply(simp_all add: f1) |
|
151 apply(simp_all add: supp_def) |
|
152 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
153 apply(simp only: supp_at_base[simplified supp_def]) |
|
154 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
155 apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute) |
|
156 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
|
157 apply(simp add: supp_Abs fv_trm1) |
|
158 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
|
159 apply(simp add: alpha1_INJ) |
|
160 apply(simp add: Abs_eq_iff) |
|
161 apply(simp add: alpha_gen.simps) |
|
162 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
|
163 apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair) |
|
164 apply blast |
|
165 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
166 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
167 apply(simp only: supp_at_base[simplified supp_def]) |
|
168 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq]) |
|
169 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
170 apply(fold supp_def) |
|
171 apply simp |
|
172 done |
|
173 |
|
174 ML {* |
|
175 map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff} |
|
176 *} |
|
177 |
|
178 |
42 |
179 |
43 |
180 |
44 |
181 |
45 lemma "Var x \<noteq> App y1 y2" |
182 lemma "Var x \<noteq> App y1 y2" |
46 apply(descending) |
183 apply(descending) |