src/Tools/isac/Knowledge/LinEq.thy
author wenzelm
Sun, 20 Jun 2021 16:26:18 +0200
changeset 60306 51ec2e101e9f
parent 60303 815b0dc8b589
child 60358 8377b6c37640
permissions -rw-r--r--
Isar command 'problem' as combination of KEStore_Elems.add_pbts + Problem.prep_import, without change of semantics;
     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 *)
     9 
    10 theory LinEq imports Poly Equation begin
    11 
    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 \<up> 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
    19 
    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)"
    24 
    25 ML \<open>
    26 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
    27   Rule_Set.append_rules "LinEq_prls" Rule_Set.empty 
    28 	     [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
    29 	      \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
    30 	      \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
    31 	      \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
    32 	      \<^rule_eval>\<open>has_degree_in\<close> (eval_has_degree_in ""),
    33  	      \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
    34 	      \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),    
    35 	      \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    36 	      \<^rule_thm>\<open>not_true\<close>,
    37 	      \<^rule_thm>\<open>not_false\<close>,
    38 	      \<^rule_thm>\<open>and_true\<close>,
    39 	      \<^rule_thm>\<open>and_false\<close>,
    40 	      \<^rule_thm>\<open>or_true\<close>,
    41 	      \<^rule_thm>\<open>or_false\<close>
    42               ];
    43 (* ----- erls ----- *)
    44 val LinEq_crls = 
    45    Rule_Set.append_rules "LinEq_crls" poly_crls
    46    [\<^rule_thm>\<open>real_assoc_1\<close>
    47     (*		
    48      Don't use
    49      \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    50      \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
    51      *)
    52     ];
    53 
    54 (* ----- crls ----- *)
    55 val LinEq_erls = 
    56    Rule_Set.append_rules "LinEq_erls" Poly_erls
    57    [\<^rule_thm>\<open>real_assoc_1\<close>
    58     (*		
    59      Don't use
    60      \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    61      \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
    62      *)
    63     ];
    64 \<close>
    65 rule_set_knowledge LinEq_erls = LinEq_erls
    66 ML \<open>
    67     
    68 val LinPoly_simplify = prep_rls'(
    69   Rule_Def.Repeat {id = "LinPoly_simplify", preconds = [], 
    70        rew_ord = ("termlessI",termlessI), 
    71        erls = LinEq_erls, 
    72        srls = Rule_Set.Empty, 
    73        calc = [], errpatts = [],
    74        rules = [
    75 		\<^rule_thm>\<open>real_assoc_1\<close>,
    76 		\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    77 		\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
    78 		\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    79 		(*  Don't use  
    80 		 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    81 		 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    82 		 *)
    83 		\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
    84 		],
    85        scr = Rule.Empty_Prog});
    86 \<close>
    87 rule_set_knowledge LinPoly_simplify = LinPoly_simplify
    88 ML \<open>
    89 
    90 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    91 val LinEq_simplify = prep_rls'(
    92 Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
    93      rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
    94      erls = LinEq_erls,
    95      srls = Rule_Set.Empty,
    96      calc = [], errpatts = [],
    97      rules = [
    98 	      \<^rule_thm>\<open>lin_isolate_add1\<close>, 
    99 	      (* a+bx=0 -> bx=-a *)
   100 	      \<^rule_thm>\<open>lin_isolate_add2\<close>, 
   101 	      (* a+ x=0 ->  x=-a *)
   102 	      \<^rule_thm>\<open>lin_isolate_div\<close>    
   103 	      (*   bx=c -> x=c/b *)  
   104 	      ],
   105      scr = Rule.Empty_Prog});
   106 \<close>
   107 rule_set_knowledge LinEq_simplify = LinEq_simplify
   108 
   109 (*----------------------------- problems --------------------------------*)
   110 (* ---------linear----------- *)
   111 
   112 problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
   113   \<open>LinEq_prls\<close>
   114   Method: "LinEq/solve_lineq_equation"
   115   CAS: "solve (e_e::bool, v_v)"
   116   Given: "equality e_e" "solveFor v_v"
   117   Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)
   118     "Not( (lhs e_e) is_polyrat_in v_v)"
   119     "Not( (rhs e_e) is_polyrat_in v_v)"
   120     "((lhs e_e) has_degree_in v_v)=1"
   121 	  "((rhs e_e) has_degree_in v_v)=1"
   122   Find: "solutions v_v'i'"
   123 
   124 (*-------------- methods------------------------------------------------------*)
   125 method met_eqlin : "LinEq" =
   126   \<open>{rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
   127     crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
   128     (* ansprechen mit ["LinEq", "solve_univar_equation"] *)
   129 
   130 partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
   131   where
   132 "solve_linear_equation e_e v_v = (
   133   let
   134     e_e = (
   135       (Try (Rewrite ''all_left'')) #>
   136       (Try (Repeat (Rewrite ''makex1_x''))) #>
   137       (Try (Rewrite_Set ''expand_binoms'')) #>
   138       (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) #>
   139       (Try (Repeat (Rewrite_Set ''LinPoly_simplify''))) ) e_e;
   140     e_e = (
   141       (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) #>
   142       (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
   143   in
   144     Or_to_List e_e)"
   145 
   146 method met_eq_lin : "LinEq/solve_lineq_equation" =
   147   \<open>{rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
   148     crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
   149   Program: solve_linear_equation.simps
   150   Given: "equality e_e" "solveFor v_v"
   151   Where: "Not ((lhs e_e) is_polyrat_in v_v)" "((lhs e_e)  has_degree_in v_v) = 1"
   152   Find: "solutions v_v'i'"
   153 
   154 ML \<open>
   155   MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];
   156 \<close> ML \<open>
   157 \<close> ML \<open>
   158 \<close>
   159 
   160 end
   161