53 |
53 |
54 (* |
54 (* |
55 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls |
55 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls |
56 *) |
56 *) |
57 fun check_for' (res, inf) subst (id, pat) rls = |
57 fun check_for' (res, inf) subst (id, pat) rls = |
58 let |
58 let |
59 val (res', _, _, rewritten) = Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord |
59 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
60 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
60 val (res', _, _, rewritten) = |
|
61 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord |
|
62 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
61 in |
63 in |
62 if rewritten then |
64 if rewritten then |
63 let |
65 let |
64 val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of |
66 val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of |
65 NONE => res' |
67 NONE => res' |
66 | SOME (norm_res, _) => norm_res |
68 | SOME (norm_res, _) => norm_res |
67 val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of |
69 val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of |
68 NONE => inf |
70 NONE => inf |
69 | SOME (norm_inf, _) => norm_inf |
71 | SOME (norm_inf, _) => norm_inf |
70 in |
72 in |
71 if norm_res = norm_inf then SOME id else NONE |
73 if norm_res = norm_inf then SOME id else NONE |
72 end |
74 end |
94 |
96 |
95 (* fill-in patterns an forms. |
97 (* fill-in patterns an forms. |
96 returns thm required by "fun in_fillform *) |
98 returns thm required by "fun in_fillform *) |
97 fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) = |
99 fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) = |
98 let |
100 let |
|
101 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
99 val (form', _, _, rewritten) = |
102 val (form', _, _, rewritten) = |
100 Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
103 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
101 in (*the fillpat of the thm must be dedicated to id*) |
104 in (*the fillpat of the thm must be dedicated to id*) |
102 if id = erpaID andalso rewritten then |
105 if id = erpaID andalso rewritten then |
103 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
106 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
104 else NONE |
107 else NONE |
105 end |
108 end |