equal
deleted
inserted
replaced
153 let |
153 let |
154 val (cv, cta) = Thm.dest_abs NONE ct |
154 val (cv, cta) = Thm.dest_abs NONE ct |
155 val (v, _) = dest_Free (term_of cv) |
155 val (v, _) = dest_Free (term_of cv) |
156 val u_th = introduce_combinators_in_cterm cta |
156 val u_th = introduce_combinators_in_cterm cta |
157 val cu = Thm.rhs_of u_th |
157 val cu = Thm.rhs_of u_th |
158 val comb_eq = abstract (Thm.cabs cv cu) |
158 val comb_eq = abstract (Thm.lambda cv cu) |
159 in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
159 in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
160 | _ $ _ => |
160 | _ $ _ => |
161 let val (ct1, ct2) = Thm.dest_comb ct in |
161 let val (ct1, ct2) = Thm.dest_comb ct in |
162 Thm.combination (introduce_combinators_in_cterm ct1) |
162 Thm.combination (introduce_combinators_in_cterm ct1) |
163 (introduce_combinators_in_cterm ct2) |
163 (introduce_combinators_in_cterm ct2) |
203 case hilbert of |
203 case hilbert of |
204 Const (_, Type (@{type_name fun}, [_, T])) => T |
204 Const (_, Type (@{type_name fun}, [_, T])) => T |
205 | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"", |
205 | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"", |
206 [hilbert]) |
206 [hilbert]) |
207 val cex = cterm_of thy (HOLogic.exists_const T) |
207 val cex = cterm_of thy (HOLogic.exists_const T) |
208 val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) |
208 val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs) |
209 val conc = |
209 val conc = |
210 Drule.list_comb (rhs, frees) |
210 Drule.list_comb (rhs, frees) |
211 |> Drule.beta_conv cabs |> Thm.capply cTrueprop |
211 |> Drule.beta_conv cabs |> Thm.apply cTrueprop |
212 fun tacf [prem] = |
212 fun tacf [prem] = |
213 rewrite_goals_tac skolem_def_raw |
213 rewrite_goals_tac skolem_def_raw |
214 THEN rtac ((prem |> rewrite_rule skolem_def_raw) |
214 THEN rtac ((prem |> rewrite_rule skolem_def_raw) |
215 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1 |
215 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1 |
216 in |
216 in |