1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 19:20:05 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat Apr 04 12:11:32 2020 +0200
1.3 @@ -26,9 +26,9 @@
1.4 | Check_elementwise' of term * Rule.cterm' * Selem.result
1.5 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.6
1.7 - | Derive' of Rule.rls
1.8 - | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.9 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.10 + | Derive' of Rule_Set.rls
1.11 + | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.12 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.13 | End_Detail' of Selem.result
1.14
1.15 | Empty_Tac_
1.16 @@ -40,10 +40,10 @@
1.17 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.18 | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
1.19
1.20 - | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.21 - | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.22 - | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.23 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.24 + | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
1.25 + | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.26 + | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.27 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.28
1.29 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.30 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
1.31 @@ -55,7 +55,7 @@
1.32 (*Istate.T * ? *)
1.33 Proof.context * (* derived from prog. in ??? *)
1.34 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
1.35 - | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
1.36 + | Substitute' of Rule_Def.rew_ord_ * Rule_Set.rls * Selem.subte * term * term
1.37 | Tac_ of theory * string * string * string
1.38 | Take' of term
1.39 val string_of: T -> string
1.40 @@ -77,9 +77,9 @@
1.41 | Check_elementwise of Rule.cterm'
1.42 | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.43
1.44 - | Derive of Rule.rls'
1.45 - | Detail_Set of Rule.rls'
1.46 - | Detail_Set_Inst of Selem.subs * Rule.rls'
1.47 + | Derive of Rule_Set.rls'
1.48 + | Detail_Set of Rule_Set.rls'
1.49 + | Detail_Set_Inst of Selem.subs * Rule_Set.rls'
1.50 | End_Detail
1.51
1.52 | Empty_Tac
1.53 @@ -93,8 +93,8 @@
1.54
1.55 | Rewrite of Celem.thm''
1.56 | Rewrite_Inst of Selem.subs * Celem.thm''
1.57 - | Rewrite_Set of Rule.rls'
1.58 - | Rewrite_Set_Inst of Selem.subs * Rule.rls'
1.59 + | Rewrite_Set of Rule_Set.rls'
1.60 + | Rewrite_Set_Inst of Selem.subs * Rule_Set.rls'
1.61
1.62 | Specify_Method of Celem.metID
1.63 | Specify_Problem of Celem.pblID
1.64 @@ -111,7 +111,7 @@
1.65 val eq_tac : input * input -> bool
1.66 val is_rewtac : input -> bool
1.67 val is_rewset : input -> bool
1.68 - val rls_of : input -> Rule.rls'
1.69 + val rls_of : input -> Rule_Set.rls'
1.70 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
1.71 val input_from_T : T -> input
1.72 val result : T -> term
1.73 @@ -165,9 +165,9 @@
1.74 | Check_elementwise of Rule.cterm'
1.75 | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
1.76
1.77 - | Derive of Rule.rls' (* WN0509 drop *)
1.78 - | Detail_Set of Rule.rls' (* WN0509 drop *)
1.79 - | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
1.80 + | Derive of Rule_Set.rls' (* WN0509 drop *)
1.81 + | Detail_Set of Rule_Set.rls' (* WN0509 drop *)
1.82 + | Detail_Set_Inst of Selem.subs * Rule_Set.rls' (* WN0509 drop *)
1.83 | End_Detail (* WN0509 drop *)
1.84
1.85 | Empty_Tac
1.86 @@ -185,8 +185,8 @@
1.87 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.88 | Rewrite of Celem.thm''
1.89 | Rewrite_Inst of Selem.subs * Celem.thm''
1.90 - | Rewrite_Set of Rule.rls'
1.91 - | Rewrite_Set_Inst of Selem.subs * Rule.rls'
1.92 + | Rewrite_Set of Rule_Set.rls'
1.93 + | Rewrite_Set_Inst of Selem.subs * Rule_Set.rls'
1.94
1.95 | Specify_Method of Celem.metID
1.96 | Specify_Problem of Celem.pblID
1.97 @@ -315,11 +315,11 @@
1.98 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
1.99 | rule2tac _ subst (Rule.Thm thm'') =
1.100 Rewrite_Inst (Selem.subst2subs subst, thm'')
1.101 - | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule.id_rls rls)
1.102 + | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id_rls rls)
1.103 | rule2tac _ subst (Rule.Rls_ rls) =
1.104 - Rewrite_Set_Inst (Selem.subst2subs subst, (Rule.id_rls rls))
1.105 + Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id_rls rls))
1.106 | rule2tac _ _ rule =
1.107 - error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
1.108 + error ("rule2tac: called with \"" ^ Rule_Set.rule2str rule ^ "\"");
1.109
1.110 (* tactics for for internal use, compare "input" for user at the front-end.
1.111 tac_ contains results from check in 'fun applicable_in'.
1.112 @@ -360,9 +360,9 @@
1.113 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.114 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.115
1.116 - | Derive' of Rule.rls
1.117 - | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.118 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.119 + | Derive' of Rule_Set.rls
1.120 + | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.121 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.122 | End_Detail' of Selem.result
1.123
1.124 | Empty_Tac_
1.125 @@ -381,10 +381,10 @@
1.126 Rule.domID * (* from new pbt?! filled in specify *)
1.127 Celem.metID * (* from new pbt?! filled in specify *)
1.128 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.129 - | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
1.130 - | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.131 - | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
1.132 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
1.133 + | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
1.134 + | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.135 + | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.136 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.137
1.138 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.139 | Specify_Problem' of Celem.pblID *
1.140 @@ -400,8 +400,8 @@
1.141 Proof.context * (* for specify-phase *)
1.142 term (* Subproblem (thyID, pbl) OR cascmd *)
1.143 | Substitute' of
1.144 - Rule.rew_ord_ * (* for re-calculation *)
1.145 - Rule.rls * (* for re-calculation *)
1.146 + Rule_Def.rew_ord_ * (* for re-calculation *)
1.147 + Rule_Set.rls * (* for re-calculation *)
1.148 Selem.subte * (* the 'substitution': terms of type bool *)
1.149 term * (* to be substituted into *)
1.150 term (* resulting from the substitution *)
1.151 @@ -437,12 +437,12 @@
1.152 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
1.153 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.154 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.155 - "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
1.156 + "," ^ Rule_Set.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
1.157 | End_Detail' _ => "End_Detail' xxx"
1.158 | Detail_Set' _ => "Detail_Set' xxx"
1.159 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.160
1.161 - | Derive' rls => "Derive' " ^ Rule.id_rls rls
1.162 + | Derive' rls => "Derive' " ^ Rule_Set.id_rls rls
1.163 | Calculate' _ => "Calculate' "
1.164 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
1.165
1.166 @@ -468,13 +468,13 @@
1.167 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
1.168 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
1.169
1.170 - | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule.id_rls rls)
1.171 - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule.id_rls rls)
1.172 + | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id_rls rls)
1.173 + | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id_rls rls)
1.174
1.175 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
1.176 - Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
1.177 + Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
1.178 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
1.179 - Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
1.180 + Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
1.181
1.182 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
1.183 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred