wneuper@59430: (* Knowledge for tests, specifically simplified or bound to a fixed state wneuper@59430: for the purpose of simplifying tests. neuper@37954: Author: Walther Neuper 2003 neuper@37954: (c) due to copyright terms wneuper@59432: wneuper@59432: Notes on cleanup: wneuper@59432: (0) revert import Test -- DiophantEq, this raises issues related to (1..4) wneuper@59432: (1) transfer methods to respective theories, if only test, then hierarchy at ["...", "Test"]: wneuper@59432: differentiate, root equatioh, polynomial equation, diophantine equation wneuper@59432: (2) transfer problems accordingly wneuper@59432: (3) rearrange rls according to (1..2) wneuper@59432: (4) rearrange axiomatizations according to (3) neuper@37954: *) neuper@37906: wneuper@59424: theory Test imports Base_Tools Poly Rational Root Diff begin neuper@37906: wneuper@59472: section \consts\ wneuper@59472: subsection \for scripts\ neuper@37906: consts neuper@37906: Solve'_univar'_err neuper@37954: :: "[bool,real,bool, neuper@37954: bool list] => bool list" wneuper@59334: ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9) neuper@37906: Solve'_linear neuper@37954: :: "[bool,real, neuper@37954: bool list] => bool list" wneuper@59334: ("((Script Solve'_linear (_ _ =))// (_))" 9) wneuper@59430: Solve'_root'_equation wneuper@59430: :: "[bool,real, wneuper@59430: bool list] => bool list" wneuper@59430: ("((Script Solve'_root'_equation (_ _ =))// (_))" 9) wneuper@59430: Solve'_plain'_square wneuper@59430: :: "[bool,real, wneuper@59430: bool list] => bool list" wneuper@59430: ("((Script Solve'_plain'_square (_ _ =))// (_))" 9) wneuper@59430: Norm'_univar'_equation wneuper@59430: :: "[bool,real, wneuper@59430: bool] => bool" wneuper@59430: ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9) wneuper@59430: STest'_simplify wneuper@59430: :: "['z, wneuper@59430: 'z] => 'z" wneuper@59430: ("((Script STest'_simplify (_ =))// (_))" 9) neuper@37906: neuper@37906: wneuper@59472: subsection \for problems\ wneuper@59430: consts neuper@42008: "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10) neuper@42008: "contains'_root" :: "'a => bool" ("contains'_root _" 10) neuper@42008: neuper@42008: "precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10) neuper@42008: "precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10) neuper@42008: "precond'_submet" :: "'a => bool" ("precond'_submet _" 10) neuper@42008: "precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10) neuper@37906: neuper@37906: wneuper@59472: section \functions\ wneuper@59472: ML \ wneuper@59430: fun bin_o (Const (op_, (Type ("fun", [Type (s2, []), Type ("fun", [Type (s4, _),Type (s5, _)])])))) wneuper@59430: = if s2 = s4 andalso s4 = s5 then [op_] else [] wneuper@59430: | bin_o _ = []; neuper@37906: wneuper@59430: fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2) wneuper@59430: | bin_op t = bin_o t; wneuper@59430: fun is_bin_op t = (bin_op t <> []); neuper@37906: wneuper@59430: fun bin_op_arg1 ((Const (_, wneuper@59430: (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) $ arg1 $ _) = arg1 wneuper@59430: | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ Rule.term2str t); wneuper@59430: fun bin_op_arg2 ((Const (_, wneuper@59430: (Type ("fun", [Type (_, []),Type ("fun", [Type _, Type _])]))))$ _ $ arg2) = arg2 wneuper@59430: | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ Rule.term2str t); neuper@37906: wneuper@59430: exception NO_EQUATION_TERM; wneuper@59430: fun is_equation ((Const ("HOL.eq", wneuper@59430: (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ _ $ _) = true wneuper@59430: | is_equation _ = false; wneuper@59430: fun equ_lhs ((Const ("HOL.eq", wneuper@59430: (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ l $ _) = l wneuper@59430: | equ_lhs _ = raise NO_EQUATION_TERM; wneuper@59430: fun equ_rhs ((Const ("HOL.eq", (Type ("fun", wneuper@59430: [Type (_, []), Type ("fun", [Type (_, []), Type ("bool",[])])])))) $ _ $ r) = r wneuper@59430: | equ_rhs _ = raise NO_EQUATION_TERM; neuper@37906: wneuper@59430: fun atom (Const (_, Type (_,[]))) = true wneuper@59430: | atom (Free (_, Type (_,[]))) = true wneuper@59430: | atom (Var (_, Type (_,[]))) = true wneuper@59430: | atom((Const ("Bin.integ_of_bin",_)) $ _) = true wneuper@59430: | atom _ = false; wneuper@59430: wneuper@59430: fun varids (Const (s, Type (_,[]))) = [strip_thy s] wneuper@59430: | varids (Free (s, Type (_,[]))) = if TermC.is_num' s then [] else [strip_thy s] wneuper@59430: | varids (Var((s, _),Type (_,[]))) = [strip_thy s] wneuper@59430: (*| varids (_ (s,"?DUMMY" )) = ..ML-error *) wneuper@59430: | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*) wneuper@59430: | varids (Abs (a, _, t)) = union op = [a] (varids t) wneuper@59430: | varids (t1 $ t2) = union op = (varids t1) (varids t2) wneuper@59430: | varids _ = []; wneuper@59430: wneuper@59430: fun bin_ops_only ((Const op_) $ t1 $ t2) = wneuper@59430: if is_bin_op (Const op_) then bin_ops_only t1 andalso bin_ops_only t2 else false wneuper@59430: | bin_ops_only t = if atom t then true else bin_ops_only t; wneuper@59430: wneuper@59430: fun polynomial opl t _(* bdVar TODO *) = wneuper@59430: subset op = (bin_op t, opl) andalso (bin_ops_only t); wneuper@59430: wneuper@59430: fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) wneuper@59430: andalso polynomial opl (equ_lhs t) bdVar wneuper@59430: andalso polynomial opl (equ_rhs t) bdVar wneuper@59430: andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse wneuper@59430: subset op = (varids bdVar, varids (equ_lhs t))); wneuper@59430: wneuper@59430: fun max (a,b) = if a < b then b else a; wneuper@59430: wneuper@59430: fun degree addl mul bdVar t = wneuper@59430: let wneuper@59430: fun deg _ _ v (Const (s, Type (_, []))) = if v=strip_thy s then 1 else 0 wneuper@59430: | deg _ _ v (Free (s, Type (_, []))) = if v=strip_thy s then 1 else 0 wneuper@59430: | deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy s then 1 else 0 wneuper@59430: (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *) wneuper@59430: | deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0 wneuper@59430: | deg addl mul v (h $ t1 $ t2) = wneuper@59430: if subset op = (bin_op h, addl) wneuper@59430: then max (deg addl mul v t1 , deg addl mul v t2) wneuper@59430: else (*mul!*)(deg addl mul v t1) + (deg addl mul v t2) wneuper@59430: | deg _ _ _ t = raise ERROR ("deg: t = " ^ Rule.term2str t) wneuper@59430: in wneuper@59430: if polynomial (addl @ [mul]) t bdVar wneuper@59430: then SOME (deg addl mul (id_of bdVar) t) wneuper@59430: else (NONE:int option) wneuper@59430: end; wneuper@59430: fun degree_ addl mul bdVar t = (* do not export *) wneuper@59430: let wneuper@59430: fun opt (SOME i)= i wneuper@59430: | opt NONE = 0 wneuper@59430: in opt (degree addl mul bdVar t) end; wneuper@59430: wneuper@59430: fun linear addl mul t bdVar = (degree_ addl mul bdVar t) < 2; wneuper@59430: wneuper@59430: fun linear_equ addl mul bdVar t = wneuper@59430: if is_equation t wneuper@59430: then wneuper@59430: let wneuper@59430: val degl = degree_ addl mul bdVar (equ_lhs t); wneuper@59430: val degr = degree_ addl mul bdVar (equ_rhs t) wneuper@59430: in if (degl>0 orelse degr>0)andalso max(degl,degr) < 2 then true else false end wneuper@59430: else false; wneuper@59430: (* strip_thy op_ before *) wneuper@59430: fun is_div_op (dv, (Const (op_, wneuper@59430: (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) ) = (dv = strip_thy op_) wneuper@59430: | is_div_op _ = false; wneuper@59430: wneuper@59430: fun is_denom bdVar div_op t = wneuper@59430: let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) wneuper@59430: | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) wneuper@59430: | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false) wneuper@59430: | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false wneuper@59430: | is bool[v]dv (h$n$d) = wneuper@59430: if is_div_op(dv,h) wneuper@59430: then (is false[v]dv n)orelse(is true[v]dv d) wneuper@59430: else (is bool [v]dv n)orelse(is bool[v]dv d) wneuper@59430: in is false (varids bdVar) (strip_thy div_op) t end; wneuper@59430: wneuper@59430: wneuper@59430: fun rational t div_op bdVar = wneuper@59430: is_denom bdVar div_op t andalso bin_ops_only t; wneuper@59430: wneuper@59472: \ wneuper@59430: wneuper@59472: section \axiomatizations\ neuper@52148: axiomatization where (*TODO: prove as theorems*) neuper@37906: neuper@52148: radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and neuper@52148: rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and neuper@52148: rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and neuper@52148: rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and neuper@37983: rcollect_right: neuper@52148: "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and neuper@37983: rcollect_one_left: neuper@52148: "m is_const ==> (n::real) + m * n = (1 + m) * n" and neuper@37983: rcollect_one_left_assoc: neuper@52148: "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and neuper@37983: rcollect_one_left_assoc_p: neuper@52148: "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and neuper@37906: neuper@52148: rtwo_of_the_same: "a + a = 2 * a" and neuper@52148: rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and neuper@52148: rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and neuper@37906: neuper@52148: rcancel_den: "not(a=0) ==> a * (b / a) = b" and neuper@52148: rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and neuper@52148: rshift_nominator: "(a::real) * b / c = a / c * b" and neuper@37906: neuper@52148: exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and neuper@52148: rsqare: "(a::real) * a = a ^^^ 2" and neuper@52148: power_1: "(a::real) ^^^ 1 = a" and neuper@52148: rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" and neuper@37906: neuper@52148: rmult_1: "1 * k = (k::real)" and neuper@52148: rmult_1_right: "k * 1 = (k::real)" and neuper@52148: rmult_0: "0 * k = (0::real)" and neuper@52148: rmult_0_right: "k * 0 = (0::real)" and neuper@52148: radd_0: "0 + k = (k::real)" and neuper@52148: radd_0_right: "k + 0 = (k::real)" and neuper@37906: neuper@37983: radd_real_const_eq: neuper@52148: "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and neuper@37983: radd_real_const: neuper@37906: "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))" neuper@52148: and neuper@37906: (*for AC-operators*) neuper@52148: radd_commute: "(m::real) + (n::real) = n + m" and neuper@52148: radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and neuper@52148: radd_assoc: "(m::real) + n + k = m + (n + k)" and neuper@52148: rmult_commute: "(m::real) * n = n * m" and neuper@52148: rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and neuper@52148: rmult_assoc: "(m::real) * n * k = m * (n * k)" and neuper@37906: neuper@37906: (*for equations: 'bdv' is a meta-constant*) neuper@52148: risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and neuper@52148: risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and neuper@52148: risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and neuper@37906: neuper@37983: rnorm_equation_add: neuper@52148: "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and neuper@37906: neuper@37906: (*17.9.02 aus SqRoot.thy------------------------------vvv---*) neuper@52148: root_ge0: "0 <= a ==> 0 <= sqrt a" and neuper@37906: (*should be dropped with better simplification in eval_rls ...*) neuper@37983: root_add_ge0: neuper@52148: "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and neuper@37983: root_ge0_1: neuper@52148: "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and neuper@37983: root_ge0_2: neuper@52148: "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and neuper@37906: neuper@37906: neuper@52148: rroot_square_inv: "(sqrt a)^^^ 2 = a" and neuper@52148: rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and neuper@52148: rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and neuper@52148: rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and neuper@37906: neuper@37906: neuper@37906: (*for root-equations*) neuper@37983: square_equation_left: neuper@52148: "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and neuper@37983: square_equation_right: neuper@52148: "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and neuper@37906: (*causes frequently non-termination:*) neuper@37983: square_equation: neuper@52148: "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" and neuper@37906: neuper@52148: risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and neuper@52148: risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and neuper@52148: risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and neuper@37906: neuper@37906: (*for polynomial equations of degree 2; linear case in RatArith*) neuper@52148: mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and neuper@52148: constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and neuper@52148: constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and neuper@37906: neuper@37983: square_equality: neuper@52148: "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and neuper@37983: square_equality_0: neuper@52148: "(x^^^2 = 0) = (x = 0)" and neuper@37906: neuper@37906: (*isolate root on the LEFT hand side of the equation neuper@37906: otherwise shuffling from left to right would not terminate*) neuper@37906: neuper@37983: rroot_to_lhs: neuper@52148: "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and neuper@37983: rroot_to_lhs_mult: neuper@52148: "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and neuper@37983: rroot_to_lhs_add_mult: neuper@37906: "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)" neuper@37906: (*17.9.02 aus SqRoot.thy------------------------------^^^---*) neuper@37906: wneuper@59472: section \eval functions\ wneuper@59472: ML \ neuper@37972: val thy = @{theory}; neuper@37972: neuper@37954: (** evaluation of numerals and predicates **) neuper@37954: neuper@37954: (*does a term contain a root ?*) neuper@37954: fun eval_contains_root (thmid:string) _ neuper@37954: (t as (Const("Test.contains'_root",t0) $ arg)) thy = neuper@38053: if member op = (ids_of arg) "sqrt" wneuper@59416: then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) wneuper@59416: else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) neuper@38053: | eval_contains_root _ _ _ _ = NONE; neuper@42008: neuper@42008: (*dummy precondition for root-met of x+1=2*) neuper@42008: fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy = wneuper@59416: SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) neuper@52070: | eval_precond_rootmet _ _ _ _ = NONE; neuper@42008: neuper@42008: (*dummy precondition for root-pbl of x+1=2*) neuper@42008: fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy = wneuper@59416: SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", wneuper@59390: HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) s1210629013@52159: | eval_precond_rootpbl _ _ _ _ = NONE; wneuper@59472: \ wneuper@59472: setup \KEStore_Elems.add_calcs wneuper@59403: [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")), s1210629013@52145: ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")), s1210629013@52145: ("Test.precond'_rootpbl", ("Test.precond'_rootpbl", wneuper@59430: eval_precond_rootpbl"#Test.precond_rootpbl_"))] wneuper@59472: \ wneuper@59472: ML \ wneuper@59430: (*8.4.03 aus Poly.ML--------------------------------vvv--- wneuper@59430: make_polynomial ---> make_poly wneuper@59430: ^-- for user ^-- for systest _ONLY_*) wneuper@59430: wneuper@59430: local (*. for make_polytest .*) wneuper@59430: wneuper@59430: open Term; (* for type order = EQUAL | LESS | GREATER *) wneuper@59430: wneuper@59430: fun pr_ord EQUAL = "EQUAL" wneuper@59430: | pr_ord LESS = "LESS" wneuper@59430: | pr_ord GREATER = "GREATER"; wneuper@59430: wneuper@59430: fun dest_hd' (Const (a, T)) = (* ~ term.ML *) wneuper@59430: (case a of wneuper@59430: "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *) wneuper@59430: | _ => (((a, 0), T), 0)) wneuper@59430: | dest_hd' (Free (a, T)) = (((a, 0), T), 1) wneuper@59430: | dest_hd' (Var v) = (v, 2) wneuper@59430: | dest_hd' (Bound i) = ((("", i), dummyT), 3) wneuper@59430: | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); wneuper@59430: (* RL *) wneuper@59430: fun get_order_pow (t $ (Free(order,_))) = wneuper@59430: (case TermC.int_of_str_opt (order) of wneuper@59430: SOME d => d wneuper@59430: | NONE => 0) wneuper@59430: | get_order_pow _ = 0; wneuper@59430: wneuper@59430: fun size_of_term' (Const(str,_) $ t) = wneuper@59430: if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*) wneuper@59430: | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body wneuper@59430: | size_of_term' (f$t) = size_of_term' f + size_of_term' t wneuper@59430: | size_of_term' _ = 1; wneuper@59430: fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) wneuper@59430: (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) wneuper@59430: | ord => ord) wneuper@59430: | term_ord' pr thy (t, u) = wneuper@59430: (if pr then wneuper@59430: let val (f, ts) = strip_comb t and (g, us) = strip_comb u; wneuper@59430: val _ = tracing ("t= f@ts= \"" ^ Rule.term2str f ^ "\" @ \"[" ^ wneuper@59430: commas(map Rule.term2str ts) ^ "]\"") wneuper@59430: val _ = tracing ("u= g@us= \"" ^ Rule.term2str g ^"\" @ \"[" ^ wneuper@59430: commas(map Rule.term2str us) ^"]\"") wneuper@59430: val _ = tracing ("size_of_term(t,u)= (" ^ wneuper@59430: string_of_int (size_of_term' t) ^ ", " ^ wneuper@59430: string_of_int (size_of_term' u) ^ ")") wneuper@59430: val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g)) wneuper@59430: val _ = tracing ("terms_ord(ts,us) = " ^ wneuper@59430: (pr_ord o terms_ord str false) (ts,us)); wneuper@59430: val _ = tracing "-------" wneuper@59430: in () end wneuper@59430: else (); wneuper@59430: case int_ord (size_of_term' t, size_of_term' u) of wneuper@59430: EQUAL => wneuper@59430: let val (f, ts) = strip_comb t and (g, us) = strip_comb u in wneuper@59430: (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) wneuper@59430: | ord => ord) wneuper@59430: end wneuper@59430: | ord => ord) wneuper@59430: and hd_ord (f, g) = (* ~ term.ML *) wneuper@59430: prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) wneuper@59430: and terms_ord str pr (ts, us) = wneuper@59430: list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us); wneuper@59430: in wneuper@59430: wneuper@59430: fun ord_make_polytest (pr:bool) thy (_: Rule.subst) tu = wneuper@59430: (term_ord' pr thy(***) tu = LESS ); wneuper@59430: wneuper@59430: end;(*local*) wneuper@59472: \ wneuper@59430: wneuper@59472: section \term order\ wneuper@59472: ML \ wneuper@59416: fun term_order (_: Rule.subst) tu = (term_ordI [] tu = LESS); wneuper@59472: \ s1210629013@52145: wneuper@59472: section \rulesets\ wneuper@59472: ML \ neuper@37954: val testerls = wneuper@59416: Rule.Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), wneuper@59416: erls = Rule.e_rls, srls = Rule.Erls, neuper@42451: calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}), wneuper@59416: Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}), wneuper@59416: Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}), wneuper@59416: Rule.Thm ("not_true",TermC.num_str @{thm not_true}), wneuper@59416: Rule.Thm ("not_false",TermC.num_str @{thm not_false}), wneuper@59416: Rule.Thm ("and_true",TermC.num_str @{thm and_true}), wneuper@59416: Rule.Thm ("and_false",TermC.num_str @{thm and_false}), wneuper@59416: Rule.Thm ("or_true",TermC.num_str @{thm or_true}), wneuper@59416: Rule.Thm ("or_false",TermC.num_str @{thm or_false}), wneuper@59416: Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}), wneuper@59416: Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}), neuper@37954: wneuper@59416: Rule.Calc ("Atools.is'_const",eval_const "#is_const_"), wneuper@59416: Rule.Calc ("Tools.matches",eval_matches ""), neuper@37954: wneuper@59416: Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow" ,eval_binop "#power_"), neuper@37954: wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), wneuper@59416: Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"), neuper@37954: wneuper@59416: Rule.Calc ("Atools.ident",eval_ident "#ident_")], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") wneuper@59406: }; wneuper@59472: \ wneuper@59472: ML \ neuper@37954: (*.for evaluation of conditions in rewrite rules.*) neuper@37954: (*FIXXXXXXME 10.8.02: handle like _simplify*) neuper@37954: val tval_rls = wneuper@59416: Rule.Rls{id = "tval_rls", preconds = [], wneuper@59397: rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), wneuper@59416: erls=testerls,srls = Rule.e_rls, neuper@42451: calc=[], errpatts = [], wneuper@59416: rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}), wneuper@59416: Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}), wneuper@59416: Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}), wneuper@59416: Rule.Thm ("not_true",TermC.num_str @{thm not_true}), wneuper@59416: Rule.Thm ("not_false",TermC.num_str @{thm not_false}), wneuper@59416: Rule.Thm ("and_true",TermC.num_str @{thm and_true}), wneuper@59416: Rule.Thm ("and_false",TermC.num_str @{thm and_false}), wneuper@59416: Rule.Thm ("or_true",TermC.num_str @{thm or_true}), wneuper@59416: Rule.Thm ("or_false",TermC.num_str @{thm or_false}), wneuper@59416: Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}), wneuper@59416: Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}), neuper@37954: wneuper@59416: Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}), neuper@37954: wneuper@59416: Rule.Thm ("root_ge0",TermC.num_str @{thm root_ge0}), wneuper@59416: Rule.Thm ("root_add_ge0",TermC.num_str @{thm root_add_ge0}), wneuper@59416: Rule.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}), wneuper@59416: Rule.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}), neuper@37954: wneuper@59416: Rule.Calc ("Atools.is'_const",eval_const "#is_const_"), wneuper@59416: Rule.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"), wneuper@59416: Rule.Calc ("Tools.matches",eval_matches ""), wneuper@59416: Rule.Calc ("Test.contains'_root", neuper@37954: eval_contains_root"#contains_root_"), neuper@37954: wneuper@59416: Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), wneuper@59416: Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), wneuper@59416: Rule.Calc ("Atools.pow" ,eval_binop "#power_"), neuper@37954: wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), wneuper@59416: Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"), neuper@37954: wneuper@59416: Rule.Calc ("Atools.ident",eval_ident "#ident_")], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") wneuper@59406: }; wneuper@59472: \ wneuper@59472: setup \KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\ neuper@52155: wneuper@59472: ML \ neuper@37954: (*make () dissappear*) neuper@37954: val rearrange_assoc = wneuper@59416: Rule.Rls{id = "rearrange_assoc", preconds = [], wneuper@59416: rew_ord = ("e_rew_ord",Rule.e_rew_ord), wneuper@59416: erls = Rule.e_rls, srls = Rule.e_rls, calc = [], errpatts = [], neuper@37954: rules = wneuper@59416: [Rule.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})), wneuper@59416: Rule.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") wneuper@59406: }; neuper@37954: neuper@37954: val ac_plus_times = wneuper@59416: Rule.Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order), wneuper@59416: erls = Rule.e_rls, srls = Rule.e_rls, calc = [], errpatts = [], neuper@37954: rules = wneuper@59416: [Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}), wneuper@59416: Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}), wneuper@59416: Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}), wneuper@59416: Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}), wneuper@59416: Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}), wneuper@59416: Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") wneuper@59406: }; neuper@37954: wneuper@59389: (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*) neuper@37954: val norm_equation = wneuper@59416: Rule.Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord), wneuper@59416: erls = tval_rls, srls = Rule.e_rls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add}) neuper@37954: ], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") wneuper@59406: }; wneuper@59472: \ wneuper@59472: ML \ neuper@37954: (* expects * distributed over + *) neuper@37954: val Test_simplify = wneuper@59416: Rule.Rls{id = "Test_simplify", preconds = [], wneuper@59397: rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), wneuper@59416: erls = tval_rls, srls = Rule.e_rls, s1210629013@55444: calc=[(*since 040209 filled by prep_rls'*)], errpatts = [], neuper@37954: rules = [ wneuper@59416: Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}), wneuper@59416: Rule.Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}), wneuper@59416: Rule.Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}), wneuper@59416: Rule.Thm ("rdistr_right_assoc_p",TermC.num_str @{thm rdistr_right_assoc_p}), wneuper@59416: Rule.Thm ("rdistr_div_right",TermC.num_str @{thm rdistr_div_right}), wneuper@59416: Rule.Thm ("rbinom_power_2",TermC.num_str @{thm rbinom_power_2}), neuper@37954: wneuper@59416: Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}), wneuper@59416: Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}), wneuper@59416: Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}), wneuper@59416: Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}), wneuper@59416: Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}), wneuper@59416: Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc}), neuper@37954: wneuper@59416: Rule.Thm ("radd_real_const_eq",TermC.num_str @{thm radd_real_const_eq}), wneuper@59416: Rule.Thm ("radd_real_const",TermC.num_str @{thm radd_real_const}), neuper@37954: (* these 2 rules are invers to distr_div_right wrt. termination. neuper@37954: thus they MUST be done IMMEDIATELY before calc *) wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_"), neuper@37954: wneuper@59416: Rule.Thm ("rcollect_right",TermC.num_str @{thm rcollect_right}), wneuper@59416: Rule.Thm ("rcollect_one_left",TermC.num_str @{thm rcollect_one_left}), wneuper@59416: Rule.Thm ("rcollect_one_left_assoc",TermC.num_str @{thm rcollect_one_left_assoc}), wneuper@59416: Rule.Thm ("rcollect_one_left_assoc_p",TermC.num_str @{thm rcollect_one_left_assoc_p}), neuper@37954: wneuper@59416: Rule.Thm ("rshift_nominator",TermC.num_str @{thm rshift_nominator}), wneuper@59416: Rule.Thm ("rcancel_den",TermC.num_str @{thm rcancel_den}), wneuper@59416: Rule.Thm ("rroot_square_inv",TermC.num_str @{thm rroot_square_inv}), wneuper@59416: Rule.Thm ("rroot_times_root",TermC.num_str @{thm rroot_times_root}), wneuper@59416: Rule.Thm ("rroot_times_root_assoc_p",TermC.num_str @{thm rroot_times_root_assoc_p}), wneuper@59416: Rule.Thm ("rsqare",TermC.num_str @{thm rsqare}), wneuper@59416: Rule.Thm ("power_1",TermC.num_str @{thm power_1}), wneuper@59416: Rule.Thm ("rtwo_of_the_same",TermC.num_str @{thm rtwo_of_the_same}), wneuper@59416: Rule.Thm ("rtwo_of_the_same_assoc_p",TermC.num_str @{thm rtwo_of_the_same_assoc_p}), neuper@37954: wneuper@59416: Rule.Thm ("rmult_1",TermC.num_str @{thm rmult_1}), wneuper@59416: Rule.Thm ("rmult_1_right",TermC.num_str @{thm rmult_1_right}), wneuper@59416: Rule.Thm ("rmult_0",TermC.num_str @{thm rmult_0}), wneuper@59416: Rule.Thm ("rmult_0_right",TermC.num_str @{thm rmult_0_right}), wneuper@59416: Rule.Thm ("radd_0",TermC.num_str @{thm radd_0}), wneuper@59416: Rule.Thm ("radd_0_right",TermC.num_str @{thm radd_0_right}) neuper@37954: ], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") s1210629013@55444: (*since 040209 filled by prep_rls': STest_simplify*) wneuper@59406: }; wneuper@59472: \ wneuper@59472: ML \ neuper@37954: (*isolate the root in a root-equation*) neuper@37954: val isolate_root = wneuper@59416: Rule.Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord), wneuper@59416: erls=tval_rls,srls = Rule.e_rls, calc=[], errpatts = [], wneuper@59416: rules = [Rule.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}), wneuper@59416: Rule.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}), wneuper@59416: Rule.Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}), wneuper@59416: Rule.Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}), wneuper@59416: Rule.Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}), wneuper@59416: Rule.Thm ("risolate_root_div",TermC.num_str @{thm risolate_root_div}) ], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) neuper@37954: "empty_script") wneuper@59406: }; neuper@37954: neuper@37954: (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) neuper@37954: val isolate_bdv = wneuper@59416: Rule.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord), wneuper@59416: erls=tval_rls,srls = Rule.e_rls, calc= [], errpatts = [], neuper@37954: rules = wneuper@59416: [Rule.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}), wneuper@59416: Rule.Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}), wneuper@59416: Rule.Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}), wneuper@59416: Rule.Thm ("mult_square",TermC.num_str @{thm mult_square}), wneuper@59416: Rule.Thm ("constant_square",TermC.num_str @{thm constant_square}), wneuper@59416: Rule.Thm ("constant_mult_square",TermC.num_str @{thm constant_mult_square}) neuper@37954: ], wneuper@59416: scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) neuper@37954: "empty_script") wneuper@59406: }; wneuper@59472: \ wneuper@59472: ML \val prep_rls' = LTool.prep_rls @{theory};\ wneuper@59472: setup \KEStore_Elems.add_rlss s1210629013@55444: [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), s1210629013@55444: ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), s1210629013@55444: ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), s1210629013@55444: ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), s1210629013@55444: ("matches", (Context.theory_name @{theory}, prep_rls' wneuper@59430: (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches",eval_matches "#matches_")])))] wneuper@59472: \ neuper@37954: wneuper@59472: subsection \problems\ neuper@37954: (** problem types **) wneuper@59472: setup \KEStore_Elems.add_pbts wneuper@59416: [(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Rule.e_rls, NONE, [])), wneuper@59406: (Specify.prep_pbt thy "pbl_test_equ" [] Celem.e_pblID s1210629013@55339: (["equation","test"], s1210629013@55339: [("#Given" ,["equality e_e","solveFor v_v"]), s1210629013@55339: ("#Where" ,["matches (?a = ?b) e_e"]), s1210629013@55339: ("#Find" ,["solutions v_v'i'"])], s1210629013@55339: assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_test_uni" [] Celem.e_pblID s1210629013@55339: (["univariate","equation","test"], s1210629013@55339: [("#Given" ,["equality e_e","solveFor v_v"]), s1210629013@55339: ("#Where" ,["matches (?a = ?b) e_e"]), s1210629013@55339: ("#Find" ,["solutions v_v'i'"])], s1210629013@55339: assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])), wneuper@59406: (Specify.prep_pbt thy "pbl_test_uni_lin" [] Celem.e_pblID s1210629013@55339: (["LINEAR","univariate","equation","test"], s1210629013@55339: [("#Given" ,["equality e_e","solveFor v_v"]), s1210629013@55339: ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^ s1210629013@55339: "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]), s1210629013@55339: ("#Find" ,["solutions v_v'i'"])], s1210629013@55339: assoc_rls' @{theory} "matches", wneuper@59430: SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))] wneuper@59472: \ wneuper@59472: ML \ wneuper@59416: Rule.rew_ord' := overwritel (! Rule.rew_ord', neuper@37954: [("termlessI", termlessI), neuper@37954: ("ord_make_polytest", ord_make_polytest false thy) neuper@37954: ]); neuper@37954: neuper@37954: val make_polytest = wneuper@59416: Rule.Rls{id = "make_polytest", preconds = []:term list, neuper@52105: rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), wneuper@59416: erls = testerls, srls = Rule.Erls, neuper@38014: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37954: ("POWER", ("Atools.pow", eval_binop "#power_")) neuper@42451: ], errpatts = [], wneuper@59416: rules = [Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}), neuper@37954: (*"a - b = a + (-1) * b"*) wneuper@59416: Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}), neuper@37954: (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) wneuper@59416: Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}), neuper@37954: (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) wneuper@59416: Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}), neuper@37954: (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) wneuper@59416: Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}), neuper@37954: (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) wneuper@59416: Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}), neuper@37954: (*"1 * z = z"*) wneuper@59416: Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}), neuper@37954: (*"0 * z = 0"*) wneuper@59416: Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}), neuper@37954: (*"0 + z = z"*) neuper@37954: neuper@37954: (*AC-rewriting*) wneuper@59416: Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}), neuper@37954: (* z * w = w * z *) wneuper@59416: Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}), neuper@37954: (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) wneuper@59416: Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}), neuper@37954: (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) wneuper@59416: Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}), neuper@37954: (*z + w = w + z*) wneuper@59416: Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}), neuper@37954: (*x + (y + z) = y + (x + z)*) wneuper@59416: Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}), neuper@37954: (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) neuper@37954: wneuper@59416: Rule.Thm ("sym_realpow_twoI", wneuper@59389: TermC.num_str (@{thm realpow_twoI} RS @{thm sym})), neuper@37954: (*"r1 * r1 = r1 ^^^ 2"*) wneuper@59416: Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}), neuper@37954: (*"r * r ^^^ n = r ^^^ (n + 1)"*) wneuper@59416: Rule.Thm ("sym_real_mult_2", wneuper@59389: TermC.num_str (@{thm real_mult_2} RS @{thm sym})), neuper@37954: (*"z1 + z1 = 2 * z1"*) wneuper@59416: Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}), neuper@37954: (*"z1 + (z1 + k) = 2 * z1 + k"*) neuper@37954: wneuper@59416: Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), neuper@37954: (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) wneuper@59416: Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}), neuper@37954: (*"[| l is_const; m is_const |] ==> neuper@37954: l * n + (m * n + k) = (l + m) * n + k"*) wneuper@59416: Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}), neuper@37954: (*"m is_const ==> n + m * n = (1 + m) * n"*) wneuper@59416: Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), neuper@37954: (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) neuper@37954: wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_") neuper@37954: ], wneuper@59416: scr = Rule.EmptyScr(*Rule.Prog ((Thm.term_of o the o (parse thy)) neuper@37954: scr_make_polytest)*) wneuper@59406: }; neuper@37954: neuper@37954: val expand_binomtest = wneuper@59416: Rule.Rls{id = "expand_binomtest", preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), wneuper@59416: erls = testerls, srls = Rule.Erls, neuper@38014: calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), neuper@38034: ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), neuper@37954: ("POWER", ("Atools.pow", eval_binop "#power_")) neuper@42451: ], errpatts = [], neuper@38001: rules = wneuper@59416: [Rule.Thm ("real_plus_binom_pow2" ,TermC.num_str @{thm real_plus_binom_pow2}), neuper@37954: (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*) wneuper@59416: Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}), neuper@37954: (*"(a + b)*(a + b) = ...*) wneuper@59416: Rule.Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}), neuper@38001: (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*) wneuper@59416: Rule.Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}), neuper@38001: (*"(a - b)*(a - b) = ...*) wneuper@59416: Rule.Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}), neuper@38001: (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*) wneuper@59416: Rule.Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}), neuper@38001: (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*) neuper@38001: (*RL 020915*) wneuper@59416: Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}), neuper@38001: (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) wneuper@59416: Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}), neuper@38001: (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) wneuper@59416: Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}), neuper@38001: (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*) wneuper@59416: Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}), neuper@38001: (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*) wneuper@59416: Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}), neuper@38001: (*(a*b)^^^n = a^^^n * b^^^n*) wneuper@59416: Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}), neuper@38001: (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *) wneuper@59416: Rule.Thm ("real_minus_binom_pow3",TermC.num_str @{thm real_minus_binom_pow3}), neuper@38001: (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *) neuper@37954: neuper@37954: wneuper@59416: (* Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}), neuper@38001: (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) wneuper@59416: Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}), neuper@38001: (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) wneuper@59416: Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}), neuper@38001: (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) wneuper@59416: Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}), neuper@38001: (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) neuper@38001: *) neuper@38001: wneuper@59416: Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}), neuper@38001: (*"1 * z = z"*) wneuper@59416: Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}), neuper@38001: (*"0 * z = 0"*) wneuper@59416: Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}), neuper@38001: (*"0 + z = z"*) neuper@37954: wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_"), neuper@38001: (* wneuper@59416: Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}), neuper@38001: (*AC-rewriting*) wneuper@59416: Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}), wneuper@59416: Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}), wneuper@59416: Rule.Thm ("add_commute",TermC.num_str @{thm add_commute}), wneuper@59416: Rule.Thm ("add_left_commute",TermC.num_str @{thm add_left_commute}), wneuper@59416: Rule.Thm ("add_assoc",TermC.num_str @{thm add_assoc}), neuper@38001: *) neuper@38001: wneuper@59416: Rule.Thm ("sym_realpow_twoI", wneuper@59389: TermC.num_str (@{thm realpow_twoI} RS @{thm sym})), neuper@38001: (*"r1 * r1 = r1 ^^^ 2"*) wneuper@59416: Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}), neuper@38001: (*"r * r ^^^ n = r ^^^ (n + 1)"*) wneuper@59416: (*Rule.Thm ("sym_real_mult_2", wneuper@59389: TermC.num_str (@{thm real_mult_2} RS @{thm sym})), neuper@38001: (*"z1 + z1 = 2 * z1"*)*) wneuper@59416: Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}), neuper@38001: (*"z1 + (z1 + k) = 2 * z1 + k"*) neuper@37954: wneuper@59416: Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), neuper@38001: (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) wneuper@59416: Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}), neuper@38001: (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) wneuper@59416: Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}), neuper@38001: (*"m is_const ==> n + m * n = (1 + m) * n"*) wneuper@59416: Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), neuper@38001: (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) neuper@37954: wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"), wneuper@59416: Rule.Calc ("Atools.pow", eval_binop "#power_") neuper@38001: ], wneuper@59416: scr = Rule.EmptyScr wneuper@59186: (*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*) wneuper@59406: }; wneuper@59472: \ wneuper@59472: setup \KEStore_Elems.add_rlss s1210629013@55444: [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)), wneuper@59472: ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\ wneuper@59472: setup \KEStore_Elems.add_rlss wneuper@59430: [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)), wneuper@59430: ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)), wneuper@59472: ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\ wneuper@59430: wneuper@59472: section \problems\ wneuper@59472: setup \KEStore_Elems.add_pbts wneuper@59430: [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Celem.e_pblID wneuper@59430: (["plain_square","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^ wneuper@59430: "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ wneuper@59430: "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ wneuper@59430: "(matches ( v_v ^^^2 = 0) e_e)"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: assoc_rls' @{theory} "matches", wneuper@59430: SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_poly" [] Celem.e_pblID wneuper@59430: (["polynomial","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), wneuper@59430: ("#Where" ,["HOL.False"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.e_rls, SOME "solve (e_e::bool, v_v)", [])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Celem.e_pblID wneuper@59430: (["degree_two","polynomial","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Celem.e_pblID wneuper@59430: (["pq_formula","degree_two","polynomial","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Celem.e_pblID wneuper@59430: (["abc_formula","degree_two","polynomial","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_root" [] Celem.e_pblID wneuper@59430: (["squareroot","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["precond_rootpbl v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.append_rls "contains_root" Rule.e_rls [Rule.Calc ("Test.contains'_root", wneuper@59430: eval_contains_root "#contains_root_")], wneuper@59430: SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_norm" [] Celem.e_pblID wneuper@59430: (["normalise","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,[]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Celem.e_pblID wneuper@59430: (["sqroot-test","univariate","equation","test"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["precond_rootpbl v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: Rule.e_rls, SOME "solve (e_e::bool, v_v)", [])), wneuper@59430: (Specify.prep_pbt thy "pbl_test_intsimp" [] Celem.e_pblID wneuper@59430: (["inttype","test"], wneuper@59430: [("#Given" ,["intTestGiven t_t"]), wneuper@59430: ("#Where" ,[]), wneuper@59430: ("#Find" ,["intTestFind s_s"])], wneuper@59472: Rule.e_rls, NONE, [["Test","intsimp"]]))]\ wneuper@59430: wneuper@59472: section \methods\ wneuper@59472: subsection \differentiate\ wneuper@59430: partial_function (tailrec) dummy1 :: "real \ real" wneuper@59430: where "dummy1 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID wneuper@59430: (["Test"], [], wneuper@59430: {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls, wneuper@59473: crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")] wneuper@59473: \ wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID wneuper@59430: (["Test","solve_linear"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["matches (?a = ?b) e_e"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, wneuper@59430: prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [], wneuper@59430: nrls = Test_simplify}, wneuper@59430: "Script Solve_linear (e_e::bool) (v_v::real)= " ^ wneuper@59430: "(let e_e = " ^ wneuper@59430: " Repeat " ^ wneuper@59430: " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^ wneuper@59430: " (Rewrite_Set Test_simplify False))) e_e" ^ wneuper@59430: " in [e_e::bool])")] wneuper@59472: \ wneuper@59472: subsection \root equation\ wneuper@59430: partial_function (tailrec) dummy2 :: "real \ real" wneuper@59430: where "dummy2 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_sqrt" [] Celem.e_metID wneuper@59430: (*root-equation, version for tests before 8.01.01*) wneuper@59430: (["Test","sqrt-equ-test"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["contains_root (e_e::bool)"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls, wneuper@59430: srls = Rule.append_rls "srls_contains_root" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.contains'_root",eval_contains_root "")], wneuper@59430: prls = Rule.append_rls "prls_contains_root" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.contains'_root",eval_contains_root "")], wneuper@59430: calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[], wneuper@59430: asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)}, wneuper@59430: "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ wneuper@59430: "(let e_e = " ^ wneuper@59430: " ((While (contains_root e_e) Do" ^ wneuper@59430: " ((Rewrite square_equation_left True) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set rearrange_assoc False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set isolate_root False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))) @@" ^ wneuper@59430: " (Try (Rewrite_Set norm_equation False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))" ^ wneuper@59430: " e_e" ^ wneuper@59430: " in [e_e::bool])")] wneuper@59472: \ wneuper@59430: partial_function (tailrec) dummy3 :: "real \ real" wneuper@59430: where "dummy3 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_sqrt2" [] Celem.e_metID wneuper@59430: (*root-equation ... for test-*.sml until 8.01*) wneuper@59430: (["Test","squ-equ-test2"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls, wneuper@59430: srls = Rule.append_rls "srls_contains_root" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.contains'_root",eval_contains_root"")], wneuper@59430: prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[], wneuper@59430: asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)}, wneuper@59430: "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ wneuper@59430: "(let e_e = " ^ wneuper@59430: " ((While (contains_root e_e) Do" ^ wneuper@59430: " ((Rewrite square_equation_left True) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set rearrange_assoc False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set isolate_root False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))) @@" ^ wneuper@59430: " (Try (Rewrite_Set norm_equation False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))" ^ wneuper@59430: " e_e;" ^ wneuper@59430: " (L_L::bool list) = Tac subproblem_equation_dummy; " ^ wneuper@59430: " L_L = Tac solve_equation_dummy " ^ wneuper@59430: " in Check_elementwise L_L {(v_v::real). Assumptions})")] wneuper@59472: \ wneuper@59477: wneuper@59477: partial_function (tailrec) solve_root_equation :: wneuper@59477: "bool \ real \ bool list" wneuper@59477: where "minisubpbl e_e v_v = wneuper@59477: (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ wneuper@59477: (Try (Rewrite_Set ''Test_simplify'' False))) e_e; wneuper@59477: (L_L::bool list) = wneuper@59477: (SubProblem (''TestX'', wneuper@59477: [''LINEAR'', ''univariate'', ''equation'', ''test''], wneuper@59477: [''Test'', ''solve_linear'']) wneuper@59477: [BOOL e_e, REAL v_v]) wneuper@59477: in Check_elementwise L_L {(v_v::real). Assumptions})" wneuper@59477: wneuper@59477: (* ^^^used for test/../Minisubpbl/ wneuper@59477: # difference between partial_function above and Script below: wneuper@59477: "Solve_root_equation" is a constant, which is NOT accepted by partial_function wneuper@59477: wneuper@59477: # differences between original "Solve_root_equation" and the version below: wneuper@59477: (1) the program name, see note above wneuper@59477: (2) the first argument of SubProblem: ''Test''' is NOT accepted by partial_function, wneuper@59477: thus previous change-set Test' \ TestX wneuper@59477: ''Test'#TODO#''. Note: this change is NOT recognised by Interpret! wneuper@59477: *) wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID wneuper@59430: (*tests subproblem fixed linear*) wneuper@59430: (["Test","squ-equ-test-subpbl1"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["precond_rootmet v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, wneuper@59430: prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")], wneuper@59430: calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}, wneuper@59477: "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ wneuper@59477: " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^ wneuper@59477: " (Try (Rewrite_Set Test_simplify False))) e_e; " ^ wneuper@59477: " (L_L::bool list) = " ^ wneuper@59477: " (SubProblem (''TestX'', " ^ wneuper@59477: " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^ wneuper@59477: " [''Test'', ''solve_linear'']) " ^ wneuper@59477: " [BOOL e_e, REAL v_v]) " ^ wneuper@59477: " in Check_elementwise L_L {(v_v::real). Assumptions}) ")] wneuper@59472: \ wneuper@59430: partial_function (tailrec) dummy7 :: "real \ real" wneuper@59430: where "dummy7 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_eq1" [] Celem.e_metID wneuper@59430: (*root-equation1:*) wneuper@59430: (["Test","square_equation1"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls, wneuper@59430: srls = Rule.append_rls "srls_contains_root" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls, wneuper@59430: errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""), wneuper@59430: ("square_equation_right","")]*)}, wneuper@59430: "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ wneuper@59430: "(let e_e = " ^ wneuper@59430: " ((While (contains_root e_e) Do" ^ wneuper@59430: " ((Rewrite square_equation_left True) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set rearrange_assoc False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set isolate_root False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))) @@" ^ wneuper@59430: " (Try (Rewrite_Set norm_equation False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))" ^ wneuper@59430: " e_e;" ^ wneuper@59430: " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^ wneuper@59430: " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^ wneuper@59430: " in Check_elementwise L_L {(v_v::real). Assumptions})")] wneuper@59472: \ wneuper@59430: partial_function (tailrec) dummy8 :: "real \ real" wneuper@59430: where "dummy8 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID wneuper@59430: (*root-equation2*) wneuper@59430: (["Test","square_equation2"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls, wneuper@59430: srls = Rule.append_rls "srls_contains_root" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.contains'_root",eval_contains_root"")], wneuper@59430: prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[], wneuper@59430: asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)}, wneuper@59430: "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ wneuper@59430: "(let e_e = " ^ wneuper@59430: " ((While (contains_root e_e) Do" ^ wneuper@59430: " (((Rewrite square_equation_left True) Or " ^ wneuper@59430: " (Rewrite square_equation_right True)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set rearrange_assoc False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set isolate_root False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))) @@" ^ wneuper@59430: " (Try (Rewrite_Set norm_equation False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))" ^ wneuper@59430: " e_e;" ^ wneuper@59430: " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^ wneuper@59430: " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^ wneuper@59430: " in Check_elementwise L_L {(v_v::real). Assumptions})")] wneuper@59472: \ wneuper@59430: partial_function (tailrec) dummy9 :: "real \ real" wneuper@59430: where "dummy9 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID wneuper@59430: (*root-equation*) wneuper@59430: (["Test","square_equation"], wneuper@59430: [("#Given" ,["equality e_e","solveFor v_v"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls, wneuper@59430: srls = Rule.append_rls "srls_contains_root" Rule.e_rls wneuper@59430: [Rule.Calc ("Test.contains'_root",eval_contains_root"")], wneuper@59430: prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[], wneuper@59430: asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)}, wneuper@59430: "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ wneuper@59430: "(let e_e = " ^ wneuper@59430: " ((While (contains_root e_e) Do" ^ wneuper@59430: " (((Rewrite square_equation_left True) Or" ^ wneuper@59430: " (Rewrite square_equation_right True)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set rearrange_assoc False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set isolate_root False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))) @@" ^ wneuper@59430: " (Try (Rewrite_Set norm_equation False)) @@" ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)))" ^ wneuper@59430: " e_e;" ^ wneuper@59430: " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^ wneuper@59430: " [no_met]) [BOOL e_e, REAL v_v])" ^ wneuper@59430: " in Check_elementwise L_L {(v_v::real). Assumptions})")] wneuper@59472: \ wneuper@59430: partial_function (tailrec) dummy10 :: "real \ real" wneuper@59430: where "dummy10 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID wneuper@59430: (*solve_plain_square*) wneuper@59430: (["Test","solve_plain_square"], wneuper@59430: [("#Given",["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^ wneuper@59430: "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ wneuper@59430: "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ wneuper@59430: "(matches ( v_v ^^^2 = 0) e_e)"]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls, wneuper@59430: prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*, wneuper@59430: asm_rls=[],asm_thm=[]*)}, wneuper@59430: "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^ wneuper@59430: " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False)) @@ " ^ wneuper@59430: " ((Rewrite square_equality_0 False) Or " ^ wneuper@59430: " (Rewrite square_equality True)) @@ " ^ wneuper@59430: " (Try (Rewrite_Set tval_rls False))) e_e " ^ wneuper@59430: " in ((Or_to_List e_e)::bool list))")] wneuper@59472: \ wneuper@59472: subsection \polynomial equation\ wneuper@59430: partial_function (tailrec) dummy11 :: "real \ real" wneuper@59430: where "dummy11 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID wneuper@59430: (["Test","norm_univar_equation"], wneuper@59430: [("#Given",["equality e_e","solveFor v_v"]), wneuper@59430: ("#Where" ,[]), wneuper@59430: ("#Find" ,["solutions v_v'i'"])], wneuper@59430: {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls, wneuper@59430: errpats = [], nrls = Rule.e_rls}, wneuper@59430: "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^ wneuper@59430: " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^ wneuper@59430: " (Try (Rewrite_Set Test_simplify False))) e_e " ^ wneuper@59430: " in (SubProblem (Test',[univariate,equation,test], " ^ wneuper@59430: " [no_met]) [BOOL e_e, REAL v_v]))")] wneuper@59472: \ wneuper@59472: subsection \diophantine equation\ wneuper@59430: partial_function (tailrec) dummy12 :: "real \ real" wneuper@59430: where "dummy12 xxx = xxx" wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID wneuper@59430: (["Test","intsimp"], wneuper@59430: [("#Given" ,["intTestGiven t_t"]), wneuper@59430: ("#Where" ,[]), wneuper@59430: ("#Find" ,["intTestFind s_s"])], wneuper@59430: {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], wneuper@59430: crls = tval_rls, errpats = [], nrls = Test_simplify}, wneuper@59430: "Script STest_simplify (t_t::int) = " ^ wneuper@59430: "(Repeat " ^ wneuper@59430: " ((Try (Calculate PLUS)) @@ " ^ wneuper@59430: " (Try (Calculate TIMES))) t_t::int)")] wneuper@59472: \ wneuper@59430: neuper@37906: end