# HG changeset patch # User Walther Neuper # Date 1283933751 -7200 # Node ID 0be0c4e7ab9e21020bf0b1ffc0d195ebb7f37cf2 # Parent 972a73d7c50b3fae71b1c7ecb5a4f6b256f2befc updated Knowledge/RootEq.thy diff -r 972a73d7c50b -r 0be0c4e7ab9e src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Mon Sep 06 17:07:28 2010 +0200 +++ b/src/Tools/isac/Build_Isac.thy Wed Sep 08 10:15:51 2010 +0200 @@ -70,10 +70,15 @@ use_thy "Knowledge/LinEq" use_thy "Knowledge/Root" + +ML {* +incr_boundvars; +*} + use_thy "Knowledge/RootEq" + ML {* -111; *} diff -r 972a73d7c50b -r 0be0c4e7ab9e src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 17:07:28 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 08 10:15:51 2010 +0200 @@ -7,11 +7,11 @@ date: 02.11.14 *) -theory RootEq imports Root end +theory RootEq imports Root begin consts - (*-------------------------root-----------------------*) - is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _") + + is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _") is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _") is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _") @@ -522,6 +522,7 @@ {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, crls=RootEq_crls, nrls=norm_Poly(*, asm_rls=[],asm_thm=[]*)}, "empty_script")); + (*-- normalize 20.10.02 --*) store_met (prep_met thy "met_rooteq_norm" [] e_metID @@ -533,56 +534,72 @@ " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), ("#Find" ,["solutions v_i"]) ], - {rew_ord'="termlessI", - rls'=RootEq_erls, - srls=e_rls, - prls=RootEq_prls, - calc=[], - crls=RootEq_crls, nrls=norm_Poly(*, - asm_rls=[], - asm_thm=[("sqrt_square_1","")]*)}, + {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, + calc=[], crls=RootEq_crls, nrls=norm_Poly}, "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^ " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^ - " in ((SubProblem (RootEq_,[univariate,equation], " ^ - " [no_met]) [BOOL e_e, REAL v_])))" + " in ((SubProblem (RootEq_',[univariate,equation], " ^ + " [no_met]) [BOOL e_e, REAL v_v])))" )); +*} + +ML {* (*-----del------------------------------------------------del-----*) +Toplevel.debug := true; +val scr = +"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ +"(let e_e = " ^ +" ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^ +" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ +" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ +" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ +" (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^ +" (L_L::bool list) = " ^ +" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ +" then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ +" [no_met]) [BOOL e_e, REAL v_v]) " ^ +" else (SubProblem (RootEq_',[univariate,equation], [no_met]) " ^ +" [BOOL e_e, REAL v_v])) " ^ +"in Check_elementwise L_L {(v_v::real). Assumptions})"; +val sss = ( term_of o the o (parse thy)) scr; +*} + +ML {* +val -------------------------------------------------- = "00000"; store_met (prep_met thy "met_rooteq_sq" [] e_metID (["RootEq","solve_sq_root_equation"], - [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ - " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ - " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), + [("#Given" ,["equality e_e", "solveFor v_v"]), + ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ + " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ + "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ + " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), ("#Find" ,["solutions v_i"]) ], - {rew_ord'="termlessI", - rls'=RootEq_erls, - srls = rooteq_srls, - prls = RootEq_prls, - calc = [], - crls=RootEq_crls, nrls=norm_Poly}, -"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ -"(let e_e = " ^ -" ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ " ^ -" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ -" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ -" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ -" (Try (Rewrite_Set rooteq_simplify True))) e_;" ^ -" (L_::bool list) = " ^ -" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ -" then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^ -" [no_met]) [BOOL e_e, REAL v_]) " ^ -" else (SubProblem (RootEq_,[univariate,equation], " ^ -" [no_met]) [BOOL e_e, REAL v_])) " ^ -" in Check_elementwise L_ {(v_v::real). Assumptions})" + {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, + prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, +"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ +"(let e_e = " ^ +" ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^ +" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ +" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ +" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ +" (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^ +" (L_L::bool list) = " ^ +" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ +" then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ +" [no_met]) [BOOL e_e, REAL v_v]) " ^ +" else (SubProblem (RootEq_',[univariate,equation], [no_met]) " ^ +" [BOOL e_e, REAL v_v])) " ^ +"in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* (*-- right 28.08.02 --*) store_met (prep_met thy "met_rooteq_sq_right" [] e_metID @@ -591,25 +608,22 @@ ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), ("#Find" ,["solutions v_i"]) ], - {rew_ord'="termlessI", - rls'=RootEq_erls, - srls=e_rls, - prls=RootEq_prls, - calc=[], - crls=RootEq_crls, nrls=norm_Poly}, - "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ - "(let e_e = " ^ - " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ " ^ - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ + {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, + prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, + "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ + "(let e_e = " ^ + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^ + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ - " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ - " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^ - " [no_met]) [BOOL e_e, REAL v_]) " ^ - " else ((SubProblem (RootEq_,[univariate,equation], " ^ - " [no_met]) [BOOL e_e, REAL v_])))" + " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ + " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ + " [no_met]) [BOOL e_e, REAL v_v]) " ^ + " else ((SubProblem (RootEq_',[univariate,equation], " ^ + " [no_met]) [BOOL e_e, REAL v_v])))" )); +val --------------------------------------------------+++ = "33333"; (*-- left 28.08.02 --*) store_met @@ -627,17 +641,18 @@ crls=RootEq_crls, nrls=norm_Poly}, "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^ "(let e_e = " ^ - " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ " ^ + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^ " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^ - " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^ - " [no_met]) [BOOL e_e, REAL v_]) " ^ - " else ((SubProblem (RootEq_,[univariate,equation], " ^ - " [no_met]) [BOOL e_e, REAL v_])))" + " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ + " [no_met]) [BOOL e_e, REAL v_v]) " ^ + " else ((SubProblem (RootEq_',[univariate,equation], " ^ + " [no_met]) [BOOL e_e, REAL v_v])))" )); +val --------------------------------------------------++++ = "44444"; calclist':= overwritel (!calclist', [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", diff -r 972a73d7c50b -r 0be0c4e7ab9e src/Tools/isac/ProgLang/Script.thy --- a/src/Tools/isac/ProgLang/Script.thy Mon Sep 06 17:07:28 2010 +0200 +++ b/src/Tools/isac/ProgLang/Script.thy Wed Sep 08 10:15:51 2010 +0200 @@ -18,12 +18,12 @@ consts (*types of subproblems' arguments*) - real_' :: "real => arg" - REAL_LIST' :: "(real list) => arg" - REAL_SET' :: "(real set) => arg" - BOOL' :: "bool => arg" - BOOL_LIST' :: "(bool list) => arg" - REAL_REAL' :: "(real => real) => arg" + REAL :: "real => arg" + REAL_LIST :: "(real list) => arg" + REAL_SET :: "(real set) => arg" + BOOL :: "bool => arg" + BOOL_LIST :: "(bool list) => arg" + REAL_REAL :: "(real => real) => arg" (*tactics*) Rewrite :: "[ID, bool, 'a] => 'a" diff -r 972a73d7c50b -r 0be0c4e7ab9e src/Tools/isac/ProgLang/term.sml --- a/src/Tools/isac/ProgLang/term.sml Mon Sep 06 17:07:28 2010 +0200 +++ b/src/Tools/isac/ProgLang/term.sml Wed Sep 08 10:15:51 2010 +0200 @@ -20,7 +20,7 @@ (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true) handle _ => false -fun atomtyp t = (*see raw_pp_typ*) +fun atomtyp t = (*WN10 see raw_pp_typ*) let fun ato n (Type (s,[])) = ("\n*** "^indent n^"Type ("^s^",[])") @@ -37,9 +37,20 @@ ("\n*** "^indent n^"]") | atol n (T::Ts) = (ato n T ^ atol n Ts) (*in print (ato 0 t ^ "\n") end; TODO TUM10*) -in writeln(ato 0 t) end; +in writeln (ato 0 t) end; +(* +> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat"; +> atomtyp T; +*** Type (fun,[ +*** Type (RealDef.real,[]) +*** Type (fun,[ +*** Type (IntDef.int,[]) +*** Type (nat,[]) +*** ] +*** ] +*) -(*Prog.Tutorial.p.34*) +(*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*) local fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] fun pp_list xs = Pretty.list "[" "]" xs @@ -64,49 +75,37 @@ (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); *) -(* -> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat"; -> atomtyp T; -*** Type (fun,[ -*** Type (RealDef.real,[]) -*** Type (fun,[ -*** Type (IntDef.int,[]) -*** Type (nat,[]) -*** ] -*** ] -*) - fun atomt t = - let fun ato (Const(a,T)) n = - ("\n*** "^indent n^"Const ("^a^")") - | ato (Free (a,T)) n = - ("\n*** "^indent n^"Free ("^a^", "^")") - | ato (Var ((a,ix),T)) n = - ("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")") - | ato (Bound ix) n = - ("\n*** "^indent n^"Bound "^(string_of_int ix)) - | ato (Abs(a,T,body)) n = - ("\n*** "^indent n^"Abs("^a^",..")^ato body (n+1) - | ato (f$t') n = (ato f n; ato t' (n+1)) - in writeln("\n*** -------------"^ ato t 0 ^"\n***") end; + let fun ato (Const (a, _)) n = + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)" + | ato (Free (a, _)) n = + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)" + | ato (Var ((a, i), _)) n = + "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^ + string_of_int i ^ "), _)" + | ato (Bound i) n = + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i + | ato (Abs (a, _, body)) n = + "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1) + | ato (f $ t) n = (ato f n ^ ato t (n + 1)) + in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end; fun term_detail2str t = - let fun ato (Const (a, T)) n = - "\n*** "^indent n^"Const ("^a^", "^string_of_typ T^")" - | ato (Free (a, T)) n = - "\n*** "^indent n^"Free ("^a^", "^string_of_typ T^")" - | ato (Var ((a, ix), T)) n = - "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^ - string_of_typ T^")" - | ato (Bound ix) n = - "\n*** "^indent n^"Bound "^string_of_int ix + let fun ato (Const (a, T)) n = + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")" + | ato (Free (a, T)) n = + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")" + | ato (Var ((a, i), T)) n = + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^ + string_of_typ T ^ ")" + | ato (Bound i) n = + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i | ato (Abs(a, T, body)) n = - "\n*** "^indent n^"Abs ("^a^", "^ - (string_of_typ T)^",.." - ^ato body (n + 1) - | ato (f $ t') n = ato f n^ato t' (n+1) - in "\n*** "^ato t 0^"\n***" end; -fun atomty t = (writeln o term_detail2str) t; + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.." + ^ ato body (n + 1) + | ato (f $ t) n = ato f n ^ ato t (n + 1) + in "\n*** " ^ ato t 0 ^ "\n***" end; +fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*) fun term_str thy (Const(s,_)) = s | term_str thy (Free(s,_)) = s @@ -802,98 +801,28 @@ fun mk_Free (s,T) = Free(s,T); fun mk_free T s = Free(s,T); +(*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*) +fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*) + let fun subst (t as Bound i, lev) = + if i atomt sc; -*** Const ( Script.Testeq) -*** . Free ( e_, ) -*** . Const ( Script.While) -*** . . Const ( RatArith.contains'_root) -*** . . . Free ( e_, ) -*** . . Const ( Let) -*** . . . Const ( Script.Try) -*** . . . . Const ( Script.Repeat) -*** . . . . . Const ( Script.Rewrite) -*** . . . . . . Free ( rroot_square_inv, ) -*** . . . . . . Const ( False) -*** . . . . . . Free ( e_, ) -*** . . . Abs( e_,.. -*** . . . . Const ( Let) -*** . . . . . Const ( Script.Try) -*** . . . . . . Const ( Script.Repeat) -*** . . . . . . . Const ( Script.Rewrite) -*** . . . . . . . . Free ( square_equation_left, ) -*** . . . . . . . . Const ( True) -*** . . . . . . . . Bound 0 <-- !!! -*** . . . . . Abs( e_,.. -*** . . . . . . Const ( Script.Try) -*** . . . . . . . Const ( Script.Repeat) -*** . . . . . . . . Const ( Script.Rewrite) -*** . . . . . . . . . Free ( radd_0, ) -*** . . . . . . . . . Const ( False) -*** . . . . . . . . . Bound 0 <-- !!! -val it = () : unit -ML> atomt (inst_abs thy sc); -*** Const ( Script.Testeq) -*** . Free ( e_, ) -*** . Const ( Script.While) -*** . . Const ( RatArith.contains'_root) -*** . . . Free ( e_, ) -*** . . Const ( Let) -*** . . . Const ( Script.Try) -*** . . . . Const ( Script.Repeat) -*** . . . . . Const ( Script.Rewrite) -*** . . . . . . Free ( rroot_square_inv, ) -*** . . . . . . Const ( False) -*** . . . . . . Free ( e_, ) -*** . . . Abs( e_,.. -*** . . . . Const ( Let) -*** . . . . . Const ( Script.Try) -*** . . . . . . Const ( Script.Repeat) -*** . . . . . . . Const ( Script.Rewrite) -*** . . . . . . . . Free ( square_equation_left, ) -*** . . . . . . . . Const ( True) -*** . . . . . . . . Free ( e_, ) <-- !!! -*** . . . . . Abs( e_,.. -*** . . . . . . Const ( Script.Try) -*** . . . . . . . Const ( Script.Repeat) -*** . . . . . . . . Const ( Script.Rewrite) -*** . . . . . . . . . Free ( radd_0, ) -*** . . . . . . . . . Const ( False) -*** . . . . . . . . . Free ( e_, ) <-- ZUFALL vor 5.03!!! -val it = () : unit*) - - - - -fun inst_abs thy (Const sT) = Const sT - | inst_abs thy (Free sT) = Free sT - | inst_abs thy (Bound n) = Bound n - | inst_abs thy (Var iT) = Var iT - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) = - let val b' = subst_bound (Free(v,T2),b); - (*fun variant_abs: term.ML*) - in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end - | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2 - | inst_abs thy t = - (writeln("inst_abs: unchanged t= "^ term2str t); - t); + | inst_abs thy t = t; (*val scr = "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \ \ (let h_ = (hd o (filterVar f_)) eqs_; \ diff -r 972a73d7c50b -r 0be0c4e7ab9e test/Tools/isac/Run_Tests.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Run_Tests.thy Wed Sep 08 10:15:51 2010 +0200 @@ -0,0 +1,11 @@ +(* +$ cd /usr/local/isabisac/test/Tools/isac +$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy & + +*) + +theory Run_Tests imports Main begin + +use "ProgLang/term.sml" + +end