wneuper/isa: src/Tools/isac/Knowledge/LinEq.thy@6ea6d9c377a0

     1 (*. (c) by Richard Lang, 2003 .*)

     2 (* theory collecting all knowledge for LinearEquations

     3    created by: rlang

     4          date: 02.10

     5    changed by: rlang

     6    last change by: rlang

     7              date: 02.10.20

     8 *)

    10 theory LinEq imports Poly Equation begin

    12 axiomatization where

    13 (*-- normalise --*)

    14   (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)

    15   all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and

    16   makex1_x:          "a^^^1  = a" and

    17   real_assoc_1:      "a+(b+c) = a+b+c" and

    18   real_assoc_2:      "a*(b*c) = a*b*c" and

    20 (*-- solve --*)

    21   lin_isolate_add1:  "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and

    22   lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)" and

    23   lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"

    25 ML \<open>

    26 val thy = @{theory};

    28 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)

    29   Rule.append_rls "LinEq_prls" Rule.e_rls

    30 	     [Rule.Calc ("HOL.eq",eval_equal "#equal_"),

    31 	      Rule.Calc ("Tools.matches", Tools.eval_matches ""),

    32 	      Rule.Calc ("Tools.lhs"    , Tools.eval_lhs ""),

    33 	      Rule.Calc ("Tools.rhs"    , Tools.eval_rhs ""),

    34 	      Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),

    35  	      Rule.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),

    36 	      Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),

    37 	      Rule.Calc ("Atools.ident",eval_ident "#ident_"),

    38 	      Rule.Thm ("not_true",TermC.num_str @{thm not_true}),

    39 	      Rule.Thm ("not_false",TermC.num_str @{thm not_false}),

    40 	      Rule.Thm ("and_true",TermC.num_str @{thm and_true}),

    41 	      Rule.Thm ("and_false",TermC.num_str @{thm and_false}),

    42 	      Rule.Thm ("or_true",TermC.num_str @{thm or_true}),

    43 	      Rule.Thm ("or_false",TermC.num_str @{thm or_false})

    44               ];

    45 (* ----- erls ----- *)

    46 val LinEq_crls =

    47    Rule.append_rls "LinEq_crls" poly_crls

    48    [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})

    49     (*

    50      Don't use

    51      Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),

    52      Rule.Calc ("Atools.pow" ,eval_binop "#power_"),

    53      *)

    54     ];

    56 (* ----- crls ----- *)

    57 val LinEq_erls =

    58    Rule.append_rls "LinEq_erls" Poly_erls

    59    [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})

    60     (*

    61      Don't use

    62      Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),

    63      Rule.Calc ("Atools.pow" ,eval_binop "#power_"),

    64      *)

    65     ];

    66 \<close>

    67 setup \<open>KEStore_Elems.add_rlss

    68   [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))]\<close>

    69 ML \<open>

    71 val LinPoly_simplify = prep_rls'(

    72   Rule.Rls {id = "LinPoly_simplify", preconds = [],

    73        rew_ord = ("termlessI",termlessI),

    74        erls = LinEq_erls,

    75        srls = Rule.Erls,

    76        calc = [], errpatts = [],

    77        rules = [

    78 		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),

    79 		Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),

    80 		Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),

    81 		Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),

    82 		(*  Dont use

    83 		 Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),

    84 		 Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),

    85 		 *)

    86 		Rule.Calc ("Atools.pow" ,eval_binop "#power_")

    87 		],

    88        scr = Rule.EmptyScr});

    89 \<close>

    90 setup \<open>KEStore_Elems.add_rlss

    91   [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))]\<close>

    92 ML \<open>

    94 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)

    95 val LinEq_simplify = prep_rls'(

    96 Rule.Rls {id = "LinEq_simplify", preconds = [],

    97      rew_ord = ("e_rew_ord", Rule.e_rew_ord),

    98      erls = LinEq_erls,

    99      srls = Rule.Erls,

   100      calc = [], errpatts = [],

   101      rules = [

   102 	      Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}),

   103 	      (* a+bx=0 -> bx=-a *)

   104 	      Rule.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}),

   105 	      (* a+ x=0 ->  x=-a *)

   106 	      Rule.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div})

   107 	      (*   bx=c -> x=c/b *)

   108 	      ],

   109      scr = Rule.EmptyScr});

   110 \<close>

   111 setup \<open>KEStore_Elems.add_rlss

   112   [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))]\<close>

   114 (*----------------------------- problem types --------------------------------*)

   115 (* ---------linear----------- *)

   116 setup \<open>KEStore_Elems.add_pbts

   117   [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Celem.e_pblID

   118       (["LINEAR", "univariate", "equation"],

   119         [("#Given" ,["equality e_e", "solveFor v_v"]),

   120           ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)

   121               "Not( (lhs e_e) is_polyrat_in v_v)",

   122               "Not( (rhs e_e) is_polyrat_in v_v)",

   123               "((lhs e_e) has_degree_in v_v)=1",

   124 	            "((rhs e_e) has_degree_in v_v)=1"]),

   125           ("#Find"  ,["solutions v_v'i'"])],

   126         LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))]\<close>

   128 (*-------------- methods------------------------------------------------------*)

   129 setup \<open>KEStore_Elems.add_mets

   130     [Specify.prep_met thy "met_eqlin" [] Celem.e_metID

   131       (["LinEq"], [],

   132         {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,

   133           crls = LinEq_crls, errpats = [], nrls = norm_Poly},

   134         @{thm refl})]

   135 \<close>

   136     (* ansprechen mit ["LinEq","solve_univar_equation"] *)

   138 partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   139   where

   140 "solve_linear_equation e_e v_v =

   141 (let e_e =((Try         (Rewrite     ''all_left''            False)) @@

   142            (Try (Repeat (Rewrite     ''makex1_x''            False))) @@

   143            (Try         (Rewrite_Set ''expand_binoms''       False)) @@

   144            (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)]

   145                                      ''make_ratpoly_in''     False))) @@

   146            (Try (Repeat (Rewrite_Set ''LinPoly_simplify''    False))))e_e;

   147      e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]

   148                                      ''LinEq_simplify'' True)) @@

   149             (Repeat(Try (Rewrite_Set ''LinPoly_simplify''    False)))) e_e

   150  in Or_to_List e_e)"

   151 setup \<open>KEStore_Elems.add_mets

   152     [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID

   153       (["LinEq","solve_lineq_equation"],

   154         [("#Given", ["equality e_e", "solveFor v_v"]),

   155           ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),

   156           ("#Find",  ["solutions v_v'i'"])],

   157         {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],

   158           crls = LinEq_crls, errpats = [], nrls = norm_Poly},

   159         @{thm solve_linear_equation.simps})]

   160 \<close>

   161 ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>

   163 end

author	Walther Neuper <wneuper@ist.tugraz.at>
	Sat, 22 Jun 2019 14:34:06 +0200
changeset 59551	6ea6d9c377a0
parent 59545	4035ec339062
child 59603	30cd47104ad7
permissions	-rw-r--r--