equal
deleted
inserted
replaced
88 | is_quasi_lambda_free _ = true |
88 | is_quasi_lambda_free _ = true |
89 |
89 |
90 fun abstract ctxt ct = |
90 fun abstract ctxt ct = |
91 let |
91 let |
92 val Abs (_, _, body) = Thm.term_of ct |
92 val Abs (_, _, body) = Thm.term_of ct |
93 val (x, cbody) = Thm.dest_abs NONE ct |
93 val (x, cbody) = Thm.dest_abs ct |
94 val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct) |
94 val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct) |
95 fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K} |
95 fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K} |
96 in |
96 in |
97 case body of |
97 case body of |
98 Const _ => makeK() |
98 Const _ => makeK() |
140 if is_quasi_lambda_free (Thm.term_of ct) then |
140 if is_quasi_lambda_free (Thm.term_of ct) then |
141 Thm.reflexive ct |
141 Thm.reflexive ct |
142 else case Thm.term_of ct of |
142 else case Thm.term_of ct of |
143 Abs _ => |
143 Abs _ => |
144 let |
144 let |
145 val (cv, cta) = Thm.dest_abs NONE ct |
145 val (cv, cta) = Thm.dest_abs ct |
146 val (v, _) = dest_Free (Thm.term_of cv) |
146 val (v, _) = dest_Free (Thm.term_of cv) |
147 val u_th = introduce_combinators_in_cterm ctxt cta |
147 val u_th = introduce_combinators_in_cterm ctxt cta |
148 val cu = Thm.rhs_of u_th |
148 val cu = Thm.rhs_of u_th |
149 val comb_eq = abstract ctxt (Thm.lambda cv cu) |
149 val comb_eq = abstract ctxt (Thm.lambda cv cu) |
150 in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
150 in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
172 val cTrueprop = Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop; |
172 val cTrueprop = Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop; |
173 |
173 |
174 (*Given an abstraction over n variables, replace the bound variables by free |
174 (*Given an abstraction over n variables, replace the bound variables by free |
175 ones. Return the body, along with the list of free variables.*) |
175 ones. Return the body, along with the list of free variables.*) |
176 fun c_variant_abs_multi (ct0, vars) = |
176 fun c_variant_abs_multi (ct0, vars) = |
177 let val (cv,ct) = Thm.dest_abs NONE ct0 |
177 let val (cv,ct) = Thm.dest_abs ct0 |
178 in c_variant_abs_multi (ct, cv::vars) end |
178 in c_variant_abs_multi (ct, cv::vars) end |
179 handle CTERM _ => (ct0, rev vars); |
179 handle CTERM _ => (ct0, rev vars); |
180 |
180 |
181 (* Given the definition of a Skolem function, return a theorem to replace |
181 (* Given the definition of a Skolem function, return a theorem to replace |
182 an existential formula by a use of that function. |
182 an existential formula by a use of that function. |
264 ct |
264 ct |
265 |> (case Thm.term_of ct of |
265 |> (case Thm.term_of ct of |
266 Const (s, _) $ Abs (s', _, _) => |
266 Const (s, _) $ Abs (s', _, _) => |
267 if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse |
267 if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse |
268 s = \<^const_name>\<open>Ex\<close> then |
268 s = \<^const_name>\<open>Ex\<close> then |
269 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos |
269 Thm.dest_comb #> snd #> Thm.dest_abs_name s' #> snd #> zap pos |
270 else |
270 else |
271 Conv.all_conv |
271 Conv.all_conv |
272 | Const (s, _) $ _ $ _ => |
272 | Const (s, _) $ _ $ _ => |
273 if s = \<^const_name>\<open>Pure.imp\<close> orelse s = \<^const_name>\<open>implies\<close> then |
273 if s = \<^const_name>\<open>Pure.imp\<close> orelse s = \<^const_name>\<open>implies\<close> then |
274 Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) |
274 Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) |