1.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Mon Jan 20 16:15:34 2014 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Tue Jan 21 00:27:44 2014 +0100
     1.3 @@ -399,25 +399,6 @@
     1.4  	else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
     1.5  in del k [] ptyps end;
     1.6  
     1.7 -fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]
     1.8 -			 
     1.9 -  | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
    1.10 -((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)
    1.11 -     if k=k'
    1.12 -     then ((Ptyp (k', [pbt], ps))::pys)
    1.13 -     else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
    1.14 -	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
    1.15 -)			 
    1.16 -  | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
    1.17 -((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)
    1.18 -     if k=k'
    1.19 -     then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
    1.20 -     else 
    1.21 -	 if length pys = 0
    1.22 -	 then error ("insert: not found "^(strs2str (d:pblID)))
    1.23 -	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
    1.24 -);
    1.25 -
    1.26  
    1.27  fun coll_pblguhs pbls =
    1.28      let fun node coll (Ptyp (_,[n],ns)) =

     2.1 --- a/src/Tools/isac/KEStore.thy	Mon Jan 20 16:15:34 2014 +0100
     2.2 +++ b/src/Tools/isac/KEStore.thy	Tue Jan 21 00:27:44 2014 +0100
     2.3 @@ -25,6 +25,8 @@
     2.4    val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory
     2.5    val get_cas: theory -> cas_elem list
     2.6    val add_cas: cas_elem list -> theory -> theory
     2.7 +  val get_ptyps: theory -> ptyps
     2.8 +  val store_pbts: (pbt * pblID) list -> theory -> theory
     2.9    (*etc*)
    2.10  end;                               
    2.11  
    2.12 @@ -59,6 +61,17 @@
    2.13    fun get_cas thy = Data.get thy
    2.14    fun add_cas cas = Data.map (union_overwrite cas_eq cas)
    2.15  
    2.16 +  structure Data = Theory_Data (
    2.17 +    type T = ptyps;
    2.18 +    val empty = [e_Ptyp];
    2.19 +    val extend = I;
    2.20 +    val merge = merge_ptyps;
    2.21 +    );
    2.22 +  fun get_ptyps thy = Data.get thy;
    2.23 +  fun store_pbts pbts = let
    2.24 +          fun store_pbts' (pbt, pblID) = ((*map writeln pblID;*) rev pblID |> insrt pblID pbt)
    2.25 +        in fold store_pbts' pbts |> Data.map end;
    2.26 +
    2.27    (*etc*)
    2.28  end;
    2.29  *}

     3.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Mon Jan 20 16:15:34 2014 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Tue Jan 21 00:27:44 2014 +0100
     3.3 @@ -55,6 +55,16 @@
     3.4  (* show_ptyps();
     3.5     *)
     3.6  *}
     3.7 +setup {* KEStore_Elems.store_pbts
     3.8 +  [(prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])),
     3.9 +    (prep_pbt thy "pbl_algein_numsym" [] e_pblID
    3.10 +      (["numerischSymbolische", "Berechnung"],
    3.11 +        [("#Given",
    3.12 +            ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
    3.13 +              "KantenSenkrecht s_s", "KantenOben o_o"]),
    3.14 +          ("#Find", ["GesamtLaenge l_l"])],
    3.15 +        e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))]; *}
    3.16 +
    3.17  ML {*
    3.18  (** methods **)
    3.19  

     4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Jan 20 16:15:34 2014 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Jan 21 00:27:44 2014 +0100
     4.3 @@ -173,8 +173,48 @@
     4.4    append_rls "e_rls" e_rls [], 
     4.5    NONE, 
     4.6    [["Equation","fromFunction"]]));
     4.7 -
     4.8 +KEStore_Elems.get_ptyps @{theory};
     4.9  *}
    4.10 +setup {* KEStore_Elems.store_pbts
    4.11 +  [(prep_pbt thy "pbl_bieg" [] e_pblID
    4.12 +      (["Biegelinien"],
    4.13 +        [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
    4.14 +          (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
    4.15 +          ("#Find"  ,["Biegelinie b_b"]),
    4.16 +          ("#Relate",["Randbedingungen r_b"])],
    4.17 +        append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
    4.18 +    (prep_pbt thy "pbl_bieg_mom" [] e_pblID
    4.19 +      (["MomentBestimmte","Biegelinien"],
    4.20 +        [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
    4.21 +          (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
    4.22 +          ("#Find"  ,["Biegelinie b_b"]),
    4.23 +          ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
    4.24 +        ],
    4.25 +        append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
    4.26 +    (prep_pbt thy "pbl_bieg_momg" [] e_pblID
    4.27 +      (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
    4.28 +        [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
    4.29 +    (prep_pbt thy "pbl_bieg_einf" [] e_pblID
    4.30 +      (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
    4.31 +        [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
    4.32 +    (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
    4.33 +      (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
    4.34 +        [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
    4.35 +    (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
    4.36 +      (["vonBelastungZu","Biegelinien"],
    4.37 +          [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
    4.38 +            ("#Find"  ,["Funktionen funs'''"])],
    4.39 +        append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
    4.40 +    (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
    4.41 +      (["setzeRandbedingungen","Biegelinien"],
    4.42 +          [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
    4.43 +            ("#Find"  ,["Gleichungen equs'''"])],
    4.44 +        append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
    4.45 +    (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
    4.46 +      (["makeFunctionTo","equation"],
    4.47 +          [("#Given" ,["functionEq fu_n","substitution su_b"]),
    4.48 +            ("#Find"  ,["equality equ'''"])],
    4.49 +        append_rls "e_rls" e_rls [], NONE, [["Equation","fromFunction"]]))] *}
    4.50  ML {*
    4.51  (** methods **)
    4.52  

     5.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Jan 20 16:15:34 2014 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Tue Jan 21 00:27:44 2014 +0100
     5.3 @@ -272,6 +272,23 @@
     5.4    append_rls "e_rls" e_rls [],
     5.5    SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]]));
     5.6  *}
     5.7 +setup {* KEStore_Elems.store_pbts
     5.8 +  [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
     5.9 +    (prep_pbt thy "pbl_fun_deriv" [] e_pblID
    5.10 +      (["derivative_of","function"],
    5.11 +        [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    5.12 +          ("#Find"  ,["derivative f_f'"])],
    5.13 +        append_rls "e_rls" e_rls [],
    5.14 +        SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
    5.15 +			  ["diff","after_simplification"]])),
    5.16 +    (*here "named" is used differently from Integration"*)
    5.17 +    (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
    5.18 +      (["named","derivative_of","function"],
    5.19 +        [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
    5.20 +          ("#Find"  ,["derivativeEq f_f'"])],
    5.21 +        append_rls "e_rls" e_rls [],
    5.22 +        SOME "Differentiate (f_f, v_v)",
    5.23 +        [["diff","differentiate_equality"]]))] *}
    5.24  ML {*
    5.25  
    5.26  (** methods **)

     6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 20 16:15:34 2014 +0100
     6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Tue Jan 21 00:27:44 2014 +0100
     6.3 @@ -135,8 +135,44 @@
     6.4     ("#Relate",["additionalRels r_s"])
     6.5    ],
     6.6    e_rls, NONE, []));
     6.7 -
     6.8  *}
     6.9 +setup {* KEStore_Elems.store_pbts
    6.10 +  [(prep_pbt thy "pbl_fun_max" [] e_pblID
    6.11 +      (["maximum_of","function"],
    6.12 +        [("#Given" ,["fixedValues f_ix"]),
    6.13 +          ("#Find"  ,["maximum m_m","valuesFor v_s"]),
    6.14 +          ("#Relate",["relations r_s"])],
    6.15 +        e_rls, NONE, [])),
    6.16 +    (prep_pbt thy "pbl_fun_make" [] e_pblID
    6.17 +      (["make","function"]:pblID,
    6.18 +        [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    6.19 +          ("#Find"  ,["functionEq f_1"])],
    6.20 +        e_rls, NONE, [])),
    6.21 +    (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
    6.22 +      (["by_explicit","make","function"]:pblID,
    6.23 +        [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    6.24 +          ("#Find"  ,["functionEq f_1"])],
    6.25 +      e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])),
    6.26 +    (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
    6.27 +      (["by_new_variable","make","function"]:pblID,
    6.28 +        [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    6.29 +          (*WN.12.5.03: precond for distinction still missing*)
    6.30 +          ("#Find"  ,["functionEq f_1"])],
    6.31 +      e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])),
    6.32 +    (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
    6.33 +      (["on_interval","maximum_of","function"]:pblID,
    6.34 +        [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
    6.35 +          (*WN.12.5.03: precond for distinction still missing*)
    6.36 +          ("#Find"  ,["maxArgument v_0"])],
    6.37 +      e_rls, NONE, [])),
    6.38 +    (prep_pbt thy "pbl_tool" [] e_pblID
    6.39 +      (["tool"]:pblID, [], e_rls, NONE, [])),
    6.40 +    (prep_pbt thy "pbl_tool_findvals" [] e_pblID
    6.41 +      (["find_values","tool"]:pblID,
    6.42 +        [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
    6.43 +          ("#Find"  ,["valuesFor v_ls"]),
    6.44 +          ("#Relate",["additionalRels r_s"])],
    6.45 +      e_rls, NONE, []))] *}
    6.46  ML{*
    6.47  
    6.48  (** methods, scripts not yet implemented **)

     7.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 20 16:15:34 2014 +0100
     7.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Jan 21 00:27:44 2014 +0100
     7.3 @@ -33,6 +33,14 @@
     7.4  show_ptyps();
     7.5  get_pbt ["diophantine","equation"];
     7.6  *}
     7.7 +setup {* KEStore_Elems.store_pbts
     7.8 +  [(prep_pbt thy "pbl_equ_dio" [] e_pblID
     7.9 +      (["diophantine","equation"],
    7.10 +        [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    7.11 +          (*                                      TODO: drop ^^^^^*)
    7.12 +          ("#Where" ,[]),
    7.13 +          ("#Find"  ,["boolTestFind s_s"])],
    7.14 +        e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
    7.15  
    7.16  text {*method solving the usecase*}
    7.17  ML {*

     8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jan 20 16:15:34 2014 +0100
     8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Tue Jan 21 00:27:44 2014 +0100
     8.3 @@ -539,6 +539,90 @@
     8.4     *)
     8.5  
     8.6  *}
     8.7 +setup {* KEStore_Elems.store_pbts
     8.8 +  [(prep_pbt thy "pbl_equsys" [] e_pblID
     8.9 +      (["system"],
    8.10 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.11 +          ("#Find"  ,["solution ss'''"](*''' is copy-named*))],
    8.12 +        append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
    8.13 +    (prep_pbt thy "pbl_equsys_lin" [] e_pblID
    8.14 +      (["LINEAR", "system"],
    8.15 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.16 +          (*TODO.WN050929 check linearity*)
    8.17 +          ("#Find"  ,["solution ss'''"])],
    8.18 +        append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
    8.19 +    (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
    8.20 +      (["2x2", "LINEAR", "system"],
    8.21 +      (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
    8.22 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.23 +          ("#Where"  ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
    8.24 +          ("#Find"  ,["solution ss'''"])],
    8.25 +        append_rls "prls_2x2_linear_system" e_rls 
    8.26 +			    [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
    8.27 +			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
    8.28 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    8.29 +			      Calc ("HOL.eq",eval_equal "#equal_")], 
    8.30 +        SOME "solveSystem e_s v_s", [])),
    8.31 +    (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
    8.32 +      (["triangular", "2x2", "LINEAR", "system"],
    8.33 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.34 +          ("#Where",
    8.35 +            ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
    8.36 +              "    v_s  from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
    8.37 +          ("#Find"  ,["solution ss'''"])],
    8.38 +        prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])),
    8.39 +    (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
    8.40 +      (["normalize", "2x2", "LINEAR", "system"],
    8.41 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.42 +          ("#Find"  ,["solution ss'''"])],
    8.43 +      append_rls "e_rls" e_rls [(*for preds in where_*)], 
    8.44 +      SOME "solveSystem e_s v_s", 
    8.45 +      [["EqSystem","normalize","2x2"]])),
    8.46 +    (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
    8.47 +      (["3x3", "LINEAR", "system"],
    8.48 +        (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
    8.49 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.50 +          ("#Where"  ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
    8.51 +          ("#Find"  ,["solution ss'''"])],
    8.52 +        append_rls "prls_3x3_linear_system" e_rls 
    8.53 +			    [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
    8.54 +			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
    8.55 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    8.56 +			      Calc ("HOL.eq",eval_equal "#equal_")],
    8.57 +        SOME "solveSystem e_s v_s", [])),
    8.58 +    (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
    8.59 +      (["4x4", "LINEAR", "system"],
    8.60 +        (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
    8.61 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.62 +          ("#Where"  ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
    8.63 +          ("#Find"  ,["solution ss'''"])],
    8.64 +        append_rls "prls_4x4_linear_system" e_rls 
    8.65 +			    [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
    8.66 +			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
    8.67 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    8.68 +			      Calc ("HOL.eq",eval_equal "#equal_")],
    8.69 +        SOME "solveSystem e_s v_s", [])),
    8.70 +    (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
    8.71 +      (["triangular", "4x4", "LINEAR", "system"],
    8.72 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.73 +          ("#Where" , (*accepts missing variables up to diagional form*)
    8.74 +            ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
    8.75 +              "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
    8.76 +              "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
    8.77 +              "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
    8.78 +          ("#Find"  ,["solution ss'''"])],
    8.79 +      append_rls "prls_tri_4x4_lin_sys" prls_triangular
    8.80 +	      [Calc ("Atools.occurs'_in",eval_occurs_in "")], 
    8.81 +      SOME "solveSystem e_s v_s", 
    8.82 +      [["EqSystem","top_down_substitution","4x4"]])),
    8.83 +    (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
    8.84 +      (["normalize", "4x4", "LINEAR", "system"],
    8.85 +        [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    8.86 +          (*LENGTH is checked 1 level above*)
    8.87 +          ("#Find"  ,["solution ss'''"])],
    8.88 +        append_rls "e_rls" e_rls [(*for preds in where_*)], 
    8.89 +        SOME "solveSystem e_s v_s", 
    8.90 +        [["EqSystem","normalize","4x4"]]))] *}
    8.91  ML {*
    8.92  (** methods **)
    8.93  

     9.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 20 16:15:34 2014 +0100
     9.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Tue Jan 21 00:27:44 2014 +0100
     9.3 @@ -68,8 +68,24 @@
     9.4     ("#Find"  ,["solutions v_v'i'"])
     9.5    ],
     9.6    univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
     9.7 +*}
     9.8 +setup {* KEStore_Elems.store_pbts
     9.9 +  [(prep_pbt thy "pbl_equ" [] e_pblID
    9.10 +      (["equation"],
    9.11 +        [("#Given" ,["equality e_e","solveFor v_v"]),
    9.12 +          ("#Where" ,["matches (?a = ?b) e_e"]),
    9.13 +          ("#Find"  ,["solutions v_v'i'"])],
    9.14 +        append_rls "equation_prls" e_rls  [Calc ("Tools.matches",eval_matches "")],
    9.15 +        SOME "solve (e_e::bool, v_v)", [])),
    9.16 +    (prep_pbt thy "pbl_equ_univ" [] e_pblID
    9.17 +      (["univariate","equation"],
    9.18 +        [("#Given" ,["equality e_e","solveFor v_v"]),
    9.19 +          ("#Where" ,["matches (?a = ?b) e_e"]),
    9.20 +          ("#Find"  ,["solutions v_v'i'"])],
    9.21 +        univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *}
    9.22  
    9.23  
    9.24 +ML{*
    9.25  (*.function for handling the cas-input "solve (x+1=2, x)":
    9.26     make a model which is already in ptree-internal format.*)
    9.27  (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");

    10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Mon Jan 20 16:15:34 2014 +0100
    10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Tue Jan 21 00:27:44 2014 +0100
    10.3 @@ -76,7 +76,16 @@
    10.4     ("#Find"  ,["sorted s_"])
    10.5    ],
    10.6    []));
    10.7 +*}
    10.8 +setup {* KEStore_Elems.store_pbts
    10.9 +  [(prep_pbt @{theory "InsSort"}
   10.10 +      (["functional"]:pblID,
   10.11 +        [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], [])),
   10.12 +    (prep_pbt @{theory "InsSort"}
   10.13 +      (["inssort","functional"]:pblID,
   10.14 +        [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], []))] *}
   10.15  
   10.16 +ML {*
   10.17  (** method, 
   10.18      todo: implementation needs extra object-level lists **)
   10.19  

    11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jan 20 16:15:34 2014 +0100
    11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Jan 21 00:27:44 2014 +0100
    11.3 @@ -359,6 +359,22 @@
    11.4    [["diff","integration","named"]]));
    11.5   
    11.6  *}
    11.7 +setup {* KEStore_Elems.store_pbts
    11.8 +  [(prep_pbt thy "pbl_fun_integ" [] e_pblID
    11.9 +      (["integrate","function"],
   11.10 +        [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
   11.11 +          ("#Find"  ,["antiDerivative F_F"])],
   11.12 +        append_rls "e_rls" e_rls [(*for preds in where_*)], 
   11.13 +        SOME "Integrate (f_f, v_v)", 
   11.14 +        [["diff","integration"]])),
   11.15 +    (*here "named" is used differently from Differentiation"*)
   11.16 +    (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
   11.17 +      (["named","integrate","function"],
   11.18 +        [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
   11.19 +          ("#Find"  ,["antiDerivativeName F_F"])],
   11.20 +        append_rls "e_rls" e_rls [(*for preds in where_*)], 
   11.21 +        SOME "Integrate (f_f, v_v)", 
   11.22 +        [["diff","integration","named"]]))] *}
   11.23  ML {*
   11.24  (** methods **)
   11.25  

    12.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 20 16:15:34 2014 +0100
    12.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Jan 21 00:27:44 2014 +0100
    12.3 @@ -73,6 +73,24 @@
    12.4      append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    12.5      [["SignalProcessing","Z_Transform","Inverse"]]));
    12.6  *}
    12.7 +setup {* KEStore_Elems.store_pbts
    12.8 +  [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
    12.9 +    (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
   12.10 +      (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])),
   12.11 +    (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
   12.12 +      (["Inverse", "Z_Transform", "SignalProcessing"],
   12.13 +        (*^ capital letter breaks coding standard
   12.14 +          because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
   12.15 +        [("#Given" ,["filterExpression (X_eq::bool)"]),
   12.16 +          ("#Find"  ,["stepResponse (n_eq::bool)"])],
   12.17 +        append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
   12.18 +        [["SignalProcessing","Z_Transform","Inverse"]])),
   12.19 +    (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
   12.20 +      (["Inverse", "Z_Transform", "SignalProcessing"],
   12.21 +        [("#Given" ,["filterExpression X_eq"]),
   12.22 +          ("#Find"  ,["stepResponse n_eq"])],
   12.23 +        append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
   12.24 +        [["SignalProcessing","Z_Transform","Inverse"]]))] *}
   12.25  
   12.26  subsection {*Define Name and Signature for the Method*}
   12.27  consts

    13.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 20 16:15:34 2014 +0100
    13.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Jan 21 00:27:44 2014 +0100
    13.3 @@ -139,7 +139,20 @@
    13.4    ],
    13.5    LinEq_prls, SOME "solve (e_e::bool, v_v)",
    13.6    [["LinEq","solve_lineq_equation"]]));
    13.7 +*}
    13.8 +setup {* KEStore_Elems.store_pbts
    13.9 +  [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
   13.10 +      (["LINEAR", "univariate", "equation"],
   13.11 +        [("#Given" ,["equality e_e", "solveFor v_v"]),
   13.12 +          ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
   13.13 +              "Not( (lhs e_e) is_polyrat_in v_v)",
   13.14 +              "Not( (rhs e_e) is_polyrat_in v_v)",
   13.15 +              "((lhs e_e) has_degree_in v_v)=1",
   13.16 +	            "((rhs e_e) has_degree_in v_v)=1"]),
   13.17 +          ("#Find"  ,["solutions v_v'i'"])],
   13.18 +        LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *}
   13.19  
   13.20 +ML {*
   13.21  (*-------------- methods------------------------------------------------------*)
   13.22  store_met
   13.23   (prep_met thy "met_eqlin" [] e_metID

    14.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Jan 20 16:15:34 2014 +0100
    14.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Tue Jan 21 00:27:44 2014 +0100
    14.3 @@ -40,6 +40,15 @@
    14.4    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
    14.5    [["Equation","solve_log"]]));
    14.6  *}
    14.7 +setup {* KEStore_Elems.store_pbts
    14.8 +  [(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
    14.9 +      (["logarithmic","univariate","equation"],
   14.10 +        [("#Given",["equality e_e","solveFor v_v"]),
   14.11 +          ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
   14.12 +          ("#Find" ,["solutions v_v'i'"]),
   14.13 +          ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
   14.14 +	          "  (rhs (Subst (v'i', v_v) e_e) || < eps)"])],
   14.15 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))] *}
   14.16  ML {*
   14.17  (** methods **)
   14.18  store_met

    15.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 20 16:15:34 2014 +0100
    15.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Tue Jan 21 00:27:44 2014 +0100
    15.3 @@ -182,6 +182,18 @@
    15.4    NONE, 
    15.5    [["simplification","of_rationals","to_partial_fraction"]]));
    15.6  *}
    15.7 +setup {* KEStore_Elems.store_pbts
    15.8 +  [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
    15.9 +      (["partial_fraction", "rational", "simplification"],
   15.10 +        [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
   15.11 +          (* TODO: call this sub-problem with appropriate functionTerm: 
   15.12 +            leading coefficient of the denominator is 1: to be checked here! and..
   15.13 +            ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < 
   15.14 +               ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
   15.15 +          ("#Find"  ,["decomposedFunction p_p'''"])],
   15.16 +        append_rls "e_rls" e_rls [(*for preds in where_ TODO*)], 
   15.17 +        NONE, 
   15.18 +        [["simplification","of_rationals","to_partial_fraction"]]))] *}
   15.19  
   15.20  subsection {* Method *}
   15.21  consts

    16.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Mon Jan 20 16:15:34 2014 +0100
    16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Tue Jan 21 00:27:44 2014 +0100
    16.3 @@ -1607,6 +1607,16 @@
    16.4    SOME "Simplify t_t", 
    16.5    [["simplification","for_polynomials"]]));
    16.6  *}
    16.7 +setup {* KEStore_Elems.store_pbts
    16.8 +  [(prep_pbt thy "pbl_simp_poly" [] e_pblID
    16.9 +      (["polynomial","simplification"],
   16.10 +        [("#Given" ,["Term t_t"]),
   16.11 +          ("#Where" ,["t_t is_polyexp"]),
   16.12 +          ("#Find"  ,["normalform n_n"])],
   16.13 +        append_rls "e_rls" e_rls [(*for preds in where_*)
   16.14 +			  Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
   16.15 +        SOME "Simplify t_t", 
   16.16 +        [["simplification","for_polynomials"]]))] *}
   16.17  ML {*
   16.18  
   16.19  (** methods **)

    17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jan 20 16:15:34 2014 +0100
    17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Jan 21 00:27:44 2014 +0100
    17.3 @@ -1013,8 +1013,129 @@
    17.4    ],
    17.5    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
    17.6    [["PolyEq","complete_square"]]));
    17.7 +*}
    17.8 +setup {* KEStore_Elems.store_pbts
    17.9 +  [(prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
   17.10 +      (["polynomial","univariate","equation"],
   17.11 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   17.12 +          ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
   17.13 +	          "~((lhs e_e) is_rootTerm_in (v_v::real))",
   17.14 +	          "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
   17.15 +          ("#Find"  ,["solutions v_v'i'"])],
   17.16 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
   17.17 +    (*--- d0 ---*)
   17.18 +    (prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID
   17.19 +      (["degree_0","polynomial","univariate","equation"],
   17.20 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   17.21 +          ("#Where" ,["matches (?a = 0) e_e",
   17.22 +	          "(lhs e_e) is_poly_in v_v",
   17.23 +	          "((lhs e_e) has_degree_in v_v ) = 0"]),
   17.24 +          ("#Find"  ,["solutions v_v'i'"])],
   17.25 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])),
   17.26 +    (*--- d1 ---*)
   17.27 +    (prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID
   17.28 +      (["degree_1","polynomial","univariate","equation"],
   17.29 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   17.30 +          ("#Where" ,["matches (?a = 0) e_e",
   17.31 +	          "(lhs e_e) is_poly_in v_v",
   17.32 +	          "((lhs e_e) has_degree_in v_v ) = 1"]),
   17.33 +          ("#Find"  ,["solutions v_v'i'"])],
   17.34 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])),
   17.35 +    (*--- d2 ---*)
   17.36 +    (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
   17.37 +      (["degree_2","polynomial","univariate","equation"],
   17.38 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   17.39 +          ("#Where" ,["matches (?a = 0) e_e",
   17.40 +	          "(lhs e_e) is_poly_in v_v ",
   17.41 +	          "((lhs e_e) has_degree_in v_v ) = 2"]),
   17.42 +          ("#Find"  ,["solutions v_v'i'"])],
   17.43 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])),
   17.44 +    (prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
   17.45 +      (["sq_only","degree_2","polynomial","univariate","equation"],
   17.46 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   17.47 +          ("#Where" ,["matches ( ?a +    ?v_^^^2 = 0) e_e | " ^
   17.48 +	          "matches ( ?a + ?b*?v_^^^2 = 0) e_e | " ^
   17.49 +            "matches (         ?v_^^^2 = 0) e_e | " ^
   17.50 +            "matches (      ?b*?v_^^^2 = 0) e_e" ,
   17.51 +            "Not (matches (?a +    ?v_ +    ?v_^^^2 = 0) e_e) &" ^
   17.52 +            "Not (matches (?a + ?b*?v_ +    ?v_^^^2 = 0) e_e) &" ^
   17.53 +            "Not (matches (?a +    ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
   17.54 +            "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
   17.55 +            "Not (matches (        ?v_ +    ?v_^^^2 = 0) e_e) &" ^
   17.56 +            "Not (matches (     ?b*?v_ +    ?v_^^^2 = 0) e_e) &" ^
   17.57 +            "Not (matches (        ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
   17.58 +            "Not (matches (     ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
   17.59 +          ("#Find"  ,["solutions v_v'i'"])],
   17.60 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   17.61 +        [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),
   17.62 +    (prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
   17.63 +      (["bdv_only","degree_2","polynomial","univariate","equation"],
   17.64 +        [("#Given", ["equality e_e","solveFor v_v"]),
   17.65 +          ("#Where", ["matches (?a*?v_ +    ?v_^^^2 = 0) e_e | " ^
   17.66 +            "matches (   ?v_ +    ?v_^^^2 = 0) e_e | " ^
   17.67 +            "matches (   ?v_ + ?b*?v_^^^2 = 0) e_e | " ^
   17.68 +            "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
   17.69 +            "matches (            ?v_^^^2 = 0) e_e | " ^
   17.70 +            "matches (         ?b*?v_^^^2 = 0) e_e "]),
   17.71 +          ("#Find", ["solutions v_v'i'"])],
   17.72 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   17.73 +        [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),
   17.74 +    (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
   17.75 +      (["pqFormula","degree_2","polynomial","univariate","equation"],
   17.76 +        [("#Given", ["equality e_e","solveFor v_v"]),
   17.77 +          ("#Where", ["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
   17.78 +	          "matches (?a +   ?v_^^^2 = 0) e_e"]),
   17.79 +          ("#Find", ["solutions v_v'i'"])],
   17.80 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])),
   17.81 +    (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
   17.82 +      (["abcFormula","degree_2","polynomial","univariate","equation"],
   17.83 +        [("#Given", ["equality e_e","solveFor v_v"]),
   17.84 +          ("#Where", ["matches (?a +    ?v_^^^2 = 0) e_e | " ^
   17.85 +	          "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
   17.86 +          ("#Find", ["solutions v_v'i'"])],
   17.87 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])),
   17.88 +    (*--- d3 ---*)
   17.89 +    (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
   17.90 +      (["degree_3","polynomial","univariate","equation"],
   17.91 +        [("#Given", ["equality e_e","solveFor v_v"]),
   17.92 +          ("#Where", ["matches (?a = 0) e_e",
   17.93 +	          "(lhs e_e) is_poly_in v_v ",
   17.94 +	          "((lhs e_e) has_degree_in v_v) = 3"]),
   17.95 +          ("#Find", ["solutions v_v'i'"])],
   17.96 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])),
   17.97 +    (*--- d4 ---*)
   17.98 +    (prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID
   17.99 +      (["degree_4","polynomial","univariate","equation"],
  17.100 +        [("#Given", ["equality e_e","solveFor v_v"]),
  17.101 +          ("#Where", ["matches (?a = 0) e_e",
  17.102 +	          "(lhs e_e) is_poly_in v_v ",
  17.103 +	          "((lhs e_e) has_degree_in v_v) = 4"]),
  17.104 +          ("#Find", ["solutions v_v'i'"])],
  17.105 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),
  17.106 +    (*--- normalize ---*)
  17.107 +    (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
  17.108 +      (["normalize","polynomial","univariate","equation"],
  17.109 +        [("#Given", ["equality e_e","solveFor v_v"]),
  17.110 +          ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
  17.111 +	          "(Not(((lhs e_e) is_poly_in v_v)))"]),
  17.112 +          ("#Find", ["solutions v_v'i'"])],
  17.113 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalize_poly"]])),
  17.114 +    (*-------------------------expanded-----------------------*)
  17.115 +    (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
  17.116 +      (["expanded","univariate","equation"],
  17.117 +        [("#Given", ["equality e_e","solveFor v_v"]),
  17.118 +          ("#Where", ["matches (?a = 0) e_e",
  17.119 +	          "(lhs e_e) is_expanded_in v_v "]),
  17.120 +          ("#Find", ["solutions v_v'i'"])],
  17.121 +        PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
  17.122 +    (*--- d2 ---*)
  17.123 +    (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID
  17.124 +      (["degree_2","expanded","univariate","equation"],
  17.125 +        [("#Given", ["equality e_e","solveFor v_v"]),
  17.126 +          ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
  17.127 +          ("#Find", ["solutions v_v'i'"])],
  17.128 +         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]]))] *}
  17.129  
  17.130 -*}
  17.131  ML{*
  17.132  val scr =     
  17.133      "Script Normalize_poly (e_e::bool) (v_v::real) =                     " ^

    18.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Mon Jan 20 16:15:34 2014 +0100
    18.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Tue Jan 21 00:27:44 2014 +0100
    18.3 @@ -498,8 +498,87 @@
    18.4  		    Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")], 
    18.5    SOME "Probe e_e w_w", 
    18.6    [["probe","fuer_bruch"]]));
    18.7 +*}
    18.8 +setup {* KEStore_Elems.store_pbts
    18.9 +  [(prep_pbt thy "pbl_vereinf_poly" [] e_pblID
   18.10 +      (["polynom","vereinfachen"], [], Erls, NONE, [])),
   18.11 +    (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
   18.12 +      (["plus_minus","polynom","vereinfachen"],
   18.13 +        [("#Given", ["Term t_t"]),
   18.14 +          ("#Where", ["t_t is_polyexp",
   18.15 +            "Not (matchsub (?a + (?b + ?c)) t_t | " ^
   18.16 +            "     matchsub (?a + (?b - ?c)) t_t | " ^
   18.17 +            "     matchsub (?a - (?b + ?c)) t_t | " ^
   18.18 +            "     matchsub (?a + (?b - ?c)) t_t )",
   18.19 +            "Not (matchsub (?a * (?b + ?c)) t_t | " ^
   18.20 +            "     matchsub (?a * (?b - ?c)) t_t | " ^
   18.21 +            "     matchsub ((?b + ?c) * ?a) t_t | " ^
   18.22 +            "     matchsub ((?b - ?c) * ?a) t_t )"]),
   18.23 +          ("#Find", ["normalform n_n"])],
   18.24 +        append_rls "prls_pbl_vereinf_poly" e_rls 
   18.25 +	        [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
   18.26 +	          Calc ("Tools.matchsub", eval_matchsub ""),
   18.27 +	          Thm ("or_true", num_str @{thm or_true}),
   18.28 +            (*"(?a | True) = True"*)
   18.29 +            Thm ("or_false", num_str @{thm or_false}),
   18.30 +            (*"(?a | False) = ?a"*)
   18.31 +            Thm ("not_true",num_str @{thm not_true}),
   18.32 +            (*"(~ True) = False"*)
   18.33 +            Thm ("not_false",num_str @{thm not_false})
   18.34 +            (*"(~ False) = True"*)], 
   18.35 +       SOME "Vereinfache t_t", [["simplification","for_polynomials","with_minus"]])),
   18.36 +    (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
   18.37 +      (["klammer","polynom","vereinfachen"],
   18.38 +        [("#Given" ,["Term t_t"]),
   18.39 +          ("#Where" ,["t_t is_polyexp",
   18.40 +            "Not (matchsub (?a * (?b + ?c)) t_t | " ^
   18.41 +            "     matchsub (?a * (?b - ?c)) t_t | " ^
   18.42 +            "     matchsub ((?b + ?c) * ?a) t_t | " ^
   18.43 +            "     matchsub ((?b - ?c) * ?a) t_t )"]),
   18.44 +          ("#Find"  ,["normalform n_n"])],
   18.45 +        append_rls "prls_pbl_vereinf_poly_klammer" e_rls
   18.46 +          [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
   18.47 +	           Calc ("Tools.matchsub", eval_matchsub ""),
   18.48 +             Thm ("or_true", num_str @{thm or_true}),
   18.49 +             (*"(?a | True) = True"*)
   18.50 +             Thm ("or_false", num_str @{thm or_false}),
   18.51 +             (*"(?a | False) = ?a"*)
   18.52 +             Thm ("not_true",num_str @{thm not_true}),
   18.53 +             (*"(~ True) = False"*)
   18.54 +             Thm ("not_false",num_str @{thm not_false})
   18.55 +             (*"(~ False) = True"*)], 
   18.56 +        SOME "Vereinfache t_t", 
   18.57 +        [["simplification","for_polynomials","with_parentheses"]])),
   18.58 +    (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
   18.59 +      (["binom_klammer","polynom","vereinfachen"],
   18.60 +        [("#Given", ["Term t_t"]),
   18.61 +          ("#Where", ["t_t is_polyexp"]),
   18.62 +          ("#Find", ["normalform n_n"])],
   18.63 +        append_rls "e_rls" e_rls [(*for preds in where_*)
   18.64 +			      Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
   18.65 +        SOME "Vereinfache t_t", 
   18.66 +        [["simplification","for_polynomials","with_parentheses_mult"]])),
   18.67 +    (prep_pbt thy "pbl_probe" [] e_pblID (["probe"], [], Erls, NONE, [])),
   18.68 +    (prep_pbt thy "pbl_probe_poly" [] e_pblID
   18.69 +      (["polynom","probe"],
   18.70 +        [("#Given", ["Pruefe e_e", "mitWert w_w"]),
   18.71 +          ("#Where", ["e_e is_polyexp"]),
   18.72 +          ("#Find", ["Geprueft p_p"])],
   18.73 +        append_rls "prls_pbl_probe_poly" e_rls [(*for preds in where_*)
   18.74 +		      Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
   18.75 +        SOME "Probe e_e w_w", 
   18.76 +        [["probe","fuer_polynom"]])),
   18.77 +    (prep_pbt thy "pbl_probe_bruch" [] e_pblID
   18.78 +      (["bruch","probe"],
   18.79 +        [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
   18.80 +          ("#Where" ,["e_e is_ratpolyexp"]),
   18.81 +          ("#Find"  ,["Geprueft p_p"])],
   18.82 +        append_rls "prls_pbl_probe_bruch" e_rls [(*for preds in where_*)
   18.83 +		      Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")], 
   18.84 +        SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))] *}
   18.85  
   18.86  
   18.87 +ML {*
   18.88  (** methods **)
   18.89  
   18.90  store_met

    19.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Jan 20 16:15:34 2014 +0100
    19.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Tue Jan 21 00:27:44 2014 +0100
    19.3 @@ -7,7 +7,7 @@
    19.4               date: 02.11.28
    19.5  *)
    19.6  
    19.7 -theory RatEq imports Rational begin
    19.8 +theory RatEq imports Rational Equation begin
    19.9  
   19.10  text {* univariate equations over multivariate rational terms:
   19.11    In 2003 this type has been integrated into ISAC's equation solver
   19.12 @@ -194,6 +194,13 @@
   19.13    RatEq_prls, SOME "solve (e_e::bool, v_v)",
   19.14    [["RatEq","solve_rat_equation"]]));
   19.15  *}
   19.16 +setup {* KEStore_Elems.store_pbts
   19.17 +  [(prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
   19.18 +    (["rational","univariate","equation"],
   19.19 +      [("#Given", ["equality e_e","solveFor v_v"]),
   19.20 +        ("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),
   19.21 +        ("#Find", ["solutions v_v'i'"])],
   19.22 +      RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq","solve_rat_equation"]]))] *}
   19.23  
   19.24  ML {*
   19.25  (*-------------------------methods-----------------------*)

    20.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jan 20 16:15:34 2014 +0100
    20.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Jan 21 00:27:44 2014 +0100
    20.3 @@ -896,6 +896,14 @@
    20.4    SOME "Simplify t_t", 
    20.5    [["simplification","of_rationals"]]));
    20.6  *}
    20.7 +setup {* KEStore_Elems.store_pbts
    20.8 +  [(prep_pbt thy "pbl_simp_rat" [] e_pblID
    20.9 +      (["rational","simplification"],
   20.10 +        [("#Given" ,["Term t_t"]),
   20.11 +          ("#Where" ,["t_t is_ratpolyexp"]),
   20.12 +          ("#Find"  ,["normalform n_n"])],
   20.13 +        append_rls "e_rls" e_rls [(*for preds in where_*)], 
   20.14 +        SOME "Simplify t_t", [["simplification","of_rationals"]]))] *}
   20.15  
   20.16  section {* A methods for simplification of rationals *}
   20.17  ML {*

    21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 20 16:15:34 2014 +0100
    21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Jan 21 00:27:44 2014 +0100
    21.3 @@ -7,7 +7,7 @@
    21.4               date: 02.11.14
    21.5  *)
    21.6  
    21.7 -theory RootEq imports Root begin
    21.8 +theory RootEq imports Root Equation begin
    21.9  
   21.10  text {* univariate equations containing real square roots:
   21.11    This type of equations has been used to bootstrap Lucas-Interpretation.
   21.12 @@ -522,7 +522,37 @@
   21.13    ],
   21.14    RootEq_prls,  SOME "solve (e_e::bool, v_v)",
   21.15    [["RootEq","norm_sq_root_equation"]]));
   21.16 +*}
   21.17 +setup {* KEStore_Elems.store_pbts
   21.18 +  [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID
   21.19 +      (["root'","univariate","equation"],
   21.20 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   21.21 +          ("#Where" ,["(lhs e_e) is_rootTerm_in  (v_v::real) | " ^
   21.22 +	          "(rhs e_e) is_rootTerm_in  (v_v::real)"]),
   21.23 +          ("#Find"  ,["solutions v_v'i'"])],
   21.24 +        RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
   21.25 +    (* ---------sqrt----------- *)
   21.26 +    (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
   21.27 +      (["sq","root'","univariate","equation"],
   21.28 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   21.29 +          ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
   21.30 +            "  ((lhs e_e) is_normSqrtTerm_in (v_v::real))   )  |" ^
   21.31 +	          "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
   21.32 +            "  ((rhs e_e) is_normSqrtTerm_in (v_v::real))   )"]),
   21.33 +          ("#Find"  ,["solutions v_v'i'"])],
   21.34 +          RootEq_prls,  SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])),
   21.35 +    (* ---------normalize----------- *)
   21.36 +    (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
   21.37 +      (["normalize","root'","univariate","equation"],
   21.38 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   21.39 +          ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
   21.40 +            "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
   21.41 +	          "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
   21.42 +            "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
   21.43 +          ("#Find"  ,["solutions v_v'i'"])],
   21.44 +        RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","norm_sq_root_equation"]]))] *}
   21.45  
   21.46 +ML {*
   21.47  (*-------------------------methods-----------------------*)
   21.48  (* ---- root 20.8.02 ---*)
   21.49  store_met

    22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jan 20 16:15:34 2014 +0100
    22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Jan 21 00:27:44 2014 +0100
    22.3 @@ -133,7 +133,6 @@
    22.4  setup {* KEStore_Elems.add_rlss
    22.5    [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}
    22.6  ML {*
    22.7 -
    22.8  (*-----------------------probleme------------------------*)
    22.9  (*
   22.10  (get_pbt ["rat","root'","univariate","equation"]);
   22.11 @@ -151,6 +150,14 @@
   22.12    RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
   22.13    [["RootRatEq","elim_rootrat_equation"]]));
   22.14  *}
   22.15 +setup {* KEStore_Elems.store_pbts
   22.16 +  [(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
   22.17 +      (["rat","sq","root'","univariate","equation"],
   22.18 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   22.19 +          ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
   22.20 +	          "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
   22.21 +          ("#Find"  ,["solutions v_v'i'"])],
   22.22 +        RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]]))] *}
   22.23  ML {*
   22.24  (*-------------------------Methode-----------------------*)
   22.25  store_met

    23.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 20 16:15:34 2014 +0100
    23.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Tue Jan 21 00:27:44 2014 +0100
    23.3 @@ -48,6 +48,17 @@
    23.4    SOME "Vereinfache t_t", 
    23.5    []));
    23.6  *}
    23.7 +setup {* KEStore_Elems.store_pbts
    23.8 +  [(prep_pbt thy "pbl_simp" [] e_pblID
    23.9 +      (["simplification"],
   23.10 +        [("#Given" ,["Term t_t"]),
   23.11 +          ("#Find"  ,["normalform n_n"])],
   23.12 +        append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
   23.13 +    (prep_pbt thy "pbl_vereinfache" [] e_pblID
   23.14 +      (["vereinfachen"],
   23.15 +        [("#Given", ["Term t_t"]),
   23.16 +          ("#Find", ["normalform n_n"])],
   23.17 +        append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}
   23.18  ML {*
   23.19  @{thm mult_commute}
   23.20  *}

    24.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Jan 20 16:15:34 2014 +0100
    24.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Tue Jan 21 00:27:44 2014 +0100
    24.3 @@ -570,6 +570,38 @@
    24.4   ------ 25.8.01*)
    24.5  
    24.6  *}
    24.7 +setup {* KEStore_Elems.store_pbts
    24.8 +  [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])),
    24.9 +    (prep_pbt thy "pbl_test_equ" [] e_pblID
   24.10 +      (["equation","test"],
   24.11 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   24.12 +           ("#Where" ,["matches (?a = ?b) e_e"]),
   24.13 +           ("#Find"  ,["solutions v_v'i'"])],
   24.14 +        assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
   24.15 +    (prep_pbt thy "pbl_test_uni" [] e_pblID
   24.16 +      (["univariate","equation","test"],
   24.17 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   24.18 +           ("#Where" ,["matches (?a = ?b) e_e"]),
   24.19 +           ("#Find"  ,["solutions v_v'i'"])],
   24.20 +        assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
   24.21 +    (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
   24.22 +      (["LINEAR","univariate","equation","test"],
   24.23 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   24.24 +           ("#Where" ,["(matches (   v_v = 0) e_e) | (matches (   ?b*v_v = 0) e_e) |" ^
   24.25 +             "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)  "]),
   24.26 +           ("#Find"  ,["solutions v_v'i'"])],
   24.27 +        assoc_rls' @{theory} "matches", 
   24.28 +        SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))(*,
   24.29 +    (prep_pbt thy
   24.30 +      (["thy"],
   24.31 +        [("#Given" ,"boolTestGiven g_g"),
   24.32 +          ("#Find"  ,"boolTestFind f_f")],
   24.33 +        [])),
   24.34 +    (prep_pbt thy
   24.35 +      (["testeq","thy"],
   24.36 +        [("#Given" ,"boolTestGiven g_g"),
   24.37 +         ("#Find"  ,"boolTestFind f_f")],
   24.38 +        []))*)] *}
   24.39  ML {*
   24.40  (** methods **)
   24.41  store_met
   24.42 @@ -799,6 +831,17 @@
   24.43  *)
   24.44  
   24.45  *}
   24.46 +setup {* KEStore_Elems.store_pbts
   24.47 +  [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
   24.48 +    (["plain_square","univariate","equation","test"],
   24.49 +      [("#Given" ,["equality e_e","solveFor v_v"]),
   24.50 +        ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
   24.51 +	        "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
   24.52 +	        "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
   24.53 +	        "(matches (        v_v ^^^2 = 0) e_e)"]),
   24.54 +        ("#Find"  ,["solutions v_v'i'"])],
   24.55 +      assoc_rls' @{theory} "matches", 
   24.56 +      SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]))] *}
   24.57  ML {*
   24.58  store_pbt
   24.59   (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
   24.60 @@ -878,6 +921,54 @@
   24.61  *)
   24.62  
   24.63  *}
   24.64 +setup {* KEStore_Elems.store_pbts
   24.65 +  [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID
   24.66 +      (["polynomial","univariate","equation","test"],
   24.67 +        [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
   24.68 +          ("#Where" ,["HOL.False"]),
   24.69 +          ("#Find"  ,["solutions v_v'i'"])],
   24.70 +        e_rls, SOME "solve (e_e::bool, v_v)", [])),
   24.71 +    (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
   24.72 +      (["degree_two","polynomial","univariate","equation","test"],
   24.73 +        [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
   24.74 +          ("#Find"  ,["solutions v_v'i'"])],
   24.75 +        e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
   24.76 +    (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
   24.77 +      (["pq_formula","degree_two","polynomial","univariate","equation","test"],
   24.78 +        [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
   24.79 +          ("#Find"  ,["solutions v_v'i'"])],
   24.80 +        e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
   24.81 +    (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
   24.82 +      (["abc_formula","degree_two","polynomial","univariate","equation","test"],
   24.83 +        [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
   24.84 +          ("#Find"  ,["solutions v_v'i'"])],
   24.85 +        e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
   24.86 +    (prep_pbt thy "pbl_test_uni_root" [] e_pblID
   24.87 +      (["squareroot","univariate","equation","test"],
   24.88 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   24.89 +          ("#Where" ,["precond_rootpbl v_v"]),
   24.90 +          ("#Find"  ,["solutions v_v'i'"])],
   24.91 +        append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
   24.92 +            eval_contains_root "#contains_root_")], 
   24.93 +        SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
   24.94 +    (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
   24.95 +      (["normalize","univariate","equation","test"],
   24.96 +        [("#Given" ,["equality e_e","solveFor v_v"]),
   24.97 +          ("#Where" ,[]),
   24.98 +          ("#Find"  ,["solutions v_v'i'"])],
   24.99 +        e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
  24.100 +    (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
  24.101 +      (["sqroot-test","univariate","equation","test"],
  24.102 +        [("#Given" ,["equality e_e","solveFor v_v"]),
  24.103 +          ("#Where" ,["precond_rootpbl v_v"]),
  24.104 +          ("#Find"  ,["solutions v_v'i'"])],
  24.105 +        e_rls, SOME "solve (e_e::bool, v_v)", [])),
  24.106 +    (prep_pbt thy "pbl_test_intsimp" [] e_pblID
  24.107 +      (["inttype","test"],
  24.108 +        [("#Given" ,["intTestGiven t_t"]),
  24.109 +          ("#Where" ,[]),
  24.110 +          ("#Find"  ,["intTestFind s_s"])],
  24.111 +      e_rls, NONE, [["Test","intsimp"]]))] *}
  24.112  
  24.113  ML {*
  24.114  store_met

    25.1 --- a/src/Tools/isac/calcelems.sml	Mon Jan 20 16:15:34 2014 +0100
    25.2 +++ b/src/Tools/isac/calcelems.sml	Tue Jan 21 00:27:44 2014 +0100
    25.3 @@ -800,6 +800,34 @@
    25.4  type ptyps = (pbt ptyp) list
    25.5  val ptyps = Unsynchronized.ref ([e_Ptyp] : ptyps);
    25.6  
    25.7 +
    25.8 +fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]
    25.9 +  | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
   25.10 +((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)
   25.11 +     if k=k'
   25.12 +     then ((Ptyp (k', [pbt], ps))::pys)
   25.13 +     else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
   25.14 +	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
   25.15 +)			 
   25.16 +  | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
   25.17 +((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)
   25.18 +     if k=k'
   25.19 +     then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
   25.20 +     else 
   25.21 +	 if length pys = 0
   25.22 +	 then error ("insert: not found "^(strs2str (d:pblID)))
   25.23 +	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
   25.24 +);
   25.25 +
   25.26 +(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
   25.27 +  function for trees / ptyps *)
   25.28 +fun merge_ptyps ([], pt) = pt
   25.29 +  | merge_ptyps (pt, []) = pt
   25.30 +  | merge_ptyps ((Ptyp (k, x, ps)::xs), (ys' as Ptyp (k', y, ps')::ys)) =
   25.31 +      if k = k' then
   25.32 +        (Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)) else
   25.33 +        (Ptyp (k, x, ps) :: merge_ptyps (xs, ys'));
   25.34 +
   25.35  (* types for methods *)
   25.36  
   25.37