1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 22 13:15:52 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 22 14:34:06 2019 +0200
1.3 @@ -24,23 +24,6 @@
1.4 is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
1.5 is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
1.6 is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
1.7 - (*----------------------scripts-----------------------*)
1.8 - Norm'_sq'_root'_equation
1.9 - :: "[bool,real,
1.10 - bool list] => bool list"
1.11 - ("((Script Norm'_sq'_root'_equation (_ _ =))// (_))" 9)
1.12 - Solve'_sq'_root'_equation
1.13 - :: "[bool,real,
1.14 - bool list] => bool list"
1.15 - ("((Script Solve'_sq'_root'_equation (_ _ =))// (_))" 9)
1.16 - Solve'_left'_sq'_root'_equation
1.17 - :: "[bool,real,
1.18 - bool list] => bool list"
1.19 - ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// (_))" 9)
1.20 - Solve'_right'_sq'_root'_equation
1.21 - :: "[bool,real,
1.22 - bool list] => bool list"
1.23 - ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// (_))" 9)
1.24
1.25 subsection \<open>theorems not yet adopted from Isabelle\<close>
1.26 axiomatization where
1.27 @@ -518,15 +501,7 @@
1.28 ("#Find" ,["solutions v_v'i'"])],
1.29 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
1.30 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
1.31 - @{thm norm_sqrt_equ.simps}
1.32 - (*"Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.33 - "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^
1.34 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.35 - " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
1.36 - " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
1.37 - " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^
1.38 - " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
1.39 - " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
1.40 + @{thm norm_sqrt_equ.simps})]
1.41 \<close>
1.42
1.43 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.44 @@ -557,21 +532,7 @@
1.45 ("#Find" ,["solutions v_v'i'"])],
1.46 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
1.47 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
1.48 - @{thm solve_sqrt_equ.simps}
1.49 - (*"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.50 - "(let e_e = " ^
1.51 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^
1.52 - " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
1.53 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.54 - " (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@ " ^
1.55 - " (Try (Rewrite_Set ''rooteq_simplify'' True)) ) e_e; " ^
1.56 - " (L_L::bool list) = " ^
1.57 - " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
1.58 - " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
1.59 - " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
1.60 - " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^
1.61 - " [BOOL e_e, REAL v_v])) " ^
1.62 - "in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
1.63 + @{thm solve_sqrt_equ.simps})]
1.64 \<close>
1.65 (*-- right 28.08.02 --*)
1.66 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.67 @@ -596,19 +557,7 @@
1.68 ("#Find" ,["solutions v_v'i'"])],
1.69 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule.e_rls, prls = RootEq_prls, calc = [],
1.70 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
1.71 - @{thm solve_sqrt_equ_right.simps}
1.72 - (*"Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.73 - "(let e_e = " ^
1.74 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^
1.75 - " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
1.76 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.77 - " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
1.78 - " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
1.79 - " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
1.80 - " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
1.81 - " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
1.82 - " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^
1.83 - " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
1.84 + @{thm solve_sqrt_equ_right.simps})]
1.85 \<close>
1.86 (*-- left 28.08.02 --*)
1.87 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.88 @@ -634,19 +583,7 @@
1.89 ("#Find" ,["solutions v_v'i'"])],
1.90 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
1.91 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
1.92 - @{thm solve_sqrt_equ_left.simps}
1.93 - (*"Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.94 - "(let e_e = " ^
1.95 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^
1.96 - " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
1.97 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.98 - " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
1.99 - " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
1.100 - " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
1.101 - " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
1.102 - " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
1.103 - " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
1.104 - " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
1.105 + @{thm solve_sqrt_equ_left.simps})]
1.106 \<close>
1.107 ML \<open>
1.108 \<close> ML \<open>