1.1 --- a/src/Tools/isac/IsacKnowledge/Isac.ML Fri Aug 20 14:58:43 2010 +0200
1.2 +++ b/src/Tools/isac/IsacKnowledge/Isac.ML Fri Aug 20 16:21:41 2010 +0200
1.3 @@ -16,7 +16,7 @@
1.4 local
1.5 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
1.6 (map (thms_of_rls o #2 o #2))) (!ruleset');
1.7 - val isacthms = (flat o (map (thms_of o #2))) (!theory');
1.8 + val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
1.9 in
1.10 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
1.11 end;
2.1 --- a/src/Tools/isac/Isac_Mathengine.thy Fri Aug 20 14:58:43 2010 +0200
2.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Fri Aug 20 16:21:41 2010 +0200
2.3 @@ -37,20 +37,22 @@
2.4 use "ME/ptyps.sml"
2.5 use "ME/generate.sml"
2.6 use "ME/calchead.sml"
2.7 -
2.8 +use "ME/appl.sml"
2.9 +use "ME/rewtools.sml"
2.10
2.11 ML {*
2.12 -cterm_of;
2.13 -111;
2.14 -member op = [1,2,3] 2;
2.15 +PureThy.all_thms_of;
2.16 *}
2.17
2.18 +use "ME/script.sml"
2.19 +
2.20 +ML {*
2.21 +111;
2.22 +*}
2.23 +
2.24
2.25
2.26 (*
2.27 -use "ME/appl.sml"
2.28 -use "ME/rewtools.sml"
2.29 -use "ME/script.sml"
2.30 use "ME/solve.sml"
2.31 use "ME/inform.sml"
2.32 use "ME/mathengine.sml"
3.1 --- a/src/Tools/isac/ME/appl.sml Fri Aug 20 14:58:43 2010 +0200
3.2 +++ b/src/Tools/isac/ME/appl.sml Fri Aug 20 16:21:41 2010 +0200
3.3 @@ -1,6 +1,9 @@
3.4 (* use"ME/appl.sml";
3.5 use"appl.sml";
3.6 - *)
3.7 +
3.8 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.9 + 10 20 30 40 50 60 70 80
3.10 +*)
3.11 val e_cterm' = empty_cterm';
3.12
3.13
4.1 --- a/src/Tools/isac/ME/calchead.sml Fri Aug 20 14:58:43 2010 +0200
4.2 +++ b/src/Tools/isac/ME/calchead.sml Fri Aug 20 16:21:41 2010 +0200
4.3 @@ -512,8 +512,7 @@
4.4
4.5 (* select an item in oris, notyet input in itms
4.6 (precondition: in itms are only Cor, Sup, Inc) *)
4.7 -local
4.8 -infix mem;
4.9 +local infix mem;
4.10 fun x mem [] = false
4.11 | x mem (y :: ys) = x = y orelse x mem ys;
4.12 in
4.13 @@ -1553,8 +1552,7 @@
4.14
4.15 (*.combine itms from pbl + met and complete them wrt. pbt.*)
4.16 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
4.17 -local
4.18 -infix mem;
4.19 +local infix mem;
4.20 fun x mem [] = false
4.21 | x mem (y :: ys) = x = y orelse x mem ys;
4.22 in
4.23 @@ -1573,8 +1571,7 @@
4.24
4.25
4.26 (*.complete model and guard of a calc-head .*)
4.27 -local
4.28 -infix mem;
4.29 +local infix mem;
4.30 fun x mem [] = false
4.31 | x mem (y :: ys) = x = y orelse x mem ys;
4.32 in
4.33 @@ -1712,8 +1709,7 @@
4.34
4.35 (*.get the values from oris; handle the term list w.r.t. penv.*)
4.36
4.37 -local
4.38 -infix mem;
4.39 +local infix mem;
4.40 fun x mem [] = false
4.41 | x mem (y :: ys) = x = y orelse x mem ys;
4.42 in
5.1 --- a/src/Tools/isac/ME/ptyps.sml Fri Aug 20 14:58:43 2010 +0200
5.2 +++ b/src/Tools/isac/ME/ptyps.sml Fri Aug 20 16:21:41 2010 +0200
5.3 @@ -833,8 +833,7 @@
5.4 (9,[1,2],"#undef",Const (#,#),[# $ #]),
5.5 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
5.6
5.7 -local
5.8 -infix mem; (*from Isabelle2002*)
5.9 +local infix mem; (*from Isabelle2002*)
5.10 fun x mem [] = false
5.11 | x mem (y :: ys) = x = y orelse x mem ys;
5.12 in
6.1 --- a/src/Tools/isac/ME/rewtools.sml Fri Aug 20 14:58:43 2010 +0200
6.2 +++ b/src/Tools/isac/ME/rewtools.sml Fri Aug 20 16:21:41 2010 +0200
6.3 @@ -25,17 +25,18 @@
6.4
6.5 (*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)
6.6 fun sym_thm thm =
6.7 - let
6.8 - val {sign_ref = sign_ref, der = der, maxidx = maxidx,
6.9 - shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} =
6.10 - rep_thm_G thm;
6.11 - val (lhs,rhs) = (dest_equals' o strip_trueprop
6.12 - o Logic.strip_imp_concl) prop;
6.13 - val prop' = case strip_imp_prems' prop of
6.14 - NONE => Trueprop $ (mk_equality (rhs, lhs))
6.15 - | SOME cs =>
6.16 - ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
6.17 - in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;
6.18 + let
6.19 + val (deriv, {thy_ref = thy_ref, tags = tags, maxidx = maxidx,
6.20 + shyps = shyps, hyps = hyps, tpairs = tpairs,
6.21 + prop = prop}) =
6.22 + rep_thm_G thm;
6.23 + val (lhs,rhs) = (dest_equals' o strip_trueprop
6.24 + o Logic.strip_imp_concl) prop;
6.25 + val prop' = case strip_imp_prems' prop of
6.26 + NONE => Trueprop $ (mk_equality (rhs, lhs))
6.27 + | SOME cs =>
6.28 + ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
6.29 + in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
6.30 (*
6.31 (sym RS real_mult_div_cancel1) handle e => print_exn e;
6.32 Exception THM 1 raised:
6.33 @@ -341,7 +342,7 @@
6.34 (*.lookup the missing theorems in some thy (of Isabelle).*)
6.35 fun make_isa missthms thy =
6.36 map (pair (theory2thyID thy))
6.37 - (curry (gen_inter eq_thmI) missthms (thms_of thy))
6.38 + ((inter eq_thmI) missthms (PureThy.all_thms_of thy))
6.39 : (thyID * (thmID * Thm.thm)) list;
6.40
6.41 (*.separate handling of sym_thms.*)
6.42 @@ -369,7 +370,7 @@
6.43 val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
6.44 *)
6.45 fun thy_contains_thm (str:xstring) (_, thy) =
6.46 - member str (map (strip_thy o fst) (thms_of thy));
6.47 + member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str;
6.48 (* val (thy', str) = ("Isac.thy", "real_mult_minus1");
6.49 val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
6.50 *)
6.51 @@ -393,6 +394,10 @@
6.52 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
6.53 (* val (thy', rls') = ("PolyEq.thy", "separate_bdv");
6.54 *)
6.55 +local infix mem; (*from Isabelle2002*)
6.56 +fun x mem [] = false
6.57 + | x mem (y :: ys) = x = y orelse x mem ys;
6.58 +in
6.59 fun thy_containing_rls (thy':theory') (rls':rls') =
6.60 let val rls' = strip_thy rls'
6.61 val thy' = thyID2theory' thy'
6.62 @@ -427,7 +432,8 @@
6.63 SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
6.64 | _ => raise error ("thy_containing_rls : rls '"^termop^
6.65 "' not in !calclist' above thy '"^thy'^"'")
6.66 - end;
6.67 + end
6.68 +end;
6.69
6.70 (* print_depth 99; map #1 startsearch; print_depth 3;
6.71 *)
6.72 @@ -512,7 +518,7 @@
6.73 (case applicable_in pos pt tac of
6.74 Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
6.75 let val thy = assoc_thy thy'
6.76 - val thm = (norm o #prop o rep_thm o (get_thm thy)) thmID
6.77 + val thm = (norm o #prop o rep_thm o (PureThy.get_thm thy)) thmID
6.78 (*WN060616 the following must be done on subterm found _IN_ rew_sub
6.79 val (lhs,rhs) = (dest_equals' o strip_trueprop
6.80 o Logic.strip_imp_concl) thm
6.81 @@ -557,7 +563,7 @@
6.82 Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
6.83 f, (res,(*path to subterm,*)asm))) =>
6.84 let val thm = (norm o #prop o rep_thm o
6.85 - (get_thm (assoc_thy thy'))) thmID
6.86 + (PureThy.get_thm (assoc_thy thy'))) thmID
6.87 val thminst = inst_bdv subst thm
6.88 (*WN060616 the following must be done on subterm found _IN_ rew_sub
6.89 val (lhs,rhs) = (dest_equals' o strip_trueprop
6.90 @@ -589,7 +595,7 @@
6.91 val thy' = get_obj g_domID pt pp
6.92 val subst = subs2subst (assoc_thy thy') subs
6.93 val thm = (norm o #prop o rep_thm o
6.94 - (get_thm (assoc_thy thy'))) thmID
6.95 + (PureThy.get_thm (assoc_thy thy'))) thmID
6.96 val thminst = inst_bdv subst thm
6.97 val f = case p_ of
6.98 Frm => get_obj g_form pt p
6.99 @@ -817,7 +823,7 @@
6.100 let val theID as [isa, thyID, sect, xstr] = guh2theID guh
6.101 in case sect of
6.102 "Theorems" =>
6.103 - let val thm = get_thm (assoc_thy (thyID2theory' thyID)) xstr
6.104 + let val thm = PureThy.get_thm (assoc_thy (thyID2theory' thyID)) xstr
6.105 in if contains_bdv thm
6.106 then let val formal_arg = str2term "v_"
6.107 val value = subst_atomic env formal_arg
7.1 --- a/test/Tools/isac/ME/rewtools.sml Fri Aug 20 14:58:43 2010 +0200
7.2 +++ b/test/Tools/isac/ME/rewtools.sml Fri Aug 20 16:21:41 2010 +0200
7.3 @@ -42,13 +42,13 @@
7.4 val ancestors = (#ancestors o rep_theory) first_isac_thy;
7.5 length ancestors;
7.6 print_depth 99; map theory2theory' ancestors; print_depth 3;
7.7 -val isabthms = (flat o (map thms_of)) ancestors;
7.8 +val isabthms = (flat o (map PureThy.all_thms_of)) ancestors;
7.9 length isabthms;
7.10
7.11 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset');
7.12 (*thms from rulesets*)
7.13 val isacrlsthms = ((map rep_thm_G') o flat o
7.14 - (map (thms_of_rls o #2 o #2))) (!ruleset');
7.15 + (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
7.16 length isacrlsthms;
7.17 (*takes a few seconds...
7.18 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
7.19 @@ -60,8 +60,8 @@
7.20
7.21 (!theory');
7.22 map #2 (!theory');
7.23 -map (thms_of o #2) (!theory');
7.24 -val isacthms = (flat o (map (thms_of o #2))) (!theory');
7.25 +map (PureThy.all_thms_of o #2) (!theory');
7.26 +val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
7.27 (*takes a few seconds...
7.28 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
7.29 length rlsthmsNOTisac;
7.30 @@ -71,22 +71,22 @@
7.31 ...*)
7.32
7.33 "----- for 'fun make_isab_thm_thy'";
7.34 -gen_inter eq_thmI (isacrlsthms, (thms_of (nth 1 ancestors)));
7.35 -gen_inter eq_thmI;
7.36 -curry (gen_inter eq_thmI);
7.37 -curry (gen_inter eq_thmI) isacrlsthms;
7.38 +inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));
7.39 +inter eq_thmI;
7.40 +(inter eq_thmI);
7.41 +(inter eq_thmI) isacrlsthms;
7.42 (*takes a few seconds...
7.43 -curry (gen_inter eq_thmI) isacrlsthms (thms_of (nth 9 ancestors));
7.44 +curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));
7.45
7.46 val thy = (nth 52 ancestors);
7.47 -val sec = (curry (gen_inter eq_thmI) isacrlsthms o thms_of) (nth 52 ancestors);
7.48 -length (thms_of (nth 9 ancestors));
7.49 +val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);
7.50 +length (PureThy.all_thms_of (nth 9 ancestors));
7.51 length sec;
7.52 ...*)
7.53
7.54 (*takes 1 minute...
7.55 print_depth 99;
7.56 -map (curry (gen_inter eq_thmI) rlsthmsNOTisac o thms_of) ancestors;
7.57 +map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
7.58 print_depth 3;
7.59 *)
7.60
8.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Fri Aug 20 14:58:43 2010 +0200
8.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Fri Aug 20 16:21:41 2010 +0200
8.3 @@ -51,7 +51,7 @@
8.4 val thy = assoc_thy (thyID2theory' thy');
8.5
8.6 "collect_thms thy'------------------------------------------------";
8.7 -(thms_of thy);
8.8 +(PureThy.all_thms_of thy);
8.9
8.10 (apfst single) ("Integrate.integral_var", integral_var);
8.11
8.12 @@ -63,7 +63,7 @@
8.13
8.14 makeHthm ("IsacKnowledge",thy') ("Integrate.integral_var", integral_var);
8.15 (makeHthm ("IsacKnowledge",thy')) ("Integrate.integral_var", integral_var);
8.16 -map (makeHthm ("IsacKnowledge",thy')) (thms_of thy);
8.17 +map (makeHthm ("IsacKnowledge",thy')) (PureThy.all_thms_of thy);
8.18 collect_thms' ("IsacKnowledge",thy');
8.19
8.20 "collect_rlss thy'------------------------------------------------";