equal
deleted
inserted
replaced
39 val p = Thm.dest_arg ep |
39 val p = Thm.dest_arg ep |
40 val ths = |
40 val ths = |
41 simplify (put_simpset HOL_basic_ss ctxt addsimps gather) |
41 simplify (put_simpset HOL_basic_ss ctxt addsimps gather) |
42 (Thm.instantiate' [] [SOME p] stupid) |
42 (Thm.instantiate' [] [SOME p] stupid) |
43 val (L, U) = |
43 val (L, U) = |
44 let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths)) |
44 let val (_, q) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of ths)) |
45 in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end |
45 in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end |
46 fun proveneF S = |
46 fun proveneF S = |
47 let |
47 let |
48 val (a, A) = Thm.dest_comb S |>> Thm.dest_arg |
48 val (a, A) = Thm.dest_comb S |>> Thm.dest_arg |
49 val cT = Thm.ctyp_of_cterm a |
49 val cT = Thm.ctyp_of_cterm a |
129 fun proc ctxt ct = |
129 fun proc ctxt ct = |
130 (case Thm.term_of ct of |
130 (case Thm.term_of ct of |
131 \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> => |
131 \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> => |
132 let |
132 let |
133 val e = Thm.dest_fun ct |
133 val e = Thm.dest_fun ct |
134 val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct) |
134 val (x,p) = Thm.dest_abs_name xn (Thm.dest_arg ct) |
135 val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p |
135 val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p |
136 val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p) |
136 val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p) |
137 in |
137 in |
138 (case eqs of |
138 (case eqs of |
139 [] => |
139 [] => |
208 | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm) |
208 | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm) |
209 | _ => Thm.dest_fun2 tm) |
209 | _ => Thm.dest_fun2 tm) |
210 and find_args bounds tm = |
210 and find_args bounds tm = |
211 (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm)) |
211 (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm)) |
212 and find_body bounds b = |
212 and find_body bounds b = |
213 let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b |
213 let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b |
214 in h (bounds + 1) b' end; |
214 in h (bounds + 1) b' end; |
215 in h end; |
215 in h end; |
216 |
216 |
217 fun dlo_instance ctxt tm = |
217 fun dlo_instance ctxt tm = |
218 (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm)); |
218 (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm)); |
238 _ $ _ $ _ => |
238 _ $ _ $ _ => |
239 if member (op aconvc) ats (Thm.dest_fun2 t) |
239 if member (op aconvc) ats (Thm.dest_fun2 t) |
240 then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) |
240 then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) |
241 else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
241 else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
242 | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
242 | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
243 | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) |
243 | Abs _ => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc)) |
244 | Free _ => if member (op aconvc) ats t then acc else ins t acc |
244 | Free _ => if member (op aconvc) ats t then acc else ins t acc |
245 | Var _ => if member (op aconvc) ats t then acc else ins t acc |
245 | Var _ => if member (op aconvc) ats t then acc else ins t acc |
246 | _ => acc) |
246 | _ => acc) |
247 in h [] ct end |
247 in h [] ct end |
248 |
248 |