1.1 --- a/src/sml/IsacKnowledge/Poly.ML Tue Aug 29 13:30:35 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Poly.ML Wed Aug 30 12:16:45 2006 +0200
1.3 @@ -1353,6 +1353,8 @@
1.4 Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
1.5 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1.6
1.7 + Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.8 +
1.9 Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.10 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.11 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.12 @@ -1393,8 +1395,7 @@
1.13
1.14 Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.15 Thm ("real_mult_0",num_str real_mult_0),(*"0 * z = 0"*)
1.16 - Thm ("real_add_zero_left",num_str real_add_zero_left)
1.17 - (*"0 + z = z"*)
1.18 + Thm ("real_add_zero_left",num_str real_add_zero_left)(*0 + z = z*)
1.19
1.20 (*Rls_ order_add_rls_*)
1.21 ],
2.1 --- a/src/sml/IsacKnowledge/Rational.ML Tue Aug 29 13:30:35 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Rational.ML Wed Aug 30 12:16:45 2006 +0200
2.3 @@ -2806,8 +2806,8 @@
2.4 list); (*derivation from given term to normalform
2.5 in reverse order with sym_thm;
2.6 (#) could be extracted from here by (map #1)*).*)
2.7 -(* val {rules=rules,rew_ord=(_,ro),...} =
2.8 - rep_rls (assoc_rls "make_polynomial") (*USE ALWAYS, SEE val cancel_p*);
2.9 +(* val {rules, rew_ord=(_,ro),...} =
2.10 + rep_rls (assoc_rls "rev_rew_p") (*USE ALWAYS, SEE val cancel_p*);
2.11 val (thy, eval_rls, ro) =(Rational.thy, Atools_erls, ro) (*..val cancel_p*);
2.12 val t = t;
2.13 *)
2.14 @@ -2821,8 +2821,9 @@
2.15 val rs = (distinct_Thm o (map #1)) der
2.16 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
2.17 "sym_real_mult_0",
2.18 - "sym_real_mult_1"]) rs
2.19 - in (t,t'',[rs(*here only _ONE_ WN060925 why?*)],der) end;
2.20 + "sym_real_mult_1"
2.21 + (*..insufficient,eg.make_Polynomial*)])rs
2.22 + in (t,t'',[rs(*here only _ONE_ to ease locate_rule*)],der) end;
2.23
2.24 (*.locate_rule = fn : rule list -> term -> rule
2.25 -> (rule * (term * term list) option) list.
3.1 --- a/src/sml/ME/ctree.sml Tue Aug 29 13:30:35 2006 +0200
3.2 +++ b/src/sml/ME/ctree.sml Wed Aug 30 12:16:45 2006 +0200
3.3 @@ -514,9 +514,15 @@
3.4 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
3.5 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
3.6
3.7 +(*
3.8 fun Thm2Rewrite (Thm (thmID,_)) = Rewrite_Set thmID
3.9 | Thm2Rewrite rule =
3.10 raise error ("Thm2Rewrite: called with '" ^ rule2str rule ^ "'");
3.11 +*)
3.12 +fun rule2tac (Thm (thmID, thm)) = Rewrite (thmID, string_of_thm thm)
3.13 + | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
3.14 + | rule2tac rule =
3.15 + raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
3.16
3.17
3.18
4.1 --- a/src/sml/ME/rewtools.sml Tue Aug 29 13:30:35 2006 +0200
4.2 +++ b/src/sml/ME/rewtools.sml Wed Aug 30 12:16:45 2006 +0200
4.3 @@ -17,9 +17,10 @@
4.4 (term2str t')^", "^(terms2str a)^"))";
4.5 fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
4.6 val deriv2str = trtas2str;
4.7 -fun rta2str (r,(t,a)) = "\n("^(rule2str r)^", ("^
4.8 +fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^
4.9 (term2str t)^", "^(terms2str a)^"))";
4.10 fun rtas2str rtas = (strs2str o (map rta2str)) rtas;
4.11 +val deri2str = rtas2str;
4.12
4.13
4.14 (*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)
4.15 @@ -84,55 +85,8 @@
4.16 WN060825 too complicated for the intended use by cancel_, common_nominator_
4.17 and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
4.18 -- replaced below*)
4.19 -fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
4.20 - let
4.21 - datatype switch = Appl | Noap;
4.22 - fun rew_once rts t Noap [] =
4.23 - (case goal of
4.24 - None => rts
4.25 - | Some g =>
4.26 - raise error ("make_deriv: no derivation for "^(term2str t)))
4.27 - | rew_once rts t Appl [] =
4.28 - (*(case rs of Rls _ =>*) rew_once rts t Noap rs
4.29 - (*| Seq _ => rts) FIXXXXXME 14.3.03*)
4.30 - | rew_once rts t apno rs' =
4.31 - (case goal of
4.32 - None => rew_or_calc rts t apno rs'
4.33 - | Some g =>
4.34 - if g = t then rts
4.35 - else rew_or_calc rts t apno rs')
4.36 - and rew_or_calc rts t apno (rrs' as (r::rs')) =
4.37 - case r of
4.38 - Thm (thmid, tm) =>
4.39 - (if not (!trace_rewrite) then () else
4.40 - writeln ("### trying thm '" ^ thmid ^ "'");
4.41 - case rewrite_ thy ro erls true tm t of
4.42 - None => rew_once rts t apno rs'
4.43 - | Some (t',a') =>
4.44 - (if ! trace_rewrite
4.45 - then writeln ("### rewrites to: "^(term2str t')) else();
4.46 - rew_once (rts@[(t,r,(t',a'))]) t' Appl rrs'))
4.47 - | Calc (c as (op_,_)) =>
4.48 - let val _ = if not (!trace_rewrite) then () else
4.49 - writeln ("### trying calc. '" ^ op_ ^ "'")
4.50 - val t = app_num_tr'2 t
4.51 - in case get_calculation_ thy c t of
4.52 - None => rew_once rts t apno rs'
4.53 - | Some (thmid, tm) =>
4.54 - (let val Some (t',a') = rewrite_ thy ro erls true tm t
4.55 - val _ = if not (!trace_rewrite) then () else
4.56 - writeln("### calc. to: " ^ (term2str t'))
4.57 - val r' = Thm (thmid, tm)
4.58 - in rew_once (rts@[(t,r',(t',a'))]) t' Appl rrs' end)
4.59 - handle _ => raise error "derive_norm, Calc: no rewrite"
4.60 - end
4.61 - | Rls_ rls =>
4.62 - (case rewrite_set_ thy true rls t of
4.63 - None => rew_once rts t apno rs'
4.64 - | Some (t',a') =>
4.65 - rew_once (rts @ [(t,r,(t',a'))]) t' Appl rrs');
4.66 -
4.67 - in rew_once [] tt Noap rs end;
4.68 +(* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
4.69 + *)
4.70 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
4.71 let datatype switch = Appl | Noap
4.72 fun rew_once lim rts t Noap [] =
4.73 @@ -249,6 +203,8 @@
4.74
4.75 (*version for reverse rewrite used before 040214*)
4.76 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
4.77 +(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, None, t');
4.78 + *)
4.79 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
4.80 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
4.81 (*
4.82 @@ -257,11 +213,15 @@
4.83 *)
4.84
4.85 fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
4.86 + | eq_Thm (Thm (id1,_), _) = false
4.87 + | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
4.88 + | eq_Thm (Rls_ r1, _) = false
4.89 | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^
4.90 (rule2str r1)^"' '"^(rule2str r2)^"'");
4.91 fun distinct_Thm r = gen_distinct eq_Thm r;
4.92
4.93 -fun eq_Thms thmIDs thm = (id_of_thm thm) mem thmIDs;
4.94 +fun eq_Thms thmIDs thm = ((id_of_thm thm) mem thmIDs)
4.95 + handle _ => false;
4.96
4.97
4.98
5.1 --- a/src/sml/ME/solve.sml Tue Aug 29 13:30:35 2006 +0200
5.2 +++ b/src/sml/ME/solve.sml Wed Aug 30 12:16:45 2006 +0200
5.3 @@ -501,7 +501,7 @@
5.4 *)
5.5 fun rul_terms_2nds nds t [] = nds
5.6 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
5.7 - (append_atomic [] e_istate t (Thm2Rewrite rule) res Complete EmptyPtree) ::
5.8 + (append_atomic [] e_istate t (rule2tac rule) res Complete EmptyPtree) ::
5.9 (rul_terms_2nds nds t' rts);
5.10
5.11
6.1 --- a/src/smltest/IsacKnowledge/rational.sml Tue Aug 29 13:30:35 2006 +0200
6.2 +++ b/src/smltest/IsacKnowledge/rational.sml Wed Aug 30 12:16:45 2006 +0200
6.3 @@ -2039,11 +2039,12 @@
6.4 interSteps 1 ([1,2],Res);
6.5 val ((pt,p),_) = get_calc 1; show_pt pt;
6.6
6.7 -(*WN060823 cancel_p_ init_state does not terminate, see Rational.ML
6.8 - @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
6.9 interSteps 1 ([1,2,1],Res);
6.10 val ((pt,p),_) = get_calc 1; show_pt pt;
6.11 -*)
6.12 +val newnds = children (get_nd pt [1,2,1]) (*see "fun detailrls"*);
6.13 +if length newnds = 12 then ()
6.14 +else raise error "rational.sml: interSteps cancel_p rev_rew_p";
6.15 +
6.16
6.17 "-------- investigate rulesets for cancel_p ----------------------";
6.18 "-------- investigate rulesets for cancel_p ----------------------";
6.19 @@ -2058,6 +2059,7 @@
6.20 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
6.21 val Some (tt',asm) = rewrite_set_ thy false make_polynomial tt;
6.22 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
6.23 +
6.24 "----- with make_deriv";
6.25 val Some (tt, _) = factout_p_ Isac.thy t; term2str tt =
6.26 "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
6.27 @@ -2078,6 +2080,7 @@
6.28 print_depth 99; map (term2str o #1) der; print_depth 3;
6.29 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
6.30 print_depth 99; map (rule2str o #2) der; print_depth 3;
6.31 +print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
6.32
6.33 val der = make_deriv thy Atools_erls rules ro None
6.34 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");