1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -28,12 +28,12 @@
1.4 | Empty_Tac_
1.5 | Free_Solve'
1.6 | Or_to_List' of term * term
1.7 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
1.8 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.9 + | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
1.10 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.11 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
1.12 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
1.13 | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
1.14 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
1.15 + | Substitute' of Rewrite_Ord.function * Rule_Set.T * Subst.as_eqs * term * term
1.16 (*RM*)| Tac_ of theory * string * string * string
1.17 | Take' of term
1.18 | End_Detail' of Celem.result
1.19 @@ -240,7 +240,7 @@
1.20
1.21 (* try if a rewrite-rule is applicable to a given formula;
1.22 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
1.23 -fun try_rew ctxt ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
1.24 +fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
1.25 if Auto_Prog.contains_bdv thm
1.26 then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of
1.27 SOME _ => [rule2tac ctxt subst thm']
1.28 @@ -268,7 +268,7 @@
1.29 (* decide if a tactic is applicable to a given formula;
1.30 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
1.31 fun applicable ctxt _ _ f (Calculate scrID) =
1.32 - try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f
1.33 + try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f
1.34 (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
1.35 | applicable ctxt ro erls f (Rewrite thm'') =
1.36 try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
1.37 @@ -325,8 +325,8 @@
1.38 | Empty_Tac_
1.39 | Free_Solve'
1.40 | Or_to_List' of term * term
1.41 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
1.42 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.43 + | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
1.44 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
1.45 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
1.46 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
1.47 | Subproblem' of (* switch from solve-phase to specify-phase *)
1.48 @@ -337,7 +337,7 @@
1.49 Proof.context * (* for the specify-phase *)
1.50 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
1.51 | Substitute' of (* substitute variables (TODO: from the context) *)
1.52 - Rule_Def.rew_ord_ *(* for re-calculation *)
1.53 + Rewrite_Ord.function *(* for re-calculation *)
1.54 Rule_Set.T * (* for re-calculation *)
1.55 Subst.as_eqs * (* the substitution: terms of type bool *)
1.56 term * (* to be substituted into *)