118 |
118 |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
120 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
120 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
121 thm alpha1_equivp |
121 thm alpha1_equivp |
122 |
122 |
123 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
123 ML {* |
124 by (rule alpha1_equivp(1)) |
124 fun define_quotient_type args tac ctxt = |
|
125 let |
|
126 val mthd = Method.SIMPLE_METHOD tac |
|
127 val mthdt = Method.Basic (fn _ => mthd) |
|
128 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
129 in |
|
130 bymt (Quotient_Type.quotient_type args ctxt) |
|
131 end |
|
132 *} |
|
133 |
|
134 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
|
135 (rtac @{thm alpha1_equivp(1)} 1) |
|
136 *} |
125 |
137 |
126 local_setup {* |
138 local_setup {* |
127 (fn ctxt => ctxt |
139 (fn ctxt => ctxt |
128 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
140 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
129 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
141 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
131 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
143 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
132 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
144 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
133 *} |
145 *} |
134 print_theorems |
146 print_theorems |
135 |
147 |
136 lemma alpha_rfv1: |
148 lemma fv_rtrm1_rsp: |
137 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
149 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
138 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
150 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
139 apply(simp_all add: alpha_gen.simps alpha_bp_eq) |
151 apply(simp_all add: alpha_gen.simps alpha_bp_eq) |
140 done |
152 done |
141 |
153 |
142 lemma [quot_respect]: |
154 lemma [quot_respect]: |
143 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
155 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
144 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
156 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
145 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
157 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
146 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
158 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
147 apply (auto simp add: alpha1_inj alpha_bp_eq) |
159 apply (simp_all only: fun_rel_def alpha1_inj alpha_bp_eq) |
|
160 apply (clarify) |
|
161 apply (clarify) |
|
162 apply (clarify) |
|
163 apply (auto) |
148 apply (rule_tac [!] x="0" in exI) |
164 apply (rule_tac [!] x="0" in exI) |
149 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) |
165 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm fv_rtrm1_rsp) |
150 done |
166 done |
151 |
167 |
152 lemma [quot_respect]: |
168 lemma [quot_respect]: |
153 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" |
169 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" |
154 by (simp add: alpha1_eqvt) |
170 by (simp add: alpha1_eqvt) |
155 |
171 |
156 lemma [quot_respect]: |
172 lemma [quot_respect]: |
157 "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" |
173 "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" |
158 by (simp add: alpha_rfv1) |
174 by (simp add: fv_rtrm1_rsp) |
159 |
175 |
160 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
176 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
161 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
177 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
162 |
178 |
163 instantiation trm1 and bp :: pt |
179 instantiation trm1 and bp :: pt |