52 while stepwise construction of solutions is called solving. |
52 while stepwise construction of solutions is called solving. |
53 The latter is supported by Lucas-Interpretation of the functions' body. |
53 The latter is supported by Lucas-Interpretation of the functions' body. |
54 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem; |
54 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem; |
55 it is as complete as possible (this has been different up to now). |
55 it is as complete as possible (this has been different up to now). |
56 (4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input. |
56 (4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input. |
|
57 (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName, |
|
58 add them to the model-pattern of met and let this input be done automatically; |
|
59 respective items must be in fmz. |
57 #1# fmz contains items, which are stored in oris of the root(!)-problem. |
60 #1# fmz contains items, which are stored in oris of the root(!)-problem. |
58 This allows to specify methods, which require more input as anticipated |
61 This allows to specify methods, which require more input as anticipated |
59 in writing partial_functions: such an item can be fetched from the root-problem's oris. |
62 in writing partial_functions: such an item can be fetched from the root-problem's oris. |
60 A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically |
63 A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically |
61 and thus is solved numerically. |
64 and thus is solved numerically. |
118 val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori |
121 val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori |
119 datatype additm = Add of Model.itm | Err of string |
122 datatype additm = Add of Model.itm | Err of string |
120 val appl_add: Proof.context -> string -> Model.ori list -> |
123 val appl_add: Proof.context -> string -> Model.ori list -> |
121 Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm |
124 Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm |
122 val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option |
125 val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option |
|
126 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list |
123 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
127 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
124 |
128 |
125 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*) |
129 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*) |
126 val variants_in : term list -> int |
130 val variants_in : term list -> int |
127 val is_untouched : Model.itm -> bool |
131 val is_untouched : Model.itm -> bool |
458 (* is the term t input (or taken from fmz) known in oris ? |
462 (* is the term t input (or taken from fmz) known in oris ? |
459 give feedback on all(?) strange input; |
463 give feedback on all(?) strange input; |
460 return _all_ terms already input to this item (e.g. valuesFor a,b) *) |
464 return _all_ terms already input to this item (e.g. valuesFor a,b) *) |
461 fun is_known ctxt sel ori t = |
465 fun is_known ctxt sel ori t = |
462 let |
466 let |
463 val _ = tracing ("RM is_known: t=" ^ Rule.term2str t) |
|
464 val ots = (distinct o flat o (map #5)) ori |
467 val ots = (distinct o flat o (map #5)) ori |
465 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots |
468 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots |
466 val (d, ts) = Model.split_dts t |
469 val (d, ts) = Model.split_dts t |
467 val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts) |
470 val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts) |
468 in |
471 in |