1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Isac.thy Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,33 @@
1.4 +(* theory collecting all knowledge defined so far
1.5 + WN.11.00
1.6 + *)
1.7 +
1.8 +Isac = Equation + PolyEq + Vect + DiffApp + Test +
1.9 +
1.10 +end
1.11 +
1.12 +(* dependencies alternative to those defined by R.Lang during his thesis:
1.13 +
1.14 + Poly Root
1.15 + |\__________ |
1.16 + | \ |
1.17 + | Rational |
1.18 + | | |
1.19 + PolyEq RatEq RootEq
1.20 + \ / \ /
1.21 + \ / \ /
1.22 + RatPolyEq RatRootEq etc.
1.23 +*)
1.24 +
1.25 +(*
1.26 +Isac = DiffAppl + InsSort + Rationals2 + Rationals + LinArith
1.27 +
1.28 +6.8.02 change to Isabelle2002 caused error -- thy excluded !
1.29 +
1.30 +Proving equations for primrec function(s) "InsSort.foldr" ...
1.31 +GC #1.17.30.54.345.21479: (10 ms)
1.32 +*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
1.33 +*** imposes additional sort constraints on the declared type of the constant
1.34 +*** The error(s) above occurred in definition "InsSort.ins.ins_list_def"
1.35 +*)
1.36 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/LinEq.ML Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,142 @@
2.4 +(* collecting all knowledge for LinearEquations
2.5 + created by: rlang
2.6 + date: 02.10
2.7 + changed by: rlang
2.8 + last change by: rlang
2.9 + date: 02.11.04
2.10 +*)
2.11 +
2.12 +(* remove_thy"LinEq";
2.13 + use_thy"knowledge/Isac";
2.14 +
2.15 + use_thy"knowledge/LinEq";
2.16 +
2.17 + use"ROOT.ML";
2.18 + cd"knowledge";
2.19 +*)
2.20 +
2.21 +"******* LinEq.ML begin *******";
2.22 +
2.23 +(*-------------------- theory -------------------------------------------------*)
2.24 +theory' := overwritel (!theory', [("LinEq.thy",LinEq.thy)]);
2.25 +
2.26 +val lineq_prls = (*3.10.02:just the following order due to subterm evaluation*)
2.27 + append_rls "lineq_prls" e_rls
2.28 + [Calc ("op =",eval_equal "#equal_"),
2.29 + Calc ("Tools.matches",eval_matches ""),
2.30 + Calc ("Tools.lhs" ,eval_lhs ""),
2.31 + Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
2.32 + Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
2.33 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
2.34 + Calc ("Atools.ident",eval_ident "#ident_")
2.35 + ];
2.36 +
2.37 +
2.38 +(*-------------- rules -------------------------------------------------------*)
2.39 +(* ----- erls ----- *)
2.40 +val lineq_erls =
2.41 + merge_rls "lineq_erls" poly_erls
2.42 + (append_rls "op_pred" e_rls
2.43 + [Calc ("op -",eval_binop "#subtract_"),
2.44 + Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in "")
2.45 + (*
2.46 + Don't use
2.47 + Calc ("HOL.divide", eval_cancel "#divide_"),
2.48 + Calc ("Atools.pow" ,eval_binop "#power_"),
2.49 + *)
2.50 + ]);
2.51 +
2.52 +(*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
2.53 +val LinEq_simplify =
2.54 +Rls {id = "LinEq_simplify", preconds = [],
2.55 + rew_ord = ("e_rew_ord",e_rew_ord),
2.56 + erls = e_rls,
2.57 + srls = Erls,
2.58 + calc = [],
2.59 + asm_thm = [],
2.60 + rules = [
2.61 + Thm("lin_isolate_add1",num_str lin_isolate_add1),
2.62 + (* a+bx=0 -> bx=-a *)
2.63 + Thm("lin_isolate_add2",num_str lin_isolate_add2),
2.64 + (* a+ x=0 -> x=-a *)
2.65 + Thm("lin_isolate_div",num_str lin_isolate_div)
2.66 + (* bx=c -> x=c/b *)
2.67 + ],
2.68 + scr = Script ((term_of o the o (parse thy)) "empty_script")
2.69 + }:rls;
2.70 +ruleset' := overwritel (!ruleset',
2.71 + [("LinEq_simplify",LinEq_simplify),
2.72 + ("lineq_erls",lineq_erls)(*FIXXXME:del with rls.rls'*)
2.73 + ]);
2.74 +val poly_simplify =
2.75 + Rls {id = "poly_simplify", preconds = [],
2.76 + rew_ord = ("termlessI",termlessI),
2.77 + erls = lineq_erls,
2.78 + srls = Erls,
2.79 + calc = [],
2.80 + asm_thm = [],
2.81 + rules = [
2.82 + Thm ("real_assoc_1",num_str real_assoc_1),
2.83 + Calc ("op +",eval_binop "#add_"),
2.84 + Calc ("op -",eval_binop "#sub_"),
2.85 + Calc ("op *",eval_binop "#mult_"),
2.86 + (* Dont use
2.87 + Calc ("HOL.divide", eval_cancel "#divide_"),
2.88 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
2.89 + *)
2.90 + Calc ("Atools.pow" ,eval_binop "#power_")
2.91 + ],
2.92 + scr = Script ((term_of o the o (parse thy)) "empty_script")
2.93 + }:rls;
2.94 +ruleset' := overwritel (!ruleset',
2.95 + [("poly_simplify",poly_simplify)]);
2.96 +
2.97 +(*----------------------------- problem types --------------------------------*)
2.98 +(*
2.99 +show_ptyps();
2.100 +(get_pbt ["linear","univariate","equation"]);
2.101 +*)
2.102 +(* ---------linear----------- *)
2.103 +store_pbt
2.104 + (prep_pbt LinEq.thy
2.105 + (["linear","univariate","equation"],
2.106 + [("#Given" ,["equality e_","solveFor v_"]),
2.107 + ("#Where" ,["False",
2.108 + "Not( (lhs e_) is_polyrat_in v_)",
2.109 + "( (lhs e_) has_degree_in v_)=1"]),
2.110 + ("#Find" ,["solutions v_i_"])
2.111 + ],
2.112 + lineq_prls, None,
2.113 + [("LinEq.thy","solve_lin_equation")]));
2.114 +
2.115 +(*-------------- methods-------------------------------------------------------*)
2.116 +(* ansprechen mit "LinEq.thy","solve_univar_equation" *)
2.117 +methods:= overwritel (!methods,
2.118 +[(* ----- 07.10.02---- *)
2.119 +prep_met
2.120 + (("LinEq.thy","solve_lin_equation"),
2.121 + [("#Given" ,["equality e_","solveFor v_"]),
2.122 + ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
2.123 + "( (lhs e_) has_degree_in v_)=1"]),
2.124 + ("#Find" ,["solutions v_i_"])
2.125 + ],
2.126 + {rew_ord'="termlessI",
2.127 + rls'=lineq_erls,
2.128 + srls=e_rls,
2.129 + prls=lineq_prls,
2.130 + calc=[],
2.131 + asm_rls=["LinEq_simplify"],
2.132 + asm_thm=[]},
2.133 + "Script Solve_lin_equation (e_::bool) (v_::real) = \
2.134 + \(let e_ =((Try (Rewrite all_left False)) @@ \
2.135 + \ (Try (Repeat (Rewrite makex1_x False))) @@ \
2.136 + \ (Try (Rewrite_Set expand_binoms False)) @@ \
2.137 + \ (Try (Rewrite_Set make_polynomial False)) @@ \
2.138 + \ (Try (Repeat (Rewrite_Set poly_simplify False)))) e_;\
2.139 + \ e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
2.140 + \ LinEq_simplify True)) @@ \
2.141 + \ (Repeat(Try (Rewrite_Set poly_simplify False)))) e_ \
2.142 + \ in ((Or_to_List e_)::bool list))"
2.143 + )
2.144 +]);
2.145 +"******* LinEq.ML end *******";
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/IsacKnowledge/LinEq.thy Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,48 @@
3.4 +(* theory collecting all knowledge for LinearEquations
3.5 + created by: rlang
3.6 + date: 02.10
3.7 + changed by: rlang
3.8 + last change by: rlang
3.9 + date: 02.10.20
3.10 +*)
3.11 +
3.12 +(*
3.13 + use"knowledge/LinEq.ML";
3.14 + use"LinEq.ML";
3.15 +
3.16 + use"ROOT.ML";
3.17 + cd"knowledge";
3.18 +
3.19 +*)
3.20 +
3.21 +LinEq = Poly +
3.22 +
3.23 +(*-------------------- consts------------------------------------------------*)
3.24 +consts
3.25 + Solve'_lin'_equation
3.26 + :: "[bool,real, \
3.27 + \ bool list] => bool list"
3.28 + ("((Script Solve'_lin'_equation (_ _ =))// \
3.29 + \ (_))" 9)
3.30 +
3.31 +(*-------------------- rules -------------------------------------------------*)
3.32 +rules
3.33 +(*-- normalize --*)
3.34 + all_left
3.35 + "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
3.36 + makex1_x
3.37 + "a^^^1 = a"
3.38 + real_assoc_1
3.39 + "a+(b+c) = a+b+c"
3.40 + real_assoc_2
3.41 + "a*(b*c) = a*b*c"
3.42 +
3.43 +(*-- solve --*)
3.44 + lin_isolate_add1
3.45 + "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
3.46 + lin_isolate_add2
3.47 + "(a + bdv = 0) = ( bdv = (-1)*a)"
3.48 + lin_isolate_div
3.49 + "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
3.50 +end
3.51 +