1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri May 01 16:06:59 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri May 01 17:17:41 2020 +0200
1.3 @@ -13,41 +13,28 @@
1.4 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
1.5 | Add_Relation' of TermC.as_string * Model.itm list
1.6 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
1.7 -
1.8 - | Begin_Sequ' | Begin_Trans' of term
1.9 - | Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.10 - | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.11 - | End_Sequ' | End_Trans' of Selem.result
1.12 - | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.13 -
1.14 + | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.15 + | Init_Proof' of TermC.as_string list * Spec.T
1.16 + | Model_Problem' of Problem.id * Model.itm list * Model.itm list
1.17 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.18 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
1.19 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.20 + | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
1.21 + | Specify_Theory' of ThyC.id
1.22 + (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.23 | CAScmd' of term
1.24 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.25 | Check_Postcond' of Problem.id * term
1.26 | Check_elementwise' of term * TermC.as_string * Selem.result
1.27 - | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.28 -
1.29 - | Derive' of Rule_Set.T
1.30 - | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.31 - | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.32 - | End_Detail' of Selem.result
1.33 -
1.34 +(*RM*)| Derive' of Rule_Set.T
1.35 | Empty_Tac_
1.36 | Free_Solve'
1.37 -
1.38 - | Init_Proof' of TermC.as_string list * Spec.T
1.39 - | Model_Problem' of Problem.id * Model.itm list * Model.itm list
1.40 +(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
1.41 | Or_to_List' of term * term
1.42 - | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
1.43 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
1.44 -
1.45 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.46 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.47 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.48 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.49 -
1.50 - | Specify_Method' of Method.id * Model.ori list * Model.itm list
1.51 - | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
1.52 - | Specify_Theory' of ThyC.id
1.53 | Subproblem' of
1.54 Spec.T * Model.ori list *
1.55 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
1.56 @@ -56,54 +43,61 @@
1.57 Proof.context * (* derived from prog. in ??? *)
1.58 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
1.59 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
1.60 - | Tac_ of theory * string * string * string
1.61 +(*RM*)| Tac_ of theory * string * string * string
1.62 | Take' of term
1.63 +(*RM* )| Take_Inst of TermC.as_string( *RM*)
1.64 +(*RM*)| Begin_Sequ' | Begin_Trans' of term
1.65 +(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
1.66 +(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
1.67 +(*RM*)| End_Sequ' | End_Trans' of Selem.result
1.68 +(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.69 +(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
1.70 +(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
1.71 +(*RM*)| End_Detail' of Selem.result;
1.72 +
1.73 val string_of: T -> string
1.74
1.75 datatype input =
1.76 - Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.77 - | Apply_Assumption of TermC.as_string list
1.78 + Add_Find of TermC.as_string | Add_Given of TermC.as_string
1.79 + | Add_Relation of TermC.as_string
1.80 | Apply_Method of Method.id
1.81 - (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
1.82 - | Begin_Sequ | Begin_Trans
1.83 - | Split_And | Split_Or | Split_Intersect
1.84 - | Conclude_And | Conclude_Or | Collect_Trues
1.85 - | End_Sequ | End_Trans
1.86 - | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
1.87 - (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.88 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.89 + | Init_Proof of TermC.as_string list * Spec.T
1.90 + | Model_Problem
1.91 + | Refine_Problem of Problem.id
1.92 + | Refine_Tacitly of Problem.id
1.93 + | Specify_Method of Method.id
1.94 + | Specify_Problem of Problem.id
1.95 + | Specify_Theory of ThyC.id
1.96 + (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.97 | CAScmd of TermC.as_string
1.98 | Calculate of string
1.99 | Check_Postcond of Problem.id
1.100 | Check_elementwise of TermC.as_string
1.101 - | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
1.102 -
1.103 - | Derive of Rule_Set.id
1.104 - | Detail_Set of Rule_Set.id
1.105 - | Detail_Set_Inst of Subst.input * Rule_Set.id
1.106 - | End_Detail
1.107 -
1.108 +(*RM*)| Derive of Rule_Set.id(*RM*)
1.109 | Empty_Tac
1.110 - | Free_Solve
1.111 -
1.112 - | Init_Proof of TermC.as_string list * Spec.T
1.113 - | Model_Problem
1.114 +(*RM*)| Free_Solve
1.115 +(*RM*)| Apply_Assumption of TermC.as_string list
1.116 | Or_to_List
1.117 - | Refine_Problem of Problem.id
1.118 - | Refine_Tacitly of Problem.id
1.119 -
1.120 | Rewrite of ThmC.T
1.121 | Rewrite_Inst of Subst.input * ThmC.T
1.122 | Rewrite_Set of Rule_Set.id
1.123 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
1.124 + | Subproblem of ThyC.id * Problem.id
1.125 + | Substitute of Subst.input
1.126 +(*RM*)| Tac of string
1.127 + | Take of TermC.as_string
1.128 +(*RM*)| Take_Inst of TermC.as_string
1.129 +(*RM*)| Begin_Sequ | Begin_Trans
1.130 +(*RM*)| Split_And | Split_Or | Split_Intersect
1.131 +(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
1.132 +(*RM*)| End_Sequ | End_Trans
1.133 +(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
1.134 +(*RM*)| Detail_Set of Rule_Set.id
1.135 +(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
1.136 +(*RM*)| End_Detail
1.137 + | End_Proof';
1.138
1.139 - | Specify_Method of Method.id
1.140 - | Specify_Problem of Problem.id
1.141 - | Specify_Theory of ThyC.id
1.142 - | Subproblem of ThyC.id * Problem.id
1.143 -
1.144 - | Substitute of Subst.input
1.145 - | Tac of string
1.146 - | Take of TermC.as_string | Take_Inst of TermC.as_string
1.147 val input_to_string : input -> string
1.148 val tac2IDstr : input -> string
1.149 val is_empty : input -> bool