equal
deleted
inserted
replaced
28 |
28 |
29 (** instantiate elimination rules **) |
29 (** instantiate elimination rules **) |
30 |
30 |
31 local |
31 local |
32 val (cpfalse, cfalse) = |
32 val (cpfalse, cfalse) = |
33 `Old_SMT_Utils.mk_cprop (Thm.global_cterm_of @{theory} @{const False}) |
33 `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False}) |
34 |
34 |
35 fun inst f ct thm = |
35 fun inst f ct thm = |
36 let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) |
36 let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) |
37 in Thm.instantiate ([], [(cv, ct)]) thm end |
37 in Thm.instantiate ([], [(cv, ct)]) thm end |
38 in |
38 in |
201 |
201 |
202 val pat = |
202 val pat = |
203 Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1 |
203 Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1 |
204 fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct |
204 fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct |
205 |
205 |
206 fun mk_clist T = apply2 (Thm.global_cterm_of @{theory}) |
206 fun mk_clist T = apply2 (Thm.cterm_of @{context}) (HOLogic.cons_const T, HOLogic.nil_const T) |
207 (HOLogic.cons_const T, HOLogic.nil_const T) |
|
208 fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil |
207 fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil |
209 val mk_pat_list = mk_list (mk_clist @{typ pattern}) |
208 val mk_pat_list = mk_list (mk_clist @{typ pattern}) |
210 val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"}) |
209 val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"}) |
211 fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss |
210 fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss |
212 |
211 |