1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Sep 06 15:09:37 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Sep 06 15:53:18 2010 +0200
     1.3 @@ -19,15 +19,15 @@
     1.4  axioms
     1.5  (*-- normalize --*)
     1.6    (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
     1.7 -  all_left          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
     1.8 -  makex1_x          "a^^^1  = a"  
     1.9 -  real_assoc_1      "a+(b+c) = a+b+c"
    1.10 -  real_assoc_2      "a*(b*c) = a*b*c"
    1.11 +  all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
    1.12 +  makex1_x:          "a^^^1  = a"  
    1.13 +  real_assoc_1:      "a+(b+c) = a+b+c"
    1.14 +  real_assoc_2:      "a*(b*c) = a*b*c"
    1.15  
    1.16  (*-- solve --*)
    1.17 -  lin_isolate_add1  "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
    1.18 -  lin_isolate_add2  "(a +   bdv = 0) = (  bdv = (-1)*a)"
    1.19 -  lin_isolate_div   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
    1.20 +  lin_isolate_add1:  "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
    1.21 +  lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)"
    1.22 +  lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
    1.23  
    1.24  ML {*
    1.25  val thy = @{theory};
    1.26 @@ -89,12 +89,12 @@
    1.27  		Calc ("op *",eval_binop "#mult_"),
    1.28  		(*  Dont use  
    1.29  		 Calc ("HOL.divide", eval_cancel "#divide_e"),		
    1.30 -		 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
    1.31 +		 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.32  		 *)
    1.33  		Calc ("Atools.pow" ,eval_binop "#power_")
    1.34  		],
    1.35 -       scr = Script ((term_of o the o (parse thy)) "empty_script")
    1.36 -       }:rls);
    1.37 +       scr = EmptyScr}:rls);
    1.38 +
    1.39  ruleset' := overwritelthy @{theory} (!ruleset',
    1.40  			  [("LinPoly_simplify",LinPoly_simplify)]);
    1.41  
    1.42 @@ -114,8 +114,7 @@
    1.43  	      Thm("lin_isolate_div",num_str @{thm lin_isolate_div})    
    1.44  	      (*   bx=c -> x=c/b *)  
    1.45  	      ],
    1.46 -     scr = Script ((term_of o the o (parse thy)) "empty_script")
    1.47 -     }:rls);
    1.48 +     scr = EmptyScr}:rls);
    1.49  ruleset' := overwritelthy @{theory} (!ruleset',
    1.50  			[("LinEq_simplify",LinEq_simplify)]);
    1.51  
    1.52 @@ -124,6 +123,7 @@
    1.53  show_ptyps(); 
    1.54  (get_pbt ["linear","univariate","equation"]);
    1.55  *)
    1.56 +
    1.57  (* ---------linear----------- *)
    1.58  store_pbt
    1.59   (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
    1.60 @@ -152,33 +152,27 @@
    1.61  store_met
    1.62  (prep_met thy "met_eq_lin" [] e_metID
    1.63   (["LinEq","solve_lineq_equation"],
    1.64 -   [("#Given" ,["equality e_e","solveFor v_v"]),
    1.65 -    ("#Where" ,["Not( (lhs e_e) is_polyrat_in v_v)",
    1.66 -                "( (lhs e_e)  has_degree_in v_v)=1"]),
    1.67 -    ("#Find"  ,["solutions v_i"])
    1.68 +   [("#Given", ["equality e_e", "solveFor v_v"]),
    1.69 +    ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)",
    1.70 +                "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.71 +    ("#Find",  ["solutions v_i"])
    1.72     ],
    1.73 -   {rew_ord'="termlessI",
    1.74 -    rls'=LinEq_erls,
    1.75 -    srls=e_rls,
    1.76 -    prls=LinEq_prls,
    1.77 -    calc=[],
    1.78 -    crls=LinEq_crls, nrls=norm_Poly(*,
    1.79 -    asm_rls=[],
    1.80 -    asm_thm=[("lin_isolate_div","")]*)},
    1.81 -    "Script Solve_lineq_equation (e_e::bool) (v_::real) =                 " ^
    1.82 -    "(let e_e =((Try         (Rewrite     all_left            False)) @@  " ^ 
    1.83 -    "          (Try (Repeat (Rewrite     makex1_x           False))) @@  " ^ 
    1.84 -    "          (Try         (Rewrite_Set expand_binoms       False)) @@  " ^ 
    1.85 -    "          (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)]           " ^
    1.86 -    "                                 make_ratpoly_in    False)))    @@  " ^
    1.87 -    "          (Try (Repeat (Rewrite_Set LinPoly_simplify      False)))) e_;" ^
    1.88 -    "     e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)]                  " ^
    1.89 -    "                                          LinEq_simplify True)) @@  " ^
    1.90 +   {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
    1.91 +    calc=[], crls=LinEq_crls, nrls=norm_Poly},
    1.92 +    "Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
    1.93 +    "(let e_e =((Try         (Rewrite      all_left           False)) @@   " ^ 
    1.94 +    "           (Try (Repeat (Rewrite     makex1_x            False))) @@  " ^ 
    1.95 +    "           (Try         (Rewrite_Set expand_binoms       False)) @@   " ^ 
    1.96 +    "           (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)]          " ^
    1.97 +    "                                 make_ratpoly_in    False)))    @@    " ^
    1.98 +    "           (Try (Repeat (Rewrite_Set LinPoly_simplify      False))))e_e;" ^
    1.99 +    "     e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)]                  " ^
   1.100 +    "                                     LinEq_simplify True)) @@  " ^
   1.101      "            (Repeat(Try (Rewrite_Set LinPoly_simplify     False)))) e_e " ^
   1.102      " in ((Or_to_List e_e)::bool list))"
   1.103   ));
   1.104 -"******* LinEq.ML end *******";
   1.105  get_met ["LinEq","solve_lineq_equation"];
   1.106 +
   1.107  *}
   1.108  
   1.109  end