1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Dec 20 18:02:25 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Dec 26 14:24:05 2018 +0100
1.3 @@ -478,14 +478,14 @@
1.4
1.5 (*-------------------------Problem-----------------------*)
1.6 (*
1.7 -(get_pbt ["root'","univariate","equation"]);
1.8 +(get_pbt ["rootX","univariate","equation"]);
1.9 show_ptyps();
1.10 *)
1.11 \<close>
1.12 setup \<open>KEStore_Elems.add_pbts
1.13 (* ---------root----------- *)
1.14 [(Specify.prep_pbt thy "pbl_equ_univ_root" [] Celem.e_pblID
1.15 - (["root'","univariate","equation"],
1.16 + (["rootX","univariate","equation"],
1.17 [("#Given" ,["equality e_e","solveFor v_v"]),
1.18 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
1.19 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
1.20 @@ -493,7 +493,7 @@
1.21 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
1.22 (* ---------sqrt----------- *)
1.23 (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] Celem.e_pblID
1.24 - (["sq","root'","univariate","equation"],
1.25 + (["sq","rootX","univariate","equation"],
1.26 [("#Given" ,["equality e_e","solveFor v_v"]),
1.27 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
1.28 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
1.29 @@ -503,7 +503,7 @@
1.30 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])),
1.31 (* ---------normalise----------- *)
1.32 (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] Celem.e_pblID
1.33 - (["normalise","root'","univariate","equation"],
1.34 + (["normalise","rootX","univariate","equation"],
1.35 [("#Given" ,["equality e_e","solveFor v_v"]),
1.36 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
1.37 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
1.38 @@ -533,12 +533,12 @@
1.39 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
1.40 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
1.41 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.42 - "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
1.43 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.44 - " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
1.45 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.46 - " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
1.47 - " in ((SubProblem (RootEq',[univariate,equation], " ^
1.48 + "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^
1.49 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.50 + " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
1.51 + " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
1.52 + " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^
1.53 + " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
1.54 " [no_met]) [BOOL e_e, REAL v_v])))")]
1.55 \<close>
1.56 setup \<open>KEStore_Elems.add_mets
1.57 @@ -554,16 +554,16 @@
1.58 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
1.59 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.60 "(let e_e = " ^
1.61 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
1.62 - " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
1.63 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.64 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.65 - " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
1.66 + " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^
1.67 + " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
1.68 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.69 + " (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@ " ^
1.70 + " (Try (Rewrite_Set ''rooteq_simplify'' True)) ) e_e; " ^
1.71 " (L_L::bool list) = " ^
1.72 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
1.73 - " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
1.74 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
1.75 - " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
1.76 + " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
1.77 + " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
1.78 + " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^
1.79 " [BOOL e_e, REAL v_v])) " ^
1.80 "in Check_elementwise L_L {(v_v::real). Assumptions})")]
1.81 \<close>
1.82 @@ -578,15 +578,15 @@
1.83 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
1.84 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.85 "(let e_e = " ^
1.86 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
1.87 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
1.88 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.89 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.90 - " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
1.91 + " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^
1.92 + " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
1.93 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.94 + " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
1.95 + " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
1.96 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
1.97 - " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
1.98 + " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
1.99 " [no_met]) [BOOL e_e, REAL v_v]) " ^
1.100 - " else ((SubProblem (RootEq',[univariate,equation], " ^
1.101 + " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^
1.102 " [no_met]) [BOOL e_e, REAL v_v])))")]
1.103 \<close>
1.104 (*-- left 28.08.02 --*)
1.105 @@ -600,16 +600,16 @@
1.106 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
1.107 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
1.108 "(let e_e = " ^
1.109 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
1.110 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
1.111 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.112 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.113 - " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
1.114 + " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^
1.115 + " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
1.116 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
1.117 + " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
1.118 + " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
1.119 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
1.120 - " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
1.121 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
1.122 - " else ((SubProblem (RootEq',[univariate,equation], " ^
1.123 - " [no_met]) [BOOL e_e, REAL v_v])))")]
1.124 + " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
1.125 + " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
1.126 + " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
1.127 + " [''no_met'']) [BOOL e_e, REAL v_v])))")]
1.128 \<close>
1.129
1.130 setup \<open>KEStore_Elems.add_calcs