neuper@37906
|
1 |
(* tools for rewriting, reverse rewriting, context to thy concerning rewriting
|
neuper@37906
|
2 |
authors: Walther Neuper 2002, 2006
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
|
wneuper@59263
|
6 |
signature REWRITE_TOOLS =
|
wneuper@59263
|
7 |
sig
|
wneuper@59263
|
8 |
type deriv
|
wneuper@59405
|
9 |
val contains_rule : Celem.rule -> Celem.rls -> bool
|
wneuper@59405
|
10 |
val atomic_appl_tacs : theory -> string -> Celem.rls -> term -> Tac.tac -> Tac.tac list
|
wneuper@59405
|
11 |
val thy_containing_rls : Celem.theory' -> Celem.rls' -> string * Celem.theory'
|
wneuper@59405
|
12 |
val thy_containing_cal : Celem.theory' -> Celem.prog_calcID -> string * string
|
wneuper@59263
|
13 |
datatype contthy
|
wneuper@59405
|
14 |
= ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: Celem.thyID}
|
wneuper@59405
|
15 |
| ContNOrewInst of {applto: term, bdvs: Celem.subst, thm_rls: Celem.guh, thminst: term, thyID: Celem.thyID}
|
wneuper@59405
|
16 |
| ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: Celem.thyID}
|
wneuper@59405
|
17 |
| ContRlsInst of {applto: term, asms: term list, bdvs: Celem.subst, result: term, rls: Celem.guh, thyID: Celem.thyID}
|
wneuper@59405
|
18 |
| ContThm of {applat: term, applto: term, asmrls: Celem.rls', asms: (term * term) list,
|
wneuper@59405
|
19 |
lhs: term * term, resasms: term list, result: term, reword: Celem.rew_ord', rhs: term * term,
|
wneuper@59405
|
20 |
thm: Celem.guh, thyID: Celem.thyID}
|
wneuper@59405
|
21 |
| ContThmInst of {applat: term, applto: term, asmrls: Celem.rls', asms: (term * term) list,
|
wneuper@59405
|
22 |
bdvs: Celem.subst, lhs: term * term, resasms: term list, result: term, reword: Celem.rew_ord',
|
wneuper@59405
|
23 |
rhs: term * term, thm: Celem.guh, thminst: term, thyID: Celem.thyID}
|
wneuper@59263
|
24 |
| EContThy
|
wneuper@59405
|
25 |
val guh2filename : Celem.guh -> Celem.filename
|
wneuper@59405
|
26 |
val is_sym : Celem.thmID -> bool
|
wneuper@59405
|
27 |
val sym_drop : Celem.thmID -> Celem.thmID
|
wneuper@59405
|
28 |
val sym_rls : Celem.rls -> Celem.rls
|
wneuper@59405
|
29 |
val sym_rule : Celem.rule -> Celem.rule
|
wneuper@59405
|
30 |
val thms_of_rls : Celem.rls -> Celem.rule list
|
wneuper@59405
|
31 |
val theID2filename : Celem.theID -> Celem.filename
|
wneuper@59405
|
32 |
val no_thycontext : Celem.guh -> bool
|
wneuper@59405
|
33 |
val subs_from : Selem.istate -> 'a -> Celem.guh -> Selem.subs
|
wneuper@59405
|
34 |
val guh2rewtac : Celem.guh -> Selem.subs -> Tac.tac
|
wneuper@59302
|
35 |
val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Tac.tac
|
wneuper@59302
|
36 |
val context_thy : Ctree.state -> Tac.tac -> contthy
|
wneuper@59405
|
37 |
val distinct_Thm : Celem.rule list -> Celem.rule list
|
wneuper@59405
|
38 |
val eq_Thms : string list -> Celem.rule -> bool
|
wneuper@59405
|
39 |
val make_deriv : theory -> Celem.rls -> Celem.rule list -> ((term * term) list -> term * term -> bool) ->
|
wneuper@59263
|
40 |
term option -> term -> deriv
|
wneuper@59405
|
41 |
val reverse_deriv : theory -> Celem.rls -> Celem.rule list -> ((term * term) list -> term * term -> bool) ->
|
wneuper@59405
|
42 |
term option -> term -> (Celem.rule * (term * term list)) list
|
wneuper@59405
|
43 |
val get_bdv_subst : term -> (term * term) list -> Selem.subs option * Celem.subst
|
wneuper@59313
|
44 |
val thy_containing_thm : string -> string * string
|
wneuper@59405
|
45 |
val guh2theID : Celem.guh -> Celem.theID
|
wneuper@59310
|
46 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59310
|
47 |
(* NONE *)
|
wneuper@59299
|
48 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59263
|
49 |
val trtas2str : (term * rule * (term * term list)) list -> string
|
wneuper@59263
|
50 |
val eq_Thm : rule * rule -> bool
|
wneuper@59263
|
51 |
val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string
|
wneuper@59299
|
52 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59310
|
53 |
|
wneuper@59310
|
54 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59405
|
55 |
val deri2str : (Celem.rule * (term * term list)) list -> string
|
wneuper@59313
|
56 |
val sym_trm : term -> term
|
wneuper@59263
|
57 |
end
|
neuper@37906
|
58 |
|
wneuper@59263
|
59 |
structure Rtools(**): REWRITE_TOOLS(**) =
|
wneuper@59263
|
60 |
struct
|
wneuper@59313
|
61 |
|
wneuper@59263
|
62 |
(*** reverse rewriting ***)
|
wneuper@59266
|
63 |
(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
|
wneuper@59266
|
64 |
* of for connecting a user-input formula with the current calc-state. *
|
wneuper@59266
|
65 |
*# It is somewhat incompatible with the rest of the math-engine: *
|
wneuper@59266
|
66 |
* (1) it is not created by a script *
|
wneuper@59266
|
67 |
* (2) thus there cannot be another user-input within a derivation *
|
wneuper@59266
|
68 |
*# It suffers particularily from the not-well-foundedness of the math-engine*
|
wneuper@59266
|
69 |
* (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
|
wneuper@59266
|
70 |
* (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
|
wneuper@59266
|
71 |
* (3) FIXME and eventually 'lev_back' *
|
wneuper@59266
|
72 |
*# SOME improvements are evident FIXME.040215 '_deriv'ation: *
|
wneuper@59266
|
73 |
* (1) FIXME nest Rls_ in 'make_deriv' *
|
wneuper@59266
|
74 |
* (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
|
wneuper@59266
|
75 |
* user-input will become possible in this part of a derivation *
|
wneuper@59266
|
76 |
* (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
|
wneuper@59266
|
77 |
* while a non-derivable inform requires to step until End_Proof' *
|
wneuper@59266
|
78 |
* (4) FIXME find criteria on when _not_ to step until End_Proof' *
|
wneuper@59266
|
79 |
* (5) FIXME
|
wneuper@59266
|
80 |
.*)
|
wneuper@59263
|
81 |
type deriv = (* derivation for insertin one level of nodes into the calctree *)
|
wneuper@59263
|
82 |
( term * (* where the rule is applied to *)
|
wneuper@59405
|
83 |
Celem.rule * (* rule to be applied *)
|
wneuper@59263
|
84 |
( term * (* resulting from rule application *)
|
wneuper@59263
|
85 |
term list)) (* assumptions resulting from rule application *)
|
wneuper@59263
|
86 |
list (* *)
|
neuper@37906
|
87 |
|
wneuper@59263
|
88 |
fun trta2str (t, r, (t', a)) =
|
wneuper@59405
|
89 |
"\n(" ^ Celem.term2str t ^ ", " ^ Celem.rule2str' r ^ ", (" ^ Celem.term2str t' ^ ", " ^ Celem.terms2str a ^ "))"
|
wneuper@59263
|
90 |
fun trtas2str trtas = (strs2str o (map trta2str)) trtas
|
wneuper@59263
|
91 |
val deriv2str = trtas2str
|
wneuper@59263
|
92 |
fun rta2str (r, (t, a)) =
|
wneuper@59405
|
93 |
"\n(" ^ Celem.rule2str' r ^ ", (" ^ Celem.term2str t ^ ", " ^ Celem.terms2str a ^ "))"
|
wneuper@59263
|
94 |
fun rtas2str rtas = (strs2str o (map rta2str)) rtas
|
wneuper@59263
|
95 |
val deri2str = rtas2str
|
neuper@37906
|
96 |
|
wneuper@59263
|
97 |
(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs)
|
neuper@42399
|
98 |
WN120320: reconsider the desing including the java front-end with html representation;
|
neuper@42399
|
99 |
see tests
|
neuper@42399
|
100 |
--- OLD compute rlsthmsNOTisac by eq_thmID ---
|
neuper@42399
|
101 |
--- compute val rlsthmsNOTisac ---
|
neuper@42399
|
102 |
*)
|
neuper@37906
|
103 |
fun sym_thm thm =
|
wneuper@59263
|
104 |
let
|
wneuper@59263
|
105 |
val (deriv,
|
wneuper@59338
|
106 |
{cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs,
|
wneuper@59263
|
107 |
prop = prop}) = Thm.rep_thm_G thm
|
wneuper@59390
|
108 |
val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
|
wneuper@59389
|
109 |
val prop' = case TermC.strip_imp_prems' prop of
|
wneuper@59390
|
110 |
NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
|
wneuper@59390
|
111 |
| SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
|
wneuper@59338
|
112 |
in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end
|
neuper@37906
|
113 |
|
wneuper@59263
|
114 |
(* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
|
neuper@38002
|
115 |
fun sym_trm trm =
|
wneuper@59263
|
116 |
let
|
wneuper@59390
|
117 |
val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) trm
|
wneuper@59389
|
118 |
val trm' = case TermC.strip_imp_prems' trm of
|
wneuper@59389
|
119 |
NONE => TermC.mk_equality (rhs, lhs)
|
wneuper@59389
|
120 |
| SOME cs => TermC.ins_concl cs (TermC.mk_equality (rhs, lhs))
|
wneuper@59263
|
121 |
in trm' end
|
neuper@37906
|
122 |
|
neuper@55487
|
123 |
(* derive normalform of a rls, or derive until SOME goal,
|
neuper@37906
|
124 |
and record rules applied and rewrites.
|
neuper@37906
|
125 |
val it = fn
|
neuper@37906
|
126 |
: theory
|
neuper@37906
|
127 |
-> rls
|
neuper@37906
|
128 |
-> rule list
|
neuper@37906
|
129 |
-> rew_ord : the order of this rls, which 1 theorem of is used
|
neuper@37906
|
130 |
for rewriting 1 single step (?14.4.03)
|
neuper@55487
|
131 |
-> term option : 040214 ??? use for "derive until SOME goal" ???
|
neuper@37906
|
132 |
-> term
|
neuper@37906
|
133 |
-> (term * : to this term ...
|
neuper@37906
|
134 |
rule * : ... this rule is applied yielding ...
|
neuper@37906
|
135 |
(term * : ... this term ...
|
neuper@37906
|
136 |
term list)) : ... under these assumptions.
|
neuper@37906
|
137 |
list :
|
neuper@37906
|
138 |
returns empty list for a normal form
|
neuper@37906
|
139 |
FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
|
neuper@37906
|
140 |
|
neuper@37906
|
141 |
WN060825 too complicated for the intended use by cancel_, common_nominator_
|
neuper@55487
|
142 |
and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
|
neuper@55487
|
143 |
-- replaced below *)
|
wneuper@59405
|
144 |
fun make_deriv thy erls rs ro goal tt =
|
neuper@55487
|
145 |
let
|
wneuper@59263
|
146 |
datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
|
wneuper@59263
|
147 |
fun rew_once _ rts t Noap [] =
|
wneuper@59405
|
148 |
(case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ Celem.term2str t))
|
neuper@55487
|
149 |
| rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
|
neuper@55487
|
150 |
(*| Seq _ => rts) FIXXXXXME 14.3.03*)
|
neuper@55487
|
151 |
| rew_once lim rts t apno rs' =
|
neuper@55487
|
152 |
(case goal of
|
neuper@55487
|
153 |
NONE => rew_or_calc lim rts t apno rs'
|
neuper@55487
|
154 |
| SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
|
neuper@55487
|
155 |
and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
|
neuper@55487
|
156 |
if lim < 0
|
wneuper@59405
|
157 |
then (tracing ("make_deriv exceeds " ^ int2str (! Celem.lim_deriv) ^ "with deriv =\n");
|
wneuper@59263
|
158 |
tracing (deriv2str rts); rts)
|
neuper@55487
|
159 |
else
|
wneuper@59263
|
160 |
(case r of
|
wneuper@59405
|
161 |
Celem.Thm (thmid, tm) =>
|
wneuper@59405
|
162 |
(if not (! Celem.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
|
wneuper@59380
|
163 |
case Rewrite.rewrite_ thy ro erls true tm t of
|
neuper@55487
|
164 |
NONE => rew_once lim rts t apno rs'
|
neuper@55487
|
165 |
| SOME (t', a') =>
|
wneuper@59405
|
166 |
(if ! Celem.trace_rewrite then tracing ("### rewrites to: " ^ Celem.term2str t') else ();
|
neuper@55487
|
167 |
rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
|
wneuper@59405
|
168 |
| Celem.Calc (c as (op_, _)) =>
|
neuper@55487
|
169 |
let
|
wneuper@59405
|
170 |
val _ = if not (! Celem.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
|
wneuper@59389
|
171 |
val t = TermC.uminus_to_string t
|
neuper@55487
|
172 |
in
|
wneuper@59386
|
173 |
case Calc.adhoc_thm thy c t of
|
neuper@55487
|
174 |
NONE => rew_once lim rts t apno rs'
|
neuper@55487
|
175 |
| SOME (thmid, tm) =>
|
neuper@55487
|
176 |
(let
|
wneuper@59380
|
177 |
val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
|
wneuper@59263
|
178 |
SOME ta => ta
|
wneuper@59263
|
179 |
| NONE => error "adhoc_thm: NONE"
|
wneuper@59405
|
180 |
val _ = if not (! Celem.trace_rewrite) then () else tracing("### calc. to: " ^ Celem.term2str t')
|
wneuper@59405
|
181 |
val r' = Celem.Thm (thmid, tm)
|
neuper@55487
|
182 |
in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
|
neuper@55487
|
183 |
handle _ => error "derive_norm, Calc: no rewrite"
|
neuper@55487
|
184 |
end
|
neuper@55487
|
185 |
(*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)
|
wneuper@59405
|
186 |
| Celem.Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
|
wneuper@59380
|
187 |
(case Rewrite.rewrite_set_ thy true rls t of
|
wneuper@59263
|
188 |
NONE => rew_once lim rts t apno rs'
|
wneuper@59263
|
189 |
| SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
|
wneuper@59405
|
190 |
| rule => error ("rew_once: uncovered case " ^ Celem.rule2str rule))
|
wneuper@59263
|
191 |
| rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
|
wneuper@59405
|
192 |
in rew_once (! Celem.lim_deriv) [] tt Noap rs end
|
neuper@37906
|
193 |
|
wneuper@59405
|
194 |
fun sym_drop thmID =
|
wneuper@59263
|
195 |
case Symbol.explode thmID of
|
wneuper@59405
|
196 |
"s" :: "y" :: "m" :: "_" :: id => implode id
|
wneuper@59263
|
197 |
| _ => thmID
|
wneuper@59405
|
198 |
fun is_sym thmID =
|
wneuper@59263
|
199 |
case Symbol.explode thmID of
|
wneuper@59263
|
200 |
"s" :: "y" :: "m" :: "_" :: _ => true
|
wneuper@59263
|
201 |
| _ => false;
|
neuper@37906
|
202 |
|
neuper@37906
|
203 |
(*FIXXXXME.040219: detail has to handle Rls id="sym_..."
|
neuper@37906
|
204 |
by applying make_deriv, rev_deriv'; see concat_deriv*)
|
wneuper@59405
|
205 |
fun sym_rls Celem.Erls = Celem.Erls
|
wneuper@59405
|
206 |
| sym_rls (Celem.Rls {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
|
wneuper@59405
|
207 |
Celem.Rls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
|
wneuper@59263
|
208 |
rules = rules, rew_ord = rew_ord, preconds = preconds}
|
wneuper@59405
|
209 |
| sym_rls (Celem.Seq {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
|
wneuper@59405
|
210 |
Celem.Seq {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
|
wneuper@59263
|
211 |
rules = rules, rew_ord = rew_ord, preconds = preconds}
|
wneuper@59405
|
212 |
| sym_rls (Celem.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
|
wneuper@59405
|
213 |
Celem.Rrls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls,
|
wneuper@59263
|
214 |
prepat = prepat, rew_ord = rew_ord}
|
neuper@37906
|
215 |
|
neuper@55485
|
216 |
(* toggles sym_* and keeps "#:" for ad-hoc calculations *)
|
wneuper@59405
|
217 |
fun sym_rule (Celem.Thm (thmID, thm)) =
|
wneuper@59263
|
218 |
let
|
wneuper@59263
|
219 |
val thm' = sym_thm thm
|
wneuper@59263
|
220 |
val thmID' = case Symbol.explode thmID of
|
wneuper@59263
|
221 |
"s" :: "y" :: "m" :: "_" :: id => implode id
|
wneuper@59405
|
222 |
| "#" :: ":" :: _ => "#: " ^ Celem.string_of_thmI thm'
|
wneuper@59263
|
223 |
| _ => "sym_" ^ thmID
|
wneuper@59405
|
224 |
in Celem.Thm (thmID', thm') end
|
wneuper@59405
|
225 |
| sym_rule (Celem.Rls_ rls) = Celem.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
|
wneuper@59405
|
226 |
| sym_rule r = error ("sym_rule: not for " ^ Celem.rule2str r)
|
neuper@37906
|
227 |
|
neuper@37906
|
228 |
(*version for reverse rewrite used before 040214*)
|
wneuper@59263
|
229 |
fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));
|
wneuper@59405
|
230 |
fun reverse_deriv thy erls rs ro goal t =
|
wneuper@59405
|
231 |
(rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
|
neuper@37906
|
232 |
|
wneuper@59405
|
233 |
fun eq_Thm (Celem.Thm (id1, _), Celem.Thm (id2,_)) = id1 = id2
|
wneuper@59405
|
234 |
| eq_Thm (Celem.Thm (_, _), _) = false
|
wneuper@59405
|
235 |
| eq_Thm (Celem.Rls_ r1, Celem.Rls_ r2) = Celem.id_rls r1 = Celem.id_rls r2
|
wneuper@59405
|
236 |
| eq_Thm (Celem.Rls_ _, _) = false
|
wneuper@59405
|
237 |
| eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Celem.rule2str r1 ^ "' '" ^ Celem.rule2str r2 ^ "'")
|
wneuper@59263
|
238 |
fun distinct_Thm r = gen_distinct eq_Thm r
|
neuper@37906
|
239 |
|
wneuper@59405
|
240 |
fun eq_Thms thmIDs thm = (member op = thmIDs (Celem.id_of_thm thm))
|
wneuper@59263
|
241 |
handle ERROR _ => false
|
neuper@37906
|
242 |
|
neuper@42400
|
243 |
fun thy_containing_thm thmDeriv =
|
neuper@42400
|
244 |
let
|
wneuper@59405
|
245 |
val isabthys' = map Context.theory_name (Celem.isabthys ());
|
neuper@42400
|
246 |
in
|
wneuper@59405
|
247 |
if member op= isabthys' (Celem.thyID_of_derivation_name thmDeriv)
|
wneuper@59405
|
248 |
then ("Isabelle", Celem.thyID_of_derivation_name thmDeriv)
|
wneuper@59405
|
249 |
else ("IsacKnowledge", Celem.thyID_of_derivation_name thmDeriv)
|
wneuper@59263
|
250 |
end
|
neuper@37906
|
251 |
|
neuper@55457
|
252 |
(* which theory in ancestors of thy' contains a ruleset *)
|
wneuper@59405
|
253 |
fun thy_containing_rls thy' rls' =
|
neuper@55457
|
254 |
let
|
wneuper@59405
|
255 |
val thy = Celem.Thy_Info_get_theory thy'
|
neuper@55457
|
256 |
in
|
neuper@55457
|
257 |
case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
|
wneuper@59405
|
258 |
SOME (thy'', _) => (Celem.partID' thy'', thy'')
|
neuper@55457
|
259 |
| _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
|
neuper@55457
|
260 |
end
|
neuper@37906
|
261 |
|
neuper@55457
|
262 |
(* this function cannot work as long as the datastructure does not contain thy' *)
|
wneuper@59405
|
263 |
fun thy_containing_cal thy' sop =
|
neuper@42407
|
264 |
let
|
wneuper@59405
|
265 |
val thy = Celem.Thy_Info_get_theory thy'
|
neuper@55457
|
266 |
in
|
neuper@55457
|
267 |
case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
|
neuper@55457
|
268 |
SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Atools" (*FIXME*))
|
neuper@55457
|
269 |
| _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
|
neuper@42407
|
270 |
end
|
neuper@37906
|
271 |
|
wneuper@59263
|
272 |
(* packing return-values to matchTheory, contextToThy for xml-generation *)
|
wneuper@59263
|
273 |
datatype contthy = (*also an item from KEStore on Browser .....#*)
|
wneuper@59263
|
274 |
EContThy (* not from KEStore ..............................*)
|
wneuper@59263
|
275 |
| ContThm of (* a theorem in contex ===========================*)
|
wneuper@59405
|
276 |
{thyID : Celem.thyID, (* for *2guh in sub-elems here .*)
|
wneuper@59405
|
277 |
thm : Celem.guh, (* theorem in the context .*)
|
wneuper@59405
|
278 |
applto : term, (* applied to formula ... .*)
|
wneuper@59405
|
279 |
applat : term, (* ... with lhs inserted .*)
|
wneuper@59405
|
280 |
reword : Celem.rew_ord', (* order used for rewrite .*)
|
wneuper@59405
|
281 |
asms : (term (* asumption instantiated .*)
|
wneuper@59405
|
282 |
* term) list, (* asumption evaluated .*)
|
wneuper@59405
|
283 |
lhs : term (* lhs of the theorem ... #*)
|
wneuper@59405
|
284 |
* term, (* ... instantiated .*)
|
wneuper@59405
|
285 |
rhs : term (* rhs of the theorem ... #*)
|
wneuper@59405
|
286 |
* term, (* ... instantiated .*)
|
wneuper@59405
|
287 |
result : term, (* resulting from the rewrite .*)
|
wneuper@59405
|
288 |
resasms : term list, (* ... with asms stored .*)
|
wneuper@59405
|
289 |
asmrls : Celem.rls' (* ruleset for evaluating asms .*)
|
wneuper@59263
|
290 |
}
|
wneuper@59263
|
291 |
| ContThmInst of (* a theorem with bdvs in contex ============ *)
|
wneuper@59405
|
292 |
{thyID : Celem.thyID, (*for *2guh in sub-elems here .*)
|
wneuper@59405
|
293 |
thm : Celem.guh, (*theorem in the context .*)
|
wneuper@59405
|
294 |
bdvs : Celem.subst, (*bound variables to modify... .*)
|
wneuper@59405
|
295 |
thminst : term, (*... theorem instantiated .*)
|
wneuper@59405
|
296 |
applto : term, (*applied to formula ... .*)
|
wneuper@59405
|
297 |
applat : term, (*... with lhs inserted .*)
|
wneuper@59405
|
298 |
reword : Celem.rew_ord', (*order used for rewrite .*)
|
wneuper@59405
|
299 |
asms : (term (*asumption instantiated .*)
|
wneuper@59405
|
300 |
* term) list, (*asumption evaluated .*)
|
wneuper@59405
|
301 |
lhs : term (*lhs of the theorem ... #*)
|
wneuper@59405
|
302 |
* term, (*... instantiated .*)
|
wneuper@59405
|
303 |
rhs : term (*rhs of the theorem ... #*)
|
wneuper@59405
|
304 |
* term, (*... instantiated .*)
|
wneuper@59405
|
305 |
result : term, (*resulting from the rewrite .*)
|
wneuper@59405
|
306 |
resasms : term list, (*... with asms stored .*)
|
wneuper@59405
|
307 |
asmrls : Celem.rls' (*ruleset for evaluating asms .*)
|
wneuper@59263
|
308 |
}
|
wneuper@59263
|
309 |
| ContRls of (* a rule set in contex ========================= *)
|
wneuper@59405
|
310 |
{thyID : Celem.thyID, (*for *2guh in sub-elems here .*)
|
wneuper@59405
|
311 |
rls : Celem.guh, (*rule set in the context .*)
|
wneuper@59405
|
312 |
applto : term, (*rewrite this formula .*)
|
wneuper@59405
|
313 |
result : term, (*resulting from the rewrite .*)
|
wneuper@59405
|
314 |
asms : term list (*... with asms stored .*)
|
wneuper@59263
|
315 |
}
|
wneuper@59263
|
316 |
| ContRlsInst of (* a rule set with bdvs in contex =========== *)
|
wneuper@59405
|
317 |
{thyID : Celem.thyID, (*for *2guh in sub-elems here .*)
|
wneuper@59405
|
318 |
rls : Celem.guh, (*rule set in the context .*)
|
wneuper@59405
|
319 |
bdvs : Celem.subst, (*for bound variables in thms .*)
|
wneuper@59405
|
320 |
applto : term, (*rewrite this formula .*)
|
wneuper@59405
|
321 |
result : term, (*resulting from the rewrite .*)
|
wneuper@59405
|
322 |
asms : term list (*... with asms stored .*)
|
wneuper@59263
|
323 |
}
|
wneuper@59263
|
324 |
| ContNOrew of (* no rewrite for thm or rls ================== *)
|
wneuper@59405
|
325 |
{thyID : Celem.thyID, (*for *2guh in sub-elems here .*)
|
wneuper@59405
|
326 |
thm_rls : Celem.guh, (*thm or rls in the context .*)
|
wneuper@59405
|
327 |
applto : term (*rewrite this formula .*)
|
wneuper@59263
|
328 |
}
|
wneuper@59263
|
329 |
| ContNOrewInst of (* no rewrite for some instantiation ====== *)
|
wneuper@59405
|
330 |
{thyID : Celem.thyID, (*for *2guh in sub-elems here .*)
|
wneuper@59405
|
331 |
thm_rls : Celem.guh, (*thm or rls in the context .*)
|
wneuper@59405
|
332 |
bdvs : Celem.subst, (*for bound variables in thms .*)
|
wneuper@59405
|
333 |
thminst : term, (*... theorem instantiated .*)
|
wneuper@59405
|
334 |
applto : term (*rewrite this formula .*)
|
wneuper@59263
|
335 |
}
|
neuper@37906
|
336 |
|
neuper@37906
|
337 |
(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
|
neuper@37906
|
338 |
pass other tacs unchanged.*)
|
wneuper@59276
|
339 |
fun get_tac_checked pt ((p, _) : Ctree.pos') = Ctree.get_obj Ctree.g_tac pt p;
|
neuper@37906
|
340 |
|
wneuper@59252
|
341 |
(* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
|
wneuper@59405
|
342 |
fun deriv_of_thm'' (thmID, _) =
|
wneuper@59405
|
343 |
thmID |> Global_Theory.get_thm (Celem.Isac ()) |> Thm.get_name_hint
|
neuper@37906
|
344 |
|
wneuper@59252
|
345 |
(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
|
wneuper@59302
|
346 |
fun context_thy (pt, pos as (p,p_)) (tac as Tac.Rewrite thm'') =
|
wneuper@59263
|
347 |
let val thm_deriv = deriv_of_thm'' thm''
|
wneuper@59263
|
348 |
in
|
wneuper@59272
|
349 |
(case Applicable.applicable_in pos pt tac of
|
wneuper@59302
|
350 |
Chead.Appl (Tac.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
|
wneuper@59263
|
351 |
ContThm
|
wneuper@59405
|
352 |
{thyID = Celem.theory'2thyID thy',
|
wneuper@59405
|
353 |
thm = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
|
wneuper@59405
|
354 |
applto = f, applat = Celem.e_term, reword = ord',
|
wneuper@59405
|
355 |
asms = [](*asms ~~ asms'*), lhs = (Celem.e_term, Celem.e_term)(*(lhs, lhs')*), rhs = (Celem.e_term, Celem.e_term)(*(rhs, rhs')*),
|
wneuper@59405
|
356 |
result = res, resasms = asm, asmrls = Celem.id_rls erls}
|
wneuper@59265
|
357 |
| Chead.Notappl _ =>
|
wneuper@59263
|
358 |
let
|
wneuper@59276
|
359 |
val pp = Ctree.par_pblobj pt p
|
wneuper@59276
|
360 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp
|
wneuper@59263
|
361 |
val f = case p_ of
|
wneuper@59313
|
362 |
Ctree.Frm => Ctree.get_obj Ctree.g_form pt p
|
wneuper@59313
|
363 |
| Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
|
wneuper@59313
|
364 |
| _ => error "context_thy: uncovered position"
|
wneuper@59263
|
365 |
in
|
wneuper@59263
|
366 |
ContNOrew
|
wneuper@59405
|
367 |
{thyID = Celem.theory'2thyID thy',
|
wneuper@59263
|
368 |
thm_rls =
|
wneuper@59405
|
369 |
Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
|
wneuper@59263
|
370 |
applto = f}
|
wneuper@59263
|
371 |
end
|
wneuper@59263
|
372 |
| _ => error "context_thy..Rewrite: uncovered case 2")
|
wneuper@59263
|
373 |
end
|
wneuper@59302
|
374 |
| context_thy (pt, pos as (p, p_)) (tac as Tac.Rewrite_Inst (subs, (thmID, _))) =
|
wneuper@59405
|
375 |
let val thm = Global_Theory.get_thm (Celem.Isac ()) thmID
|
wneuper@59263
|
376 |
in
|
wneuper@59272
|
377 |
(case Applicable.applicable_in pos pt tac of
|
wneuper@59302
|
378 |
Chead.Appl (Tac.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
|
wneuper@59263
|
379 |
let
|
wneuper@59263
|
380 |
val thm_deriv = Thm.get_name_hint thm
|
wneuper@59389
|
381 |
val thminst = TermC.inst_bdv subst ((Calc.norm o #prop o Thm.rep_thm) thm)
|
wneuper@59263
|
382 |
in
|
wneuper@59263
|
383 |
ContThmInst
|
wneuper@59405
|
384 |
{thyID = Celem.theory'2thyID thy',
|
wneuper@59263
|
385 |
thm =
|
wneuper@59405
|
386 |
Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
|
wneuper@59405
|
387 |
bdvs = subst, thminst = thminst, applto = f, applat = Celem.e_term, reword = ord',
|
wneuper@59405
|
388 |
asms = [](*asms ~~ asms'*), lhs = (Celem.e_term, Celem.e_term)(*(lhs, lhs')*), rhs = (Celem.e_term, Celem.e_term)(*(rhs, rhs')*),
|
wneuper@59405
|
389 |
result = res, resasms = asm, asmrls = Celem.id_rls erls}
|
wneuper@59263
|
390 |
end
|
wneuper@59265
|
391 |
| Chead.Notappl _ =>
|
wneuper@59263
|
392 |
let
|
wneuper@59405
|
393 |
val thm = Global_Theory.get_thm (Celem.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
|
wneuper@59263
|
394 |
val thm_deriv = Thm.get_name_hint thm
|
wneuper@59276
|
395 |
val pp = Ctree.par_pblobj pt p
|
wneuper@59276
|
396 |
val thy' = Ctree.get_obj Ctree.g_domID pt pp
|
wneuper@59405
|
397 |
val subst = Selem.subs2subst (Celem.assoc_thy thy') subs
|
wneuper@59389
|
398 |
val thminst = TermC.inst_bdv subst ((Calc.norm o #prop o Thm.rep_thm) thm)
|
wneuper@59263
|
399 |
val f = case p_ of
|
wneuper@59313
|
400 |
Ctree.Frm => Ctree.get_obj Ctree.g_form pt p
|
wneuper@59313
|
401 |
| Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
|
wneuper@59313
|
402 |
| _ => error "context_thy: uncovered case 3"
|
wneuper@59263
|
403 |
in
|
wneuper@59263
|
404 |
ContNOrewInst
|
wneuper@59405
|
405 |
{thyID = Celem.theory'2thyID thy',
|
wneuper@59405
|
406 |
thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
|
wneuper@59263
|
407 |
bdvs = subst, thminst = thminst, applto = f}
|
wneuper@59263
|
408 |
end
|
wneuper@59263
|
409 |
| _ => error "context_thy..Rewrite_Inst: uncovered case 4")
|
wneuper@59263
|
410 |
end
|
wneuper@59302
|
411 |
| context_thy (pt, p) (tac as Tac.Rewrite_Set rls') =
|
wneuper@59272
|
412 |
(case Applicable.applicable_in p pt tac of
|
wneuper@59302
|
413 |
Chead.Appl (Tac.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
|
wneuper@59263
|
414 |
ContRls
|
wneuper@59405
|
415 |
{thyID = Celem.theory'2thyID thy',
|
wneuper@59405
|
416 |
rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',
|
wneuper@59263
|
417 |
applto = f, result = res, asms = asm}
|
wneuper@59265
|
418 |
| _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
|
wneuper@59302
|
419 |
| context_thy (pt,p) (tac as Tac.Rewrite_Set_Inst (_(*subs*), rls')) =
|
wneuper@59272
|
420 |
(case Applicable.applicable_in p pt tac of
|
wneuper@59302
|
421 |
Chead.Appl (Tac.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
|
wneuper@59263
|
422 |
ContRlsInst
|
wneuper@59405
|
423 |
{thyID = Celem.theory'2thyID thy',
|
wneuper@59405
|
424 |
rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',
|
wneuper@59263
|
425 |
bdvs = subst, applto = f, result = res, asms = asm}
|
wneuper@59265
|
426 |
| _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))
|
wneuper@59263
|
427 |
| context_thy (_, p) tac =
|
wneuper@59302
|
428 |
error ("context_thy: not for tac " ^ Tac.tac2str tac ^ " at " ^ Ctree.pos'2str p)
|
neuper@37906
|
429 |
|
neuper@42372
|
430 |
(* get all theorems in a rule set (recursivley containing rule sets) *)
|
neuper@37906
|
431 |
fun thm_of_rule Erule = []
|
wneuper@59405
|
432 |
| thm_of_rule (thm as Celem.Thm _) = [thm]
|
wneuper@59405
|
433 |
| thm_of_rule (Celem.Calc _) = []
|
wneuper@59405
|
434 |
| thm_of_rule (Celem.Cal1 _) = []
|
wneuper@59405
|
435 |
| thm_of_rule (Celem.Rls_ rls) = thms_of_rls rls
|
wneuper@59405
|
436 |
and thms_of_rls Celem.Erls = []
|
wneuper@59405
|
437 |
| thms_of_rls (Celem.Rls {rules,...}) = (flat o (map thm_of_rule)) rules
|
wneuper@59405
|
438 |
| thms_of_rls (Celem.Seq {rules,...}) = (flat o (map thm_of_rule)) rules
|
wneuper@59405
|
439 |
| thms_of_rls (Celem.Rrls _) = []
|
neuper@37906
|
440 |
|
wneuper@59263
|
441 |
(* check if a rule is contained in a rule-set (recursivley down in Rls_);
|
wneuper@59263
|
442 |
this rule can even be a rule-set itself *)
|
neuper@37906
|
443 |
fun contains_rule r rls =
|
wneuper@59263
|
444 |
let
|
wneuper@59263
|
445 |
fun (*find (_, Rls_ rls) = finds (get_rules rls)
|
wneuper@59263
|
446 |
| find r12 = eq_rule r12
|
wneuper@59263
|
447 |
and*) finds [] = false
|
wneuper@59405
|
448 |
| finds (r1 :: rs) = if Celem.eq_rule (r, r1) then true else finds rs
|
wneuper@59263
|
449 |
in
|
wneuper@59405
|
450 |
finds (Celem.get_rules rls)
|
wneuper@59263
|
451 |
end
|
neuper@37906
|
452 |
|
wneuper@59263
|
453 |
(* try if a rewrite-rule is applicable to a given formula;
|
wneuper@59263
|
454 |
in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
|
wneuper@59405
|
455 |
fun try_rew thy ((_, ro) : Celem.rew_ord) erls (subst : Celem.subst) f (thm' as Celem.Thm (_, thm)) =
|
wneuper@59374
|
456 |
if LTool.contains_bdv thm
|
wneuper@59380
|
457 |
then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
|
wneuper@59302
|
458 |
SOME _ => [Tac.rule2tac thy subst thm']
|
wneuper@59263
|
459 |
| NONE => []
|
wneuper@59380
|
460 |
else (case Rewrite.rewrite_ thy ro erls false thm f of
|
wneuper@59302
|
461 |
SOME _ => [Tac.rule2tac thy [] thm']
|
wneuper@59263
|
462 |
| NONE => [])
|
wneuper@59405
|
463 |
| try_rew thy _ _ _ f (cal as Celem.Calc c) =
|
wneuper@59386
|
464 |
(case Calc.adhoc_thm thy c f of
|
wneuper@59302
|
465 |
SOME _ => [Tac.rule2tac thy [] cal]
|
wneuper@59263
|
466 |
| NONE => [])
|
wneuper@59405
|
467 |
| try_rew thy _ _ _ f (cal as Celem.Cal1 c) =
|
wneuper@59386
|
468 |
(case Calc.adhoc_thm thy c f of
|
wneuper@59302
|
469 |
SOME _ => [Tac.rule2tac thy [] cal]
|
neuper@37926
|
470 |
| NONE => [])
|
wneuper@59405
|
471 |
| try_rew thy _ _ subst f (Celem.Rls_ rls) = filter_appl_rews thy subst f rls
|
wneuper@59263
|
472 |
| try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
|
wneuper@59405
|
473 |
and filter_appl_rews thy subst f (Celem.Rls {rew_ord = ro, erls, rules, ...}) =
|
wneuper@59302
|
474 |
gen_distinct Tac.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
|
wneuper@59405
|
475 |
| filter_appl_rews thy subst f (Celem.Seq {rew_ord = ro, erls, rules,...}) =
|
wneuper@59302
|
476 |
gen_distinct Tac.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
|
wneuper@59405
|
477 |
| filter_appl_rews _ _ _ (Celem.Rrls _) = []
|
wneuper@59263
|
478 |
| filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
|
neuper@37906
|
479 |
|
wneuper@59263
|
480 |
(* decide if a tactic is applicable to a given formula;
|
wneuper@59263
|
481 |
in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
|
wneuper@59302
|
482 |
fun atomic_appl_tacs thy _ _ f (Tac.Calculate scrID) =
|
wneuper@59405
|
483 |
try_rew thy Celem.e_rew_ordX Celem.e_rls [] f (Celem.Calc (assoc_calc' thy scrID |> snd))
|
wneuper@59302
|
484 |
| atomic_appl_tacs thy ro erls f (Tac.Rewrite thm'') =
|
wneuper@59405
|
485 |
try_rew thy (ro, Celem.assoc_rew_ord ro) erls [] f (Celem.Thm thm'')
|
wneuper@59302
|
486 |
| atomic_appl_tacs thy ro erls f (Tac.Rewrite_Inst (subs, thm'')) =
|
wneuper@59405
|
487 |
try_rew thy (ro, Celem.assoc_rew_ord ro) erls (Selem.subs2subst thy subs) f (Celem.Thm thm'')
|
neuper@37906
|
488 |
|
wneuper@59302
|
489 |
| atomic_appl_tacs thy _ _ f (Tac.Rewrite_Set rls') =
|
neuper@37906
|
490 |
filter_appl_rews thy [] f (assoc_rls rls')
|
wneuper@59302
|
491 |
| atomic_appl_tacs thy _ _ f (Tac.Rewrite_Set_Inst (subs, rls')) =
|
wneuper@59301
|
492 |
filter_appl_rews thy (Selem.subs2subst thy subs) f (assoc_rls rls')
|
neuper@37906
|
493 |
| atomic_appl_tacs _ _ _ _ tac =
|
wneuper@59302
|
494 |
(tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Tac.tac2str tac ^ "'"); []);
|
neuper@37906
|
495 |
|
wneuper@59263
|
496 |
(* filenames not only for thydata, but also for thy's etc *)
|
wneuper@59405
|
497 |
fun theID2filename theID = Celem.theID2guh theID ^ ".xml"
|
neuper@37906
|
498 |
|
wneuper@59405
|
499 |
fun guh2theID guh =
|
wneuper@59263
|
500 |
let
|
wneuper@59263
|
501 |
val guh' = Symbol.explode guh
|
wneuper@59263
|
502 |
val part = implode (take_fromto 1 4 guh')
|
wneuper@59263
|
503 |
val isa = implode (take_fromto 5 9 guh')
|
wneuper@59263
|
504 |
in
|
wneuper@59263
|
505 |
if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
|
wneuper@59263
|
506 |
then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")
|
wneuper@59263
|
507 |
else
|
wneuper@59263
|
508 |
let
|
wneuper@59263
|
509 |
val chap = case isa of
|
wneuper@59263
|
510 |
"isab_" => "Isabelle"
|
wneuper@59263
|
511 |
| "scri_" => "IsacScripts"
|
wneuper@59263
|
512 |
| "isac_" => "IsacKnowledge"
|
wneuper@59263
|
513 |
| _ =>
|
wneuper@59263
|
514 |
raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")
|
wneuper@59263
|
515 |
val rest = takerest (9, guh')
|
wneuper@59263
|
516 |
val thyID = takewhile [] (not o (curry op= "-")) rest
|
wneuper@59263
|
517 |
val rest' = dropuntil (curry op = "-") rest
|
neuper@37906
|
518 |
in case implode rest' of
|
wneuper@59405
|
519 |
"-part" => [chap] : Celem.theID
|
wneuper@59263
|
520 |
| "" => [chap, implode thyID]
|
wneuper@59263
|
521 |
| "-Theorems" => [chap, implode thyID, "Theorems"]
|
wneuper@59263
|
522 |
| "-Rulesets" => [chap, implode thyID, "Rulesets"]
|
wneuper@59263
|
523 |
| "-Operations" => [chap, implode thyID, "Operations"]
|
wneuper@59263
|
524 |
| "-Orders" => [chap, implode thyID, "Orders"]
|
wneuper@59263
|
525 |
| _ =>
|
wneuper@59263
|
526 |
let val sect = implode (take_fromto 1 5 rest')
|
wneuper@59263
|
527 |
val sect' = case sect of
|
neuper@37906
|
528 |
"-thm-" => "Theorems"
|
neuper@37906
|
529 |
| "-rls-" => "Rulesets"
|
neuper@37906
|
530 |
| "-cal-" => "Operations"
|
neuper@37906
|
531 |
| "-ord-" => "Orders"
|
wneuper@59263
|
532 |
| _ =>
|
wneuper@59263
|
533 |
raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")
|
wneuper@59263
|
534 |
in
|
wneuper@59263
|
535 |
[chap, implode thyID, sect', implode (takerest (5, rest'))]
|
wneuper@59263
|
536 |
end
|
neuper@37906
|
537 |
end
|
wneuper@59263
|
538 |
end
|
neuper@37906
|
539 |
|
wneuper@59405
|
540 |
fun guh2filename guh = guh ^ ".xml";
|
neuper@37906
|
541 |
|
wneuper@59301
|
542 |
fun guh2rewtac guh [] =
|
wneuper@59263
|
543 |
let
|
wneuper@59263
|
544 |
val (_, thy, sect, xstr) = case guh2theID guh of
|
wneuper@59263
|
545 |
[isa, thy, sect, xstr] => (isa, thy, sect, xstr)
|
wneuper@59263
|
546 |
| _ => error "guh2rewtac: uncovered case"
|
wneuper@59263
|
547 |
in case sect of
|
wneuper@59405
|
548 |
"Theorems" => Tac.Rewrite (xstr, Rewrite.assoc_thm'' (Celem.assoc_thy thy) xstr)
|
wneuper@59302
|
549 |
| "Rulesets" => Tac.Rewrite_Set xstr
|
wneuper@59263
|
550 |
| _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
|
wneuper@59263
|
551 |
end
|
wneuper@59263
|
552 |
| guh2rewtac guh subs =
|
wneuper@59263
|
553 |
let
|
wneuper@59263
|
554 |
val (_, thy, sect, xstr) = case guh2theID guh of
|
wneuper@59263
|
555 |
[isa, thy, sect, xstr] => (isa, thy, sect, xstr)
|
wneuper@59263
|
556 |
| _ => error "guh2rewtac: uncovered case"
|
wneuper@59263
|
557 |
in case sect of
|
wneuper@59263
|
558 |
"Theorems" =>
|
wneuper@59405
|
559 |
Tac.Rewrite_Inst (subs, (xstr, Rewrite.assoc_thm'' (Celem.assoc_thy thy) xstr))
|
wneuper@59302
|
560 |
| "Rulesets" => Tac.Rewrite_Set_Inst (subs, xstr)
|
wneuper@59263
|
561 |
| str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
|
wneuper@59263
|
562 |
end
|
neuper@37906
|
563 |
|
wneuper@59263
|
564 |
(* the front-end may request a context for any element of the hierarchy *)
|
wneuper@59405
|
565 |
fun no_thycontext guh = (guh2theID guh; false)
|
wneuper@59263
|
566 |
handle ERROR _ => true;
|
neuper@37906
|
567 |
|
wneuper@59263
|
568 |
(* get the substitution of bound variables for matchTheory:
|
neuper@37906
|
569 |
# lookup the thm|rls' in the script
|
neuper@37906
|
570 |
# take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
|
neuper@37906
|
571 |
# instantiate this subs with the istates env to [(bdv, x),..]
|
wneuper@59263
|
572 |
# otherwise []
|
wneuper@59263
|
573 |
WN060617 hack assuming that all scripts use only one bound variable
|
wneuper@59263
|
574 |
and use 'v_' as the formal argument for this bound variable*)
|
wneuper@59405
|
575 |
fun subs_from (Selem.ScrState (env, _, _, _, _, _)) _ guh =
|
wneuper@59263
|
576 |
let
|
wneuper@59263
|
577 |
val (_, _, thyID, sect, xstr) = case guh2theID guh of
|
wneuper@59263
|
578 |
theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
|
wneuper@59263
|
579 |
| _ => error "subs_from: uncovered case"
|
wneuper@59263
|
580 |
in
|
wneuper@59263
|
581 |
case sect of
|
wneuper@59263
|
582 |
"Theorems" =>
|
wneuper@59405
|
583 |
let val thm = Global_Theory.get_thm (Celem.assoc_thy (Celem.thyID2theory' thyID)) xstr
|
wneuper@59263
|
584 |
in
|
wneuper@59374
|
585 |
if LTool.contains_bdv thm
|
wneuper@59263
|
586 |
then
|
wneuper@59263
|
587 |
let
|
wneuper@59389
|
588 |
val formal_arg = TermC.str2term "v_"
|
wneuper@59263
|
589 |
val value = subst_atomic env formal_arg
|
wneuper@59405
|
590 |
in ["(bdv," ^ Celem.term2str value ^ ")"] : Selem.subs end
|
wneuper@59263
|
591 |
else []
|
wneuper@59263
|
592 |
end
|
wneuper@59263
|
593 |
| "Rulesets" =>
|
wneuper@59263
|
594 |
let
|
wneuper@59405
|
595 |
val rules = (Celem.get_rules o assoc_rls) xstr
|
wneuper@59263
|
596 |
in
|
wneuper@59374
|
597 |
if LTool.contain_bdv rules
|
wneuper@59263
|
598 |
then
|
wneuper@59263
|
599 |
let
|
wneuper@59389
|
600 |
val formal_arg = TermC.str2term "v_"
|
wneuper@59263
|
601 |
val value = subst_atomic env formal_arg
|
wneuper@59405
|
602 |
in ["(bdv," ^ Celem.term2str value ^ ")"] : Selem.subs end
|
wneuper@59263
|
603 |
else []
|
wneuper@59263
|
604 |
end
|
wneuper@59263
|
605 |
| str => error ("subs_from: uncovered case with " ^ str)
|
wneuper@59263
|
606 |
end
|
wneuper@59405
|
607 |
| subs_from _ _ guh = error ("subs_from: uncovered case with " ^ guh)
|
neuper@37906
|
608 |
|
neuper@42433
|
609 |
(* get a substitution for "bdv*" from the current program and environment.
|
wneuper@59263
|
610 |
returns a substitution: subst for rewriting and another: sube for Rewrite: *)
|
neuper@42433
|
611 |
fun get_bdv_subst prog env =
|
neuper@42433
|
612 |
let
|
neuper@42433
|
613 |
fun scan (Const _) = NONE
|
neuper@42433
|
614 |
| scan (Free _) = NONE
|
neuper@42433
|
615 |
| scan (Var _) = NONE
|
neuper@42433
|
616 |
| scan (Bound _) = NONE
|
wneuper@59263
|
617 |
| scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ Free _$ _) $ _) =
|
wneuper@59389
|
618 |
if TermC.is_bdv_subst t then SOME t else NONE
|
neuper@42433
|
619 |
| scan (Abs (_, _, body)) = scan body
|
wneuper@59263
|
620 |
| scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
|
neuper@42433
|
621 |
in
|
neuper@42433
|
622 |
case scan prog of
|
wneuper@59405
|
623 |
NONE => (NONE: Selem.subs option, []: Celem.subst)
|
neuper@42433
|
624 |
| SOME tm =>
|
wneuper@59389
|
625 |
let val subst = tm |> subst_atomic env |> TermC.isalist2list |> map TermC.isapair2pair
|
wneuper@59263
|
626 |
(* "[(bdv,v_v)]": term
|
neuper@42433
|
627 |
|> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
|
wneuper@59263
|
628 |
|> [("bdv","x")]: (term * term) list *)
|
wneuper@59301
|
629 |
in (SOME (Selem.subst2subs subst), subst) end
|
neuper@42433
|
630 |
(*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)
|
wneuper@59263
|
631 |
end
|
neuper@42433
|
632 |
|
wneuper@59263
|
633 |
end
|