41 | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r); |
41 | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r); |
42 |
42 |
43 (*the lists contain eq-al elem-pairs at the beginning; |
43 (*the lists contain eq-al elem-pairs at the beginning; |
44 return first list reverted (again) - ie. in order as required subsequently*) |
44 return first list reverted (again) - ie. in order as required subsequently*) |
45 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = |
45 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = |
46 if equal f1 i1 |
46 if equal f1 i1 then |
47 then |
|
48 if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is) |
47 if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is) |
49 else (rev (f1 :: f2 :: fs), i1 :: i2 :: is) |
48 else (rev (f1 :: f2 :: fs), i1 :: i2 :: is) |
50 else error "dropwhile': did not start with equal elements" |
49 else error "dropwhile': did not start with equal elements" |
51 | dropwhile' equal (f::fs) [i] = |
50 | dropwhile' equal (f::fs) [i] = |
52 if equal f i |
51 if equal f i then |
53 then (rev (f::fs), [i]) |
52 (rev (f::fs), [i]) |
54 else error "dropwhile': did not start with equal elements" |
53 else error "dropwhile': did not start with equal elements" |
55 | dropwhile' equal [f] (i::is) = |
54 | dropwhile' equal [f] (i::is) = |
56 if equal f i |
55 if equal f i then |
57 then ([f], i::is) |
56 ([f], i::is) |
58 else error "dropwhile': did not start with equal elements" |
57 else error "dropwhile': did not start with equal elements" |
59 | dropwhile' _ _ _ = error "dropwhile': uncovered case" |
58 | dropwhile' _ _ _ = error "dropwhile': uncovered case" |
60 |
59 |
61 (* 040214: version for concat_deriv *) |
60 (* 040214: version for concat_deriv *) |
62 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a)); |
61 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a)); |
83 case (fod, ifod) of |
82 case (fod, ifod) of |
84 ([], []) => if fo = ifo then (true, []) else (false, []) |
83 ([], []) => if fo = ifo then (true, []) else (false, []) |
85 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) |
84 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) |
86 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) |
85 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) |
87 | (fod, ifod) => |
86 | (fod, ifod) => |
88 if derivat fod = derivat ifod (*common normal form found*) |
87 if derivat fod = derivat ifod (*common normal form found*) then |
89 then |
|
90 let |
88 let |
91 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod) |
89 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod) |
92 in (true, fod' @ (map rev_deriv' rifod')) end |
90 in (true, fod' @ (map rev_deriv' rifod')) end |
93 else (false, []) |
91 else (false, []) |
94 end |
92 end |
99 fun check_err_patt (res, inf) subst (errpatID, pat) rls = |
97 fun check_err_patt (res, inf) subst (errpatID, pat) rls = |
100 let |
98 let |
101 val (res', _, _, rewritten) = |
99 val (res', _, _, rewritten) = |
102 Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res; |
100 Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res; |
103 in |
101 in |
104 if rewritten |
102 if rewritten then |
105 then |
|
106 let |
103 let |
107 val norm_res = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls res' of |
104 val norm_res = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls res' of |
108 NONE => res' |
105 NONE => res' |
109 | SOME (norm_res, _) => norm_res |
106 | SOME (norm_res, _) => norm_res |
110 val norm_inf = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls inf of |
107 val norm_inf = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls inf of |
137 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) = |
134 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) = |
138 let |
135 let |
139 val (form', _, _, rewritten) = |
136 val (form', _, _, rewritten) = |
140 Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form; |
137 Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form; |
141 in (*the fillpat of the thm must be dedicated to errpatID*) |
138 in (*the fillpat of the thm must be dedicated to errpatID*) |
142 if errpatID = erpaID andalso rewritten |
139 if errpatID = erpaID andalso rewritten then |
143 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
140 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
144 else NONE |
141 else NONE |
145 end |
142 end |
146 |
143 |
147 fun get_fillpats subst form errpatID thm = |
144 fun get_fillpats subst form errpatID thm = |
148 let |
145 let |
187 val res = case rew of |
184 val res = case rew of |
188 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res |
185 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res |
189 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res |
186 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res |
190 | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t) |
187 | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t) |
191 in |
188 in |
192 if not (ifo = res) |
189 if not (ifo = res) then |
193 then ("input does not exactly fill the gaps", Tactic.Tac "") |
190 ("input does not exactly fill the gaps", Tactic.Tac "") |
194 else ("ok", tac) |
191 else ("ok", tac) |
195 end |
192 end |
196 end |
193 end |
197 |
194 |
198 (* fetch errpatIDs from an arbitrary tactic *) |
195 (* fetch errpatIDs from an arbitrary tactic *) |