134 Applicable.Yes (Tactic.Or_to_List' (f, ls)) |
134 Applicable.Yes (Tactic.Or_to_List' (f, ls)) |
135 end |
135 end |
136 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = |
136 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = |
137 let |
137 let |
138 val (msg, thy', ro, rls', _) = get_ruleset thm p pt; |
138 val (msg, thy', ro, rls', _) = get_ruleset thm p pt; |
139 val thy = ThyC.id_to_ctxt thy'; |
139 val thy = ThyC.get_theory thy'; |
|
140 val ctxt = Proof_Context.init_global thy; |
140 val f = Calc.current_formula cs; |
141 val f = Calc.current_formula cs; |
141 in |
142 in |
142 if msg = "OK" |
143 if msg = "OK" |
143 then |
144 then |
144 case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of |
145 case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of |
145 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm))) |
146 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm))) |
146 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") |
147 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") |
147 else Applicable.No msg |
148 else Applicable.No msg |
148 end |
149 end |
149 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) = |
150 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) = |
154 val ctxt = Proof_Context.init_global thy; |
155 val ctxt = Proof_Context.init_global thy; |
155 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp); |
156 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp); |
156 val f = Calc.current_formula cs; |
157 val f = Calc.current_formula cs; |
157 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) |
158 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) |
158 in |
159 in |
159 case Rewrite.rewrite_inst_ ctxt (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of |
160 case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of |
160 SOME (f', asm) => |
161 SOME (f', asm) => |
161 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm))) |
162 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm))) |
162 | NONE => Applicable.No (fst thm ^ " not applicable") |
163 | NONE => Applicable.No (fst thm ^ " not applicable") |
163 end |
164 end |
164 | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) = |
165 | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) = |
196 val ctxt = Proof_Context.init_global thy; |
197 val ctxt = Proof_Context.init_global thy; |
197 val f = Calc.current_formula cs; |
198 val f = Calc.current_formula cs; |
198 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) |
199 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) |
199 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*) |
200 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*) |
200 val subst = Subst.T_from_string_eqs thy sube |
201 val subst = Subst.T_from_string_eqs thy sube |
201 val ro = Rewrite_Ord.assoc_rew_ord rew_ord' |
202 val ro = assoc_rew_ord thy rew_ord' |
202 in |
203 in |
203 if foldl and_ (true, map TermC.contains_Var subte) |
204 if foldl and_ (true, map TermC.contains_Var subte) |
204 then (*1*) |
205 then (*1*) |
205 let val f' = subst_atomic subst f |
206 let val f' = subst_atomic subst f |
206 in if f = f' |
207 in if f = f' |