1 (* Title: BaseDefinitions/rule-def.sml
3 (c) due to copyright terms
5 Here is a minimum of code required for Know_Store.thy.
6 For main code see structure Rule.
8 signature RULE_DEFINITION =
13 type rew_ord' = string
14 type rew_ord_ = (term * term) list -> term * term -> bool
15 type rew_ord = rew_ord' * rew_ord_
16 type eval_fn = string -> term -> theory -> (string * term) option
20 | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
21 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
22 | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
23 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
24 | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
25 prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
26 and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule
27 | Rls_ of rule_set | Thm of string * thm
32 {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
33 init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
34 locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
35 next_rule: rule list list -> term -> rule option, normal_form: term ->
36 (term * term list) option}
40 structure Rule_Def(**): RULE_DEFINITION(**) =
44 type eval_fn = string -> term -> theory -> (string * term) option;
46 type rew_ord' = string;
47 type rew_ord_ = (term * term) list -> term * term -> bool;
48 type rew_ord = rew_ord' * rew_ord_;
51 type cal = calID * eval_fn;
52 type prog_calcID = string;
53 type calc = (prog_calcID * cal);
55 (* error patterns and fill patterns *)
56 type errpatID = string
58 (* all these different data justify a step in a calculation *)
60 Erule (* the empty rule *)
61 | Thm of (* theorem associated with the identifier for reflection *)
62 string * (* needless since Thm.get_name_hint *)
63 Thm.thm (* see TODO CLEANUP Thm *)
64 | Eval of (* evaluation by rewriting *)
65 string * (* unique identifier for the evaluation function *)
66 eval_fn (* evaluation function in ML code *)
67 | Cal1 of string * (* applied once to whole term or lhs/rhs of an eqality *)
68 eval_fn (* evaluation function in ML code *)
69 | Rls_ of rule_set (* rule sets may be nested *)
70 and program = (* program for Lucas-Interpretation *)
71 Empty_Prog (* DEPRECATED: needless after removal of Rfuns *)
72 | Prog of term (* Lucas-Interpretation works on Isabelle's terms *)
73 | Rfuns of (* DEPRECATED, replaced by Auto_Prog *)
74 {init_state : (* initialise for reverse rewriting by the Interpreter *)
75 term -> (* for this the rrlsstate is initialised: *)
76 term * (* the current formula via istate *)
77 term * (* the final formula *)
78 rule list (* of reverse rewrite set (#1#) *)
79 list * (* may be serveral, eg. in norm_rational *)
80 ( rule * (* Thm (+ Thm generated from Eval) resulting in ... *)
81 (term * (* ... rewrite with ... *)
82 term list)) (* ... assumptions *)
83 list, (* derivation from given term to normalform in reverse order *)
84 normal_form: (* the function which drives the Rrls *)
85 term -> (term * term list) option,
86 locate_rule: (* checks a rule R for being a cancel-rule *)
87 rule list list -> (* the reverse rule list *)
88 term -> (* ... to which the rule shall be applied *)
89 rule -> (* ... to be applied to term *)
90 ( rule * (* value: a rule rewriting to ... *)
91 (term * (* ... the resulting term ... *)
92 term list)) (* ... with the assumptions ( //#0) *)
93 list, (* there may be several such rules *)
94 next_rule: (* for a given term return the next rules to be done for cancel *)
95 rule list list->(* the reverse rule list *)
96 term -> (* the term for which ... *)
97 rule option, (* ... this rule is appropriate for cancellation *)
98 attach_form: (* checks an input term TI, if it may belong to a current cancel*)
100 term -> (* TG, the last one agreed upon by user + math-eng *)
101 term -> (* TI, the next one input by the user *)
102 ( rule * (* the rule to be applied in order to reach TI *)
103 (term * (* ... obtained by applying the rule ... *)
104 term list)) (* ... and the respective assumptions *)
105 list} (* there may be several such rules; the list is empty, if ... *)
106 and rule_set = (* a collection for ordered & conditional rewriting *)
107 Empty (* empty Rule_Set.T *)
108 | Repeat of (*a confluent and terminating ruleset, in principle *)
109 {id: string, (* for trace_rewrite *)
110 preconds: term list, (* STILL UNUSED *)
111 rew_ord: rew_ord,(* for rules *)
112 erls: rule_set, (* for the conditions in rules *)
113 srls: rule_set, (* for evaluation of Prog_Expr *)
114 calc: calc list, (* for Calculate in program, set by prep_rls' *)
116 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *)
117 scr: program} (* DEPRECATED: intersteps are created on the fly now *)
118 | Sequence of (* a sequence of rules to be tried only once *)
119 {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
120 calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
121 | Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
122 {id: string, (* for trace_rewrite *)
123 prepat: (* a guard which guarantees a redex *)
124 (term list * (* preconds, eval with subst from pattern below *)
125 term) (* pattern matched with current (sub)term *)
126 list, (* meta-conjunction in guarding is or *)
127 rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}