1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 11:36:13 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 12:13:20 2020 +0200
1.3 @@ -4,7 +4,7 @@
1.4
1.5 regular expression for search:
1.6
1.7 -Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
1.8 +Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
1.9
1.10 *)
1.11 signature TACTIC =
1.12 @@ -25,10 +25,9 @@
1.13 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.14 | Check_Postcond' of Problem.id * term
1.15 | Check_elementwise' of term * TermC.as_string * Selem.result
1.16 -(*RM*)| Derive' of Rule_Set.T
1.17 + | Derive' of Rule_Set.T
1.18 | Empty_Tac_
1.19 | Free_Solve'
1.20 -(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
1.21 | Or_to_List' of term * term
1.22 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.23 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
1.24 @@ -60,10 +59,9 @@
1.25 | Calculate of string
1.26 | Check_Postcond of Problem.id
1.27 | Check_elementwise of TermC.as_string
1.28 -(*RM*)| Derive of Rule_Set.id(*RM*)
1.29 + | Derive of Rule_Set.id
1.30 | Empty_Tac
1.31 -(*RM*)| Free_Solve
1.32 -(*RM*)| Apply_Assumption of TermC.as_string list
1.33 + | Free_Solve
1.34 | Or_to_List
1.35 | Rewrite of ThmC.T
1.36 | Rewrite_Inst of Subst.input * ThmC.T
1.37 @@ -127,10 +125,9 @@
1.38 | Calculate of string
1.39 | Check_Postcond of Problem.id
1.40 | Check_elementwise of TermC.as_string
1.41 -(*RM*)| Derive of Rule_Set.id
1.42 + | Derive of Rule_Set.id
1.43 | Empty_Tac
1.44 -(*RM*)| Free_Solve
1.45 -(*RM*)| Apply_Assumption of TermC.as_string list
1.46 + | Free_Solve
1.47 | Or_to_List
1.48 | Rewrite of ThmC.T
1.49 | Rewrite_Inst of Subst.input * ThmC.T
1.50 @@ -169,22 +166,19 @@
1.51 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
1.52 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
1.53 | End_Detail => "End_Detail"
1.54 - | Derive rls' => "Derive " ^ rls'
1.55 + | Derive rls' => "Derive " ^ rls'
1.56 | Calculate op_ => "Calculate " ^ op_
1.57 | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
1.58 - | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
1.59
1.60 | Take cterm' => "Take " ^ quote cterm'
1.61 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
1.62 - | End_Subproblem => "End_Subproblem"
1.63 | CAScmd cterm' => "CAScmd " ^ quote cterm'
1.64
1.65 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
1.66 | Or_to_List => "Or_to_List "
1.67 - | Collect_Trues => "Collect_Trues"
1.68
1.69 | Empty_Tac => "Empty_Tac"
1.70 - | Tac string => "Tac " ^ string
1.71 +(*RM*)| Tac string => "Tac " ^ string(*RM*)
1.72 | End_Proof' => "input End_Proof'"
1.73 | _ => "input_to_string not impl. for ?!";
1.74
1.75 @@ -213,16 +207,13 @@
1.76 | Derive _ => "Derive "
1.77 | Calculate _ => "Calculate "
1.78 | Substitute _ => "Substitute"
1.79 - | Apply_Assumption _ => "Apply_Assumption"
1.80
1.81 | Take _ => "Take"
1.82 | Subproblem _ => "Subproblem"
1.83 - | End_Subproblem => "End_Subproblem"
1.84 | CAScmd _ => "CAScmd"
1.85
1.86 | Check_elementwise _ => "Check_elementwise"
1.87 | Or_to_List => "Or_to_List "
1.88 - | Collect_Trues => "Collect_Trues"
1.89
1.90 | Empty_Tac => "Empty_Tac"
1.91 | Tac _ => "Tac "
1.92 @@ -342,7 +333,7 @@
1.93 term * (* the current formula: [x=1,x=...] *)
1.94 string * (* the pred from Check_elementwise *)
1.95 Selem.result (* composed from (1) and (2): {x. pred} *)
1.96 -(*RM*)| Derive' of Rule_Set.T
1.97 + | Derive' of Rule_Set.T(* for Generate.embed_deriv *)
1.98 | Empty_Tac_
1.99 | Free_Solve'
1.100 | Or_to_List' of term * term
1.101 @@ -365,8 +356,9 @@
1.102 term (* resulting from the substitution *)
1.103 (*RM*)| Tac_ of theory * string * string * string
1.104 | Take' of term
1.105 - | End_Detail' of Selem.result
1.106 - | Begin_Trans' of term | End_Trans' of Selem.result
1.107 + | End_Detail' of Selem.result (* for intermediate steps into Rewrite_Set *)
1.108 + | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *)
1.109 + | End_Trans' of Selem.result (* for intermediate steps into Rewrite_Set *)
1.110 | End_Proof''
1.111
1.112 fun string_of ma = case ma of