1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 24 09:01:48 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 27 12:36:21 2020 +0200
1.3 @@ -55,7 +55,7 @@
1.4 (*Istate.T * ? *)
1.5 Proof.context * (* derived from prog. in ??? *)
1.6 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
1.7 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Selem.subte * term * term
1.8 + | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_equality * term * term
1.9 | Tac_ of theory * string * string * string
1.10 | Take' of term
1.11 val string_of: T -> string
1.12 @@ -79,7 +79,7 @@
1.13
1.14 | Derive of Rule_Set.id
1.15 | Detail_Set of Rule_Set.id
1.16 - | Detail_Set_Inst of Selem.subs * Rule_Set.id
1.17 + | Detail_Set_Inst of Subst.input * Rule_Set.id
1.18 | End_Detail
1.19
1.20 | Empty_Tac
1.21 @@ -92,16 +92,16 @@
1.22 | Refine_Tacitly of Problem.id
1.23
1.24 | Rewrite of ThmC.T
1.25 - | Rewrite_Inst of Selem.subs * ThmC.T
1.26 + | Rewrite_Inst of Subst.input * ThmC.T
1.27 | Rewrite_Set of Rule_Set.id
1.28 - | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
1.29 + | Rewrite_Set_Inst of Subst.input * Rule_Set.id
1.30
1.31 | Specify_Method of Method.id
1.32 | Specify_Problem of Problem.id
1.33 | Specify_Theory of ThyC.id
1.34 | Subproblem of ThyC.id * Problem.id
1.35
1.36 - | Substitute of Selem.sube
1.37 + | Substitute of Subst.tyty
1.38 | Tac of string
1.39 | Take of TermC.as_string | Take_Inst of TermC.as_string
1.40 val input_to_string : input -> string
1.41 @@ -167,7 +167,7 @@
1.42
1.43 | Derive of Rule_Set.id (* WN0509 drop *)
1.44 | Detail_Set of Rule_Set.id (* WN0509 drop *)
1.45 - | Detail_Set_Inst of Selem.subs * Rule_Set.id (* WN0509 drop *)
1.46 + | Detail_Set_Inst of Subst.input * Rule_Set.id (* WN0509 drop *)
1.47 | End_Detail (* WN0509 drop *)
1.48
1.49 | Empty_Tac
1.50 @@ -184,16 +184,16 @@
1.51 (where user-views can show both or only one of (thmID, thm)),
1.52 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.53 | Rewrite of ThmC.T
1.54 - | Rewrite_Inst of Selem.subs * ThmC.T
1.55 + | Rewrite_Inst of Subst.input * ThmC.T
1.56 | Rewrite_Set of Rule_Set.id
1.57 - | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
1.58 + | Rewrite_Set_Inst of Subst.input * Rule_Set.id
1.59
1.60 | Specify_Method of Method.id
1.61 | Specify_Problem of Problem.id
1.62 | Specify_Theory of ThyC.id
1.63 | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
1.64
1.65 - | Substitute of Selem.sube
1.66 + | Substitute of Subst.tyty
1.67 | Tac of string (* WN0509 drop *)
1.68 | Take of TermC.as_string | Take_Inst of TermC.as_string
1.69
1.70 @@ -227,8 +227,8 @@
1.71 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.72 | End_Detail => "End_Detail"
1.73 | Derive rls' => "Derive " ^ rls'
1.74 - | Calculate op_ => "Calculate " ^ op_
1.75 - | Substitute sube => "Substitute " ^ Selem.sube2str sube
1.76 + | Calculate op_ => "Calculate " ^ op_
1.77 + | Substitute sube => "Substitute " ^ Subst.tyty_to_string sube
1.78 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
1.79
1.80 | Take cterm' => "Take " ^ quote cterm'
1.81 @@ -314,10 +314,10 @@
1.82 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
1.83 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
1.84 | rule2tac _ subst (Rule.Thm thm'') =
1.85 - Rewrite_Inst (Selem.subst2subs subst, thm'')
1.86 + Rewrite_Inst (Subst.T_to_input subst, thm'')
1.87 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
1.88 | rule2tac _ subst (Rule.Rls_ rls) =
1.89 - Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id rls))
1.90 + Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
1.91 | rule2tac _ _ rule =
1.92 error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
1.93
1.94 @@ -402,7 +402,7 @@
1.95 | Substitute' of
1.96 Rule_Def.rew_ord_ * (* for re-calculation *)
1.97 Rule_Set.T * (* for re-calculation *)
1.98 - Selem.subte * (* the 'substitution': terms of type bool *)
1.99 + Subst.as_equality * (* the 'substitution': terms of type bool *)
1.100 term * (* to be substituted into *)
1.101 term (* resulting from the substitution *)
1.102 | Tac_ of theory * string * string * string
1.103 @@ -466,22 +466,22 @@
1.104 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
1.105
1.106 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
1.107 - | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
1.108 + | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
1.109
1.110 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
1.111 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
1.112
1.113 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
1.114 - Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
1.115 + Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
1.116 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
1.117 - Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
1.118 + Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
1.119
1.120 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
1.121 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
1.122
1.123 | input_from_T (Or_to_List' _) = Or_to_List
1.124 | input_from_T (Take' term) = Take (UnparseC.term term)
1.125 - | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
1.126 + | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_tyty subte)
1.127 | input_from_T (Tac_ (_, _, id, _)) = Tac id
1.128
1.129 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)