1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,845 @@
1.4 +(* tools for rewriting, reverse rewriting, context to thy concerning rewriting
1.5 + authors: Walther Neuper 2002, 2006
1.6 + (c) due to copyright terms
1.7 +
1.8 +use"ME/rewtools.sml";
1.9 +use"rewtools.sml";
1.10 +*)
1.11 +
1.12 +
1.13 +
1.14 +(***.reverse rewriting.***)
1.15 +
1.16 +(*.derivation for insertin one level of nodes into the calctree.*)
1.17 +type deriv = (term * rule * (term *term list)) list;
1.18 +
1.19 +fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^
1.20 + (term2str t')^", "^(terms2str a)^"))";
1.21 +fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
1.22 +val deriv2str = trtas2str;
1.23 +fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^
1.24 + (term2str t)^", "^(terms2str a)^"))";
1.25 +fun rtas2str rtas = (strs2str o (map rta2str)) rtas;
1.26 +val deri2str = rtas2str;
1.27 +
1.28 +
1.29 +(*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)
1.30 +fun sym_thm thm =
1.31 + let
1.32 + val (deriv, {thy_ref = thy_ref, tags = tags, maxidx = maxidx,
1.33 + shyps = shyps, hyps = hyps, tpairs = tpairs,
1.34 + prop = prop}) =
1.35 + rep_thm_G thm;
1.36 + val (lhs,rhs) = (dest_equals' o strip_trueprop
1.37 + o Logic.strip_imp_concl) prop;
1.38 + val prop' = case strip_imp_prems' prop of
1.39 + NONE => Trueprop $ (mk_equality (rhs, lhs))
1.40 + | SOME cs =>
1.41 + ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
1.42 + in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
1.43 +(*
1.44 + (sym RS real_mult_div_cancel1) handle e => print_exn e;
1.45 +Exception THM 1 raised:
1.46 +RSN: no unifiers
1.47 +"?s = ?t ==> ?t = ?s"
1.48 +"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
1.49 +
1.50 + val thm = real_mult_div_cancel1;
1.51 + val prop = (#prop o rep_thm) thm;
1.52 + atomt prop;
1.53 + val ppp = Logic.strip_imp_concl prop;
1.54 + atomt ppp;
1.55 + ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;
1.56 +val it = true : bool
1.57 + ((sym_thm o sym_thm) thm) = thm;
1.58 +val it = true : bool
1.59 +
1.60 + val thm = real_le_anti_sym;
1.61 + ((sym_thm o sym_thm) thm) = thm;
1.62 +val it = true : bool
1.63 +
1.64 + val thm = real_minus_zero;
1.65 + ((sym_thm o sym_thm) thm) = thm;
1.66 +val it = true : bool
1.67 +*)
1.68 +
1.69 +
1.70 +
1.71 +(*.derive normalform of a rls, or derive until SOME goal,
1.72 + and record rules applied and rewrites.
1.73 +val it = fn
1.74 + : theory
1.75 + -> rls
1.76 + -> rule list
1.77 + -> rew_ord : the order of this rls, which 1 theorem of is used
1.78 + for rewriting 1 single step (?14.4.03)
1.79 + -> term option : 040214 ??? nonsense ???
1.80 + -> term
1.81 + -> (term * : to this term ...
1.82 + rule * : ... this rule is applied yielding ...
1.83 + (term * : ... this term ...
1.84 + term list)) : ... under these assumptions.
1.85 + list :
1.86 +returns empty list for a normal form
1.87 +FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
1.88 +
1.89 +WN060825 too complicated for the intended use by cancel_, common_nominator_
1.90 +and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
1.91 + -- replaced below*)
1.92 +(* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
1.93 + val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt);
1.94 + *)
1.95 +fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
1.96 + let datatype switch = Appl | Noap
1.97 + fun rew_once lim rts t Noap [] =
1.98 + (case goal of
1.99 + NONE => rts
1.100 + | SOME g =>
1.101 + raise error ("make_deriv: no derivation for "^(term2str t)))
1.102 + | rew_once lim rts t Appl [] =
1.103 + (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
1.104 + (*| Seq _ => rts) FIXXXXXME 14.3.03*)
1.105 + | rew_once lim rts t apno rs' =
1.106 + (case goal of
1.107 + NONE => rew_or_calc lim rts t apno rs'
1.108 + | SOME g =>
1.109 + if g = t then rts
1.110 + else rew_or_calc lim rts t apno rs')
1.111 + and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
1.112 + if lim < 0
1.113 + then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
1.114 + "with deriv =\n"); writeln (deriv2str rts); rts)
1.115 + else
1.116 + case r of
1.117 + Thm (thmid, tm) =>
1.118 + (if not (!trace_rewrite) then () else
1.119 + writeln ("### trying thm '" ^ thmid ^ "'");
1.120 + case rewrite_ thy ro erls true tm t of
1.121 + NONE => rew_once lim rts t apno rs'
1.122 + | SOME (t',a') =>
1.123 + (if ! trace_rewrite
1.124 + then writeln ("### rewrites to: "^(term2str t')) else();
1.125 + rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
1.126 + | Calc (c as (op_,_)) =>
1.127 + let val _ = if not (!trace_rewrite) then () else
1.128 + writeln ("### trying calc. '" ^ op_ ^ "'")
1.129 + val t = uminus_to_string t
1.130 + in case get_calculation_ thy c t of
1.131 + NONE => rew_once lim rts t apno rs'
1.132 + | SOME (thmid, tm) =>
1.133 + (let val SOME (t',a') = rewrite_ thy ro erls true tm t
1.134 + val _ = if not (!trace_rewrite) then () else
1.135 + writeln("### calc. to: " ^ (term2str t'))
1.136 + val r' = Thm (thmid, tm)
1.137 + in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
1.138 + end)
1.139 + handle _ => raise error "derive_norm, Calc: no rewrite"
1.140 + end
1.141 +(* TODO.WN080222: see rewrite__set_
1.142 + @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
1.143 + | Cal1 (cc as (op_,_)) =>
1.144 + (let val _= if !trace_rewrite andalso i < ! depth then
1.145 + writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
1.146 + val ct = uminus_to_string ct
1.147 + in case get_calculation_ thy cc ct of
1.148 + NONE => (ct, asm)
1.149 + | SOME (thmid, thm') =>
1.150 + let
1.151 + val pairopt =
1.152 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.153 + ((#erls o rep_rls) rls) put_asm thm' ct;
1.154 + val _ = if pairopt <> NONE then ()
1.155 + else raise error("rewrite_set_, rewrite_ \""^
1.156 + (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
1.157 + val _ = if ! trace_rewrite andalso i < ! depth
1.158 + then writeln((idt"="(i+1))^" cal1. to: "^
1.159 + (term2str ((fst o the) pairopt)))
1.160 + else()
1.161 + in the pairopt end
1.162 + end)
1.163 +@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.164 + | Rls_ rls =>
1.165 + (case rewrite_set_ thy true rls t of
1.166 + NONE => rew_once lim rts t apno rs'
1.167 + | SOME (t',a') =>
1.168 + rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
1.169 +(*WN060829 | Rls_ rls =>
1.170 + (case rewrite_set_ thy true rls t of
1.171 + NONE => rew_once lim rts t apno rs'
1.172 + | SOME (t',a') =>
1.173 + if ro [] (t, t') then rew_once lim rts t apno rs'
1.174 + else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
1.175 +...lead to deriv = [] with make_polynomial.
1.176 +THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
1.177 +and between rewriting with rewrite_set: with rules from make_polynomial and
1.178 +t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
1.179 +leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..
1.180 +*)
1.181 + in rew_once (!lim_deriv) [] tt Noap rs end;
1.182 +
1.183 +
1.184 +(*.toggles the marker for 'fun sym_thm'.*)
1.185 +fun sym_thmID (thmID : thmID) =
1.186 + case explode thmID of
1.187 + "s"::"y"::"m"::"_"::id => implode id : thmID
1.188 + | id => "sym_"^thmID;
1.189 +(*
1.190 +> val thmID = "sym_real_mult_2";
1.191 +> sym_thmID thmID;
1.192 +val it = "real_mult_2" : string
1.193 +> val thmID = "real_num_collect";
1.194 +> sym_thmID thmID;
1.195 +val it = "sym_real_num_collect" : string*)
1.196 +fun sym_drop (thmID : thmID) =
1.197 + case explode thmID of
1.198 + "s"::"y"::"m"::"_"::id => implode id : thmID
1.199 + | id => thmID;
1.200 +fun is_sym (thmID : thmID) =
1.201 + case explode thmID of
1.202 + "s"::"y"::"m"::"_"::id => true
1.203 + | id => false;
1.204 +
1.205 +
1.206 +(*FIXXXXME.040219: detail has to handle Rls id="sym_..."
1.207 + by applying make_deriv, rev_deriv'; see concat_deriv*)
1.208 +fun sym_rls Erls = Erls
1.209 + | sym_rls (Rls {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
1.210 + Rls {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls,
1.211 + rules=rules, rew_ord=rew_ord, preconds=preconds}
1.212 + | sym_rls (Seq {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
1.213 + Seq {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls,
1.214 + rules=rules, rew_ord=rew_ord, preconds=preconds}
1.215 + | sym_rls (Rrls {id, scr, calc, erls, prepat, rew_ord}) =
1.216 + Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat,
1.217 + rew_ord=rew_ord};
1.218 +
1.219 +fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
1.220 + | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
1.221 + | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
1.222 +(*
1.223 + val th = Thm ("real_one_collect",num_str real_one_collect);
1.224 + sym_Thm th;
1.225 +val th =
1.226 + Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
1.227 + : rule
1.228 +ML> val it =
1.229 + Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
1.230 +
1.231 +
1.232 +(*version for reverse rewrite used before 040214*)
1.233 +fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
1.234 +(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');
1.235 + *)
1.236 +fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
1.237 + (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
1.238 +(*
1.239 + val rev_rew = reverse_deriv thy e_rls ;
1.240 + writeln(rtas2str rev_rew);
1.241 +*)
1.242 +
1.243 +fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
1.244 + | eq_Thm (Thm (id1,_), _) = false
1.245 + | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
1.246 + | eq_Thm (Rls_ r1, _) = false
1.247 + | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^
1.248 + (rule2str r1)^"' '"^(rule2str r2)^"'");
1.249 +fun distinct_Thm r = gen_distinct eq_Thm r;
1.250 +
1.251 +fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))
1.252 + handle _ => false;
1.253 +
1.254 +
1.255 +(***. context to thy concerning rewriting .***)
1.256 +
1.257 +(*.create the unique handles and filenames for the theory-data.*)
1.258 +fun part2guh ([str]:theID) =
1.259 + (case str of
1.260 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
1.261 + | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
1.262 + | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
1.263 + | str => raise error ("thy2guh: called with '"^str^"'"))
1.264 + | part2guh theID = raise error ("part2guh called with theID = "
1.265 + ^ theID2str theID);
1.266 +fun part2filename str = part2guh str ^ ".xml" : filename;
1.267 +
1.268 +
1.269 +fun thy2guh ([part, thyID]:theID) =
1.270 + (case part of
1.271 + "Isabelle" => "thy_isab_" ^ thyID : guh
1.272 + | "IsacScripts" => "thy_scri_" ^ thyID
1.273 + | "IsacKnowledge" => "thy_isac_" ^ thyID
1.274 + | str => raise error ("thy2guh: called with '"^str^"'"))
1.275 + | thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'");
1.276 +fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
1.277 +fun thypart2guh ([part, thyID, thypart]:theID) =
1.278 + case part of
1.279 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
1.280 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
1.281 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
1.282 + | str => raise error ("thypart2guh: called with '"^str^"'");
1.283 +fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
1.284 +
1.285 +(*.convert the data got via contextToThy to a globally unique handle
1.286 + there is another way to get the guh out of the 'theID' in the hierarchy.*)
1.287 +fun thm2guh (isa, thyID:thyID) (thmID:thmID) =
1.288 + case isa of
1.289 + "Isabelle" =>
1.290 + "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
1.291 + | "IsacKnowledge" =>
1.292 + "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.293 + | "IsacScripts" =>
1.294 + "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
1.295 + | str => raise error ("thm2guh called with isa = '"^isa^
1.296 + "' for thm = "^thmID^"'");
1.297 +fun thm2filename (isa_thyID: string * thyID) thmID =
1.298 + (thm2guh isa_thyID thmID) ^ ".xml" : filename;
1.299 +
1.300 +fun rls2guh (isa, thyID:thyID) (rls':rls') =
1.301 + case isa of
1.302 + "Isabelle" =>
1.303 + "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
1.304 + | "IsacKnowledge" =>
1.305 + "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.306 + | "IsacScripts" =>
1.307 + "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
1.308 + | str => raise error ("rls2guh called with isa = '"^isa^
1.309 + "' for rls = '"^rls'^"'");
1.310 + fun rls2filename (isa, thyID) rls' =
1.311 + rls2guh (isa, thyID) rls' ^ ".xml" : filename;
1.312 +
1.313 +fun cal2guh (isa, thyID:thyID) calID =
1.314 + case isa of
1.315 + "Isabelle" =>
1.316 + "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
1.317 + | "IsacKnowledge" =>
1.318 + "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.319 + | "IsacScripts" =>
1.320 + "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
1.321 + | str => raise error ("cal2guh called with isa = '"^isa^
1.322 + "' for cal = '"^calID^"'");
1.323 +fun cal2filename (isa, thyID:thyID) calID =
1.324 + cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
1.325 +
1.326 +fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =
1.327 + case isa of
1.328 + "Isabelle" =>
1.329 + "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
1.330 + | "IsacKnowledge" =>
1.331 + "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.332 + | "IsacScripts" =>
1.333 + "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
1.334 + | str => raise error ("ord2guh called with isa = '"^isa^
1.335 + "' for ord = '"^rew_ord'^"'");
1.336 +fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
1.337 + ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
1.338 +
1.339 +
1.340 +(**.set up isab_thm_thy in Isac.ML.**)
1.341 +
1.342 +fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));
1.343 +fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));
1.344 +
1.345 +(*.lookup the missing theorems in some thy (of Isabelle).*)
1.346 +fun make_isa missthms thy =
1.347 + map (pair (theory2thyID thy))
1.348 + ((inter eq_thmI) missthms (PureThy.all_thms_of thy))
1.349 + : (thyID * (thmID * Thm.thm)) list;
1.350 +
1.351 +(*.separate handling of sym_thms.*)
1.352 +fun make_isab rlsthmsNOTisac isab_thys =
1.353 + let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
1.354 + val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
1.355 + val notsym_isab = (flat o (map (make_isa notsym))) isab_thys
1.356 +
1.357 + val sym = filter (is_sym o #1) rlsthmsNOTisac
1.358 +
1.359 + val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym
1.360 + val symsym_isab = (flat o (map (make_isa symsym))) isab_thys
1.361 +
1.362 + val sym_isab = map (((apsnd o apfst) sym_drop) o
1.363 + ((apsnd o apsnd) sym_thm)) symsym_isab
1.364 +
1.365 + val isab = notsym_isab @ symsym_isab @ sym_isab
1.366 + in ((map rearrange) o (gen_sort les)) isab
1.367 + : (thmID * (thyID * Thm.thm)) list
1.368 + end;
1.369 +
1.370 +(*.which theory below thy' contains a theorem; this can be in isabelle !
1.371 +get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
1.372 +(* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy));
1.373 + val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
1.374 + *)
1.375 +fun thy_contains_thm (str:xstring) (_, thy) =
1.376 + member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str;
1.377 +(* val (thy', str) = ("Isac.thy", "real_mult_minus1");
1.378 + val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
1.379 + *)
1.380 +fun thy_containing_thm (thy':theory') (str:xstring) =
1.381 + let val thy' = thyID2theory' thy'
1.382 + val str = sym_drop str
1.383 + val startsearch = dropuntil ((curry op= thy') o
1.384 + (#1:theory' * theory -> theory'))
1.385 + (rev (!theory'))
1.386 + in case find_first (thy_contains_thm str) startsearch of
1.387 + SOME (thy',_) => ("IsacKnowledge", thy')
1.388 + | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
1.389 + SOME (thyID,_) => ("Isabelle", thyID)
1.390 + | NONE =>
1.391 + raise error ("thy_containing_thm: theorem '"^str^
1.392 + "' not in !theory' above thy '"^thy'^"'"))
1.393 + end;
1.394 +
1.395 +
1.396 +(*.which theory below thy' contains a ruleset;
1.397 +get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
1.398 +(* val (thy', rls') = ("PolyEq.thy", "separate_bdv");
1.399 + *)
1.400 +local infix mem; (*from Isabelle2002*)
1.401 +fun x mem [] = false
1.402 + | x mem (y :: ys) = x = y orelse x mem ys;
1.403 +in
1.404 +fun thy_containing_rls (thy':theory') (rls':rls') =
1.405 + let val rls' = strip_thy rls'
1.406 + val thy' = thyID2theory' thy'
1.407 + (*take thys between "Isac" and thy' not to search #1#*)
1.408 + val dropthys = takewhile [] (not o (curry op= thy') o
1.409 + (#1:theory' * theory -> theory'))
1.410 + (rev (!theory'))
1.411 + val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
1.412 + dropthys
1.413 + (*drop those rulesets which are generated in a theory found in #1#*)
1.414 + val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
1.415 + ((#1 o #2) : rls' * (theory' * rls)
1.416 + -> theory'))
1.417 + (rev (!ruleset'))
1.418 + in case assoc (startsearch, rls') of
1.419 + SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
1.420 + | _ => raise error ("thy_containing_rls : rls '"^rls'^
1.421 + "' not in !rulset' above thy '"^thy'^"'")
1.422 + end;
1.423 +(* val (thy', termop) = (thyID, termop);
1.424 + *)
1.425 +fun thy_containing_cal (thy':theory') termop =
1.426 + let val thy' = thyID2theory' thy'
1.427 + val dropthys = takewhile [] (not o (curry op= thy') o
1.428 + (#1:theory' * theory -> theory'))
1.429 + (rev (!theory'))
1.430 + val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
1.431 + dropthys
1.432 + val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
1.433 + (#1 : calc -> string)) (rev (!calclist'))
1.434 + in case assoc (startsearch, strip_thy termop) of
1.435 + SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
1.436 + | _ => raise error ("thy_containing_rls : rls '"^termop^
1.437 + "' not in !calclist' above thy '"^thy'^"'")
1.438 + end
1.439 +end;
1.440 +
1.441 +(* print_depth 99; map #1 startsearch; print_depth 3;
1.442 + *)
1.443 +
1.444 +(*.packing return-values to matchTheory, contextToThy for xml-generation.*)
1.445 +datatype contthy = (*also an item from KEStore on Browser ......#*)
1.446 + EContThy (*not from KEStore ...........................*)
1.447 + | ContThm of (*a theorem in contex =============*)
1.448 + {thyID : thyID, (*for *2guh in sub-elems here .*)
1.449 + thm : guh, (*theorem in the context .*)
1.450 + applto : term, (*applied to formula ... .*)
1.451 + applat : term, (*... with lhs inserted .*)
1.452 + reword : rew_ord', (*order used for rewrite .*)
1.453 + asms : (term (*asumption instantiated .*)
1.454 + * term) list, (*asumption evaluated .*)
1.455 + lhs : term (*lhs of the theorem ... #*)
1.456 + * term, (*... instantiated .*)
1.457 + rhs : term (*rhs of the theorem ... #*)
1.458 + * term, (*... instantiated .*)
1.459 + result : term, (*resulting from the rewrite .*)
1.460 + resasms : term list, (*... with asms stored .*)
1.461 + asmrls : rls' (*ruleset for evaluating asms .*)
1.462 + }
1.463 + | ContThmInst of (*a theorem with bdvs in contex ======== *)
1.464 + {thyID : thyID, (*for *2guh in sub-elems here .*)
1.465 + thm : guh, (*theorem in the context .*)
1.466 + bdvs : subst, (*bound variables to modify....*)
1.467 + thminst : term, (*... theorem instantiated .*)
1.468 + applto : term, (*applied to formula ... .*)
1.469 + applat : term, (*... with lhs inserted .*)
1.470 + reword : rew_ord', (*order used for rewrite .*)
1.471 + asms : (term (*asumption instantiated .*)
1.472 + * term) list, (*asumption evaluated .*)
1.473 + lhs : term (*lhs of the theorem ... #*)
1.474 + * term, (*... instantiated .*)
1.475 + rhs : term (*rhs of the theorem ... #*)
1.476 + * term, (*... instantiated .*)
1.477 + result : term, (*resulting from the rewrite .*)
1.478 + resasms : term list, (*... with asms stored .*)
1.479 + asmrls : rls' (*ruleset for evaluating asms .*)
1.480 + }
1.481 + | ContRls of (*a rule set in contex ===================== *)
1.482 + {thyID : thyID, (*for *2guh in sub-elems here .*)
1.483 + rls : guh, (*rule set in the context .*)
1.484 + applto : term, (*rewrite this formula .*)
1.485 + result : term, (*resulting from the rewrite .*)
1.486 + asms : term list (*... with asms stored .*)
1.487 + }
1.488 + | ContRlsInst of (*a rule set with bdvs in contex ======= *)
1.489 + {thyID : thyID, (*for *2guh in sub-elems here .*)
1.490 + rls : guh, (*rule set in the context .*)
1.491 + bdvs : subst, (*for bound variables in thms .*)
1.492 + applto : term, (*rewrite this formula .*)
1.493 + result : term, (*resulting from the rewrite .*)
1.494 + asms : term list (*... with asms stored .*)
1.495 + }
1.496 + | ContNOrew of (*no rewrite for thm or rls ============== *)
1.497 + {thyID : thyID, (*for *2guh in sub-elems here .*)
1.498 + thm_rls : guh, (*thm or rls in the context .*)
1.499 + applto : term (*rewrite this formula .*)
1.500 + }
1.501 + | ContNOrewInst of (*no rewrite for some instantiation == *)
1.502 + {thyID : thyID, (*for *2guh in sub-elems here .*)
1.503 + thm_rls : guh, (*thm or rls in the context .*)
1.504 + bdvs : subst, (*for bound variables in thms .*)
1.505 + thminst : term, (*... theorem instantiated .*)
1.506 + applto : term (*rewrite this formula .*)
1.507 + };
1.508 +
1.509 +(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
1.510 + pass other tacs unchanged.*)
1.511 +fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p;
1.512 +
1.513 +(*..*)
1.514 +
1.515 +
1.516 +
1.517 +(*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*)
1.518 +(* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';
1.519 + *)
1.520 +fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =
1.521 + (case applicable_in pos pt tac of
1.522 + Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
1.523 + let val thy = assoc_thy thy'
1.524 + val thm = (norm o #prop o rep_thm o (PureThy.get_thm thy)) thmID
1.525 + (*WN060616 the following must be done on subterm found _IN_ rew_sub
1.526 + val (lhs,rhs) = (dest_equals' o strip_trueprop
1.527 + o Logic.strip_imp_concl) thm
1.528 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
1.529 + val thm' = ren_inst (insts, thm, lhs, f)
1.530 + val (lhs',rhs') = (dest_equals' o strip_trueprop
1.531 + o Logic.strip_imp_concl) thm'
1.532 + val asms = map strip_trueprop (Logic.strip_imp_prems thm)
1.533 + val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
1.534 + *)
1.535 + in ContThm {thyID = theory'2thyID thy',
1.536 + thm = thm2guh (thy_containing_thm thy' thmID) thmID,
1.537 + applto = f,
1.538 + applat = e_term,
1.539 + reword = ord',
1.540 + asms = [](*asms ~~ asms'*),
1.541 + lhs = (e_term, e_term)(*(lhs, lhs')*),
1.542 + rhs = (e_term, e_term)(*(rhs, rhs')*),
1.543 + result = res,
1.544 + resasms = asm,
1.545 + asmrls = id_rls erls}
1.546 + end
1.547 + | Notappl _ =>
1.548 + let val pp = par_pblobj pt p
1.549 + val thy' = get_obj g_domID pt pp
1.550 + val f = case p_ of
1.551 + Frm => get_obj g_form pt p
1.552 + | Res => (fst o (get_obj g_result pt)) p
1.553 + in ContNOrew {thyID = theory'2thyID thy',
1.554 + thm_rls = thm2guh (thy_containing_thm thy' thmID) thmID,
1.555 + applto = f}
1.556 + end)
1.557 +
1.558 +(* val ((pt,p), tac as Rewrite_Inst (subs, (thmID,_))) = ((pt,pos), tac);
1.559 + *)
1.560 + | context_thy (pt, pos as (p,p_))
1.561 + (tac as Rewrite_Inst (subs, (thmID,_))) =
1.562 + (case applicable_in pos pt tac of
1.563 +(* val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
1.564 + f, (res,asm))) = applicable_in p pt tac;
1.565 + *)
1.566 + Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
1.567 + f, (res,(*path to subterm,*)asm))) =>
1.568 + let val thm = (norm o #prop o rep_thm o
1.569 + (PureThy.get_thm (assoc_thy thy'))) thmID
1.570 + val thminst = inst_bdv subst thm
1.571 + (*WN060616 the following must be done on subterm found _IN_ rew_sub
1.572 + val (lhs,rhs) = (dest_equals' o strip_trueprop
1.573 + o Logic.strip_imp_concl) thminst
1.574 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
1.575 + val thm' = ren_inst (insts, thminst, lhs, f)
1.576 + val (lhs',rhs') = (dest_equals' o strip_trueprop
1.577 + o Logic.strip_imp_concl) thm'
1.578 + val asms = map strip_trueprop (Logic.strip_imp_prems thminst)
1.579 + val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
1.580 + *)
1.581 + in ContThmInst {thyID = theory'2thyID thy',
1.582 + thm = thm2guh (thy_containing_thm
1.583 + thy' thmID) thmID,
1.584 + bdvs = subst,
1.585 + thminst = thminst,
1.586 + applto = f,
1.587 + applat = e_term,
1.588 + reword = ord',
1.589 + asms = [](*asms ~~ asms'*),
1.590 + lhs = (e_term, e_term)(*(lhs, lhs')*),
1.591 + rhs = (e_term, e_term)(*(rhs, rhs')*),
1.592 + result = res,
1.593 + resasms = asm,
1.594 + asmrls = id_rls erls}
1.595 + end
1.596 + | Notappl _ =>
1.597 + let val pp = par_pblobj pt p
1.598 + val thy' = get_obj g_domID pt pp
1.599 + val subst = subs2subst (assoc_thy thy') subs
1.600 + val thm = (norm o #prop o rep_thm o
1.601 + (PureThy.get_thm (assoc_thy thy'))) thmID
1.602 + val thminst = inst_bdv subst thm
1.603 + val f = case p_ of
1.604 + Frm => get_obj g_form pt p
1.605 + | Res => (fst o (get_obj g_result pt)) p
1.606 + in ContNOrewInst {thyID = theory'2thyID thy',
1.607 + thm_rls = thm2guh (thy_containing_thm
1.608 + thy' thmID) thmID,
1.609 + bdvs = subst,
1.610 + thminst = thminst,
1.611 + applto = f}
1.612 + end)
1.613 + | context_thy (pt,p) (tac as Rewrite_Set rls') =
1.614 + (case applicable_in p pt tac of
1.615 + Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
1.616 + ContRls {thyID = theory'2thyID thy',
1.617 + rls = rls2guh (thy_containing_rls thy' rls') rls',
1.618 + applto = f,
1.619 + result = res,
1.620 + asms = asm})
1.621 + | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) =
1.622 + (case applicable_in p pt tac of
1.623 + Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>
1.624 + ContRlsInst {thyID = theory'2thyID thy',
1.625 + rls = rls2guh (thy_containing_rls thy' rls') rls',
1.626 + bdvs = subst,
1.627 + applto = f,
1.628 + result = res,
1.629 + asms = asm});
1.630 +
1.631 +(*.get all theorems in a rule set (recursivley containing rule sets).*)
1.632 +fun thm_of_rule Erule = []
1.633 + | thm_of_rule (thm as Thm _) = [thm]
1.634 + | thm_of_rule (Calc _) = []
1.635 + | thm_of_rule (Cal1 _) = []
1.636 + | thm_of_rule (Rls_ rls) = thms_of_rls rls
1.637 +and thms_of_rls Erls = []
1.638 + | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules
1.639 + | thms_of_rls (Seq {rules,...}) = (flat o (map thm_of_rule)) rules
1.640 + | thms_of_rls (Rrls _) = [];
1.641 +(* val Hrls {thy_rls = (_, rls),...} =
1.642 + get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"];
1.643 +> thms_of_rls rls;
1.644 + *)
1.645 +
1.646 +(*. check if a rule is contained in a rule-set (recursivley down in Rls_);
1.647 + this rule can even be a rule-set itself.*)
1.648 +fun contains_rule r rls =
1.649 + let fun find (r, Rls_ rls) = finds (get_rules rls)
1.650 + | find r12 = eq_rule r12
1.651 + and finds [] = false
1.652 + | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
1.653 + in
1.654 + (*writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)
1.655 + finds (get_rules rls)
1.656 + end;
1.657 +
1.658 +(*. try if a rewrite-rule is applicable to a given formula;
1.659 + in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
1.660 +fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
1.661 + if contains_bdv thm
1.662 + then case rewrite_inst_ thy ro erls false subst thm f of
1.663 + SOME (f',_) =>[rule2tac subst thm']
1.664 + | NONE => []
1.665 + else (case rewrite_ thy ro erls false thm f of
1.666 + SOME (f',_) => [rule2tac [] thm']
1.667 + | NONE => [])
1.668 + | try_rew thy _ _ _ f (cal as Calc c) =
1.669 + (case get_calculation_ thy c f of
1.670 + SOME (str, _) => [rule2tac [] cal]
1.671 + | NONE => [])
1.672 + | try_rew thy _ _ _ f (cal as Cal1 c) =
1.673 + (case get_calculation_ thy c f of
1.674 + SOME (str, _) => [rule2tac [] cal]
1.675 + | NONE => [])
1.676 + | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
1.677 +and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
1.678 + distinct (flat (map (try_rew thy ro erls subst f) rules))
1.679 + | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
1.680 + distinct (flat (map (try_rew thy ro erls subst f) rules))
1.681 + | filter_appl_rews thy subst f (Rrls _) = [];
1.682 +
1.683 +(*. decide if a tactic is applicable to a given formula;
1.684 + in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
1.685 +(* val
1.686 + *)
1.687 +fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
1.688 + try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', scrID))))
1.689 + | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
1.690 + try_rew thy (ro, assoc_rew_ord ro) erls [] f
1.691 + (Thm (thmID, assoc_thm' thy thm'))
1.692 + | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) =
1.693 + try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f
1.694 + (Thm (thmID, assoc_thm' thy thm'))
1.695 +
1.696 + | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
1.697 + filter_appl_rews thy [] f (assoc_rls rls')
1.698 + | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
1.699 + filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
1.700 + | atomic_appl_tacs _ _ _ _ tac =
1.701 + (writeln ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
1.702 + []);
1.703 +
1.704 +
1.705 +
1.706 +
1.707 +
1.708 +(*.not only for thydata, but also for thy's etc.*)
1.709 +fun theID2guh (theID:theID) =
1.710 + case length theID of
1.711 + 0 => raise error ("theID2guh: called with theID = "^strs2str' theID)
1.712 + | 1 => part2guh theID
1.713 + | 2 => thy2guh theID
1.714 + | 3 => thypart2guh theID
1.715 + | 4 => let val [isa, thyID, typ, elemID] = theID
1.716 + in case typ of
1.717 + "Theorems" => thm2guh (isa, thyID) elemID
1.718 + | "Rulesets" => rls2guh (isa, thyID) elemID
1.719 + | "Calculations" => cal2guh (isa, thyID) elemID
1.720 + | "Orders" => ord2guh (isa, thyID) elemID
1.721 + | "Theorems" => thy2guh [isa, thyID]
1.722 + | str => raise error ("theID2guh: called with theID = "^
1.723 + strs2str' theID)
1.724 + end
1.725 + | n => raise error ("theID2guh called with theID = "^strs2str' theID);
1.726 +(*.filenames not only for thydata, but also for thy's etc.*)
1.727 +fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
1.728 +
1.729 +fun guh2theID (guh:guh) =
1.730 + let val guh' = explode guh
1.731 + val part = implode (take_fromto 1 4 guh')
1.732 + val isa = implode (take_fromto 5 9 guh')
1.733 + in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
1.734 + then raise error ("guh '"^guh^"' does not begin with \
1.735 + \exp_ | thy_ | pbl_ | met_")
1.736 + else let val chap = case isa of
1.737 + "isab_" => "Isabelle"
1.738 + | "scri_" => "IsacScripts"
1.739 + | "isac_" => "IsacKnowledge"
1.740 + | _ =>
1.741 + raise error ("guh2theID: '"^guh^
1.742 + "' does not have isab_ | scri_ | \
1.743 + \isac_ at position 5..9")
1.744 + val rest = takerest (9, guh')
1.745 + val thyID = takewhile [] (not o (curry op= "-")) rest
1.746 + val rest' = dropuntil (curry op= "-") rest
1.747 + in case implode rest' of
1.748 + "-part" => [chap] : theID
1.749 + | "" => [chap, implode thyID]
1.750 + | "-Theorems" => [chap, implode thyID, "Theorems"]
1.751 + | "-Rulesets" => [chap, implode thyID, "Rulesets"]
1.752 + | "-Operations" => [chap, implode thyID, "Operations"]
1.753 + | "-Orders" => [chap, implode thyID, "Orders"]
1.754 + | _ =>
1.755 + let val sect = implode (take_fromto 1 5 rest')
1.756 + val sect' =
1.757 + case sect of
1.758 + "-thm-" => "Theorems"
1.759 + | "-rls-" => "Rulesets"
1.760 + | "-cal-" => "Operations"
1.761 + | "-ord-" => "Orders"
1.762 + | str =>
1.763 + raise error ("guh2theID: '"^guh^"' has '"^sect^
1.764 + "' instead -thm- | -rls- | \
1.765 + \-cal- | -ord-")
1.766 + in [chap, implode thyID, sect', implode
1.767 + (takerest (5, rest'))]
1.768 + end
1.769 + end
1.770 + end;
1.771 +(*> guh2theID "thy_isac_Biegelinie-Theorems";
1.772 +val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID
1.773 +> guh2theID "thy_scri_ListC-thm-zip_Nil";
1.774 +val it = ["IsacScripts", "ListC", "Theorems", "zip_Nil"] : theID*)
1.775 +
1.776 +fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
1.777 +
1.778 +
1.779 +(*..*)
1.780 +fun guh2rewtac (guh:guh) ([] : subs) =
1.781 + let val [isa, thy, sect, xstr] = guh2theID guh
1.782 + in case sect of
1.783 + "Theorems" => Rewrite (xstr, "")
1.784 + | "Rulesets" => Rewrite_Set xstr
1.785 + | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
1.786 + end
1.787 + | guh2rewtac (guh:guh) subs =
1.788 + let val [isa, thy, sect, xstr] = guh2theID guh
1.789 + in case sect of
1.790 + "Theorems" => Rewrite_Inst (subs, (xstr, ""))
1.791 + | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
1.792 + | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
1.793 + end;
1.794 +(*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
1.795 +val it = Rewrite ("constant_mult_square", "") : tac
1.796 +> guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];
1.797 +val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac
1.798 +> guh2rewtac "thy_isac_Test-rls-Test_simplify" [];
1.799 +val it = Rewrite_Set "Test_simplify" : tac
1.800 +> guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"];
1.801 +val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*)
1.802 +
1.803 +
1.804 +(*.the front-end may request a context for any element of the hierarchy.*)
1.805 +(* val guh = "thy_isac_Test-rls-Test_simplify";
1.806 + *)
1.807 +fun no_thycontext (guh : guh) = (guh2theID guh; false)
1.808 + handle _ => true;
1.809 +
1.810 +(*> has_thycontext "thy_isac_Test";
1.811 +if has_thycontext "thy_isac_Test" then "OK" else "NOTOK";
1.812 + *)
1.813 +
1.814 +
1.815 +
1.816 +(*.get the substitution of bound variables for matchTheory:
1.817 + # lookup the thm|rls' in the script
1.818 + # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
1.819 + # instantiate this subs with the istates env to [(bdv, x),..]
1.820 + # otherwise [].*)
1.821 +(*WN060617 hack assuming that all scripts use only one bound variable
1.822 +and use 'v_' as the formal argument for this bound variable*)
1.823 +(* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);
1.824 + *)
1.825 +fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) =
1.826 + let val theID as [isa, thyID, sect, xstr] = guh2theID guh
1.827 + in case sect of
1.828 + "Theorems" =>
1.829 + let val thm = PureThy.get_thm (assoc_thy (thyID2theory' thyID)) xstr
1.830 + in if contains_bdv thm
1.831 + then let val formal_arg = str2term "v_"
1.832 + val value = subst_atomic env formal_arg
1.833 + in ["(bdv," ^ term2str value ^ ")"]:subs end
1.834 + else []
1.835 + end
1.836 + | "Rulesets" =>
1.837 + let val rules = (get_rules o assoc_rls) xstr
1.838 + in if contain_bdv rules
1.839 + then let val formal_arg = str2term"v_"
1.840 + val value = subst_atomic env formal_arg
1.841 + in ["(bdv,"^term2str value^")"]:subs end
1.842 + else []
1.843 + end
1.844 + end;
1.845 +
1.846 +(* use"ME/rewtools.sml";
1.847 + *)
1.848 +