wneuper/isa: src/Tools/isac/Knowledge/DiffApp.thy@7497ff20f1e8

     1 (* application of differential calculus

     2    Walther Neuper 2002

     3    (c) due to copyright terms

     4 *)

     6 theory DiffApp imports Diff begin

     8 consts

    10   Maximum'_value

    11              :: "[bool list,real,bool list,real,real set,bool,

    12 		    bool list] => bool list"

    13                ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)

    15   Make'_fun'_by'_new'_variable

    16              :: "[real,real,bool list,

    17 		    bool] => bool"

    18                ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))//

    19 		   (_))" 9)

    20   Make'_fun'_by'_explicit

    21              :: "[real,real,bool list,

    22 		    bool] => bool"

    23                ("((Script Make'_fun'_by'_explicit (_ _ _ =))//

    24 		   (_))" 9)

    26   dummy :: real

    28 (*for script Maximum_value*)

    29   filterVar :: "[real, 'a list] => 'a list"

    31 (*primrec*)axiomatization where

    32   filterVar_Nil:		"filterVar v []     = []" and

    33   filterVar_Const:	"filterVar v (x#xs) =

    34 			 (if (v : set (Vars x)) then x#(filterVar v xs)

    35 			                    else filterVar v xs)   "

    36 text {*WN.6.5.03: old decisions in this file partially are being changed

    37   in a quick-and-dirty way to make scripts run: Maximum_value,

    38   Make_fun_by_new_variable, Make_fun_by_explicit.

    39 found to be reconsidered:

    40 - descriptions (Descript.thy)

    41 - penv: really need term list; or just rerun the whole example with num/var

    42 - mk_arg, itms2args ... env in script different from penv ?

    43 - L = SubProblem eq ... show some vars on the worksheet ? (other means for

    44   referencing are labels (no on worksheet))

    46 WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env

    47   from penv as is.

    48 *}

    50 ML {*

    51 val thy = @{theory};

    53 val eval_rls = prep_rls(

    54   Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),

    55       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

    56       rules = [Thm ("refl",num_str @{thm refl}),

    57 		Thm ("real_le_refl",num_str @{thm real_le_refl}),

    58 		Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),

    59 		Thm ("not_true",num_str @{thm not_true}),

    60 		Thm ("not_false",num_str @{thm not_false}),

    61 		Thm ("and_true",num_str @{thm and_true}),

    62 		Thm ("and_false",num_str @{thm and_false}),

    63 		Thm ("or_true",num_str @{thm or_true}),

    64 		Thm ("or_false",num_str @{thm or_false}),

    65 		Thm ("and_commute",num_str @{thm and_commute}),

    66 		Thm ("or_commute",num_str @{thm or_commute}),

    68 		Calc ("Orderings.ord_class.less",eval_equ "#less_"),

    69 		Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

    71 		Calc ("Atools.ident",eval_ident "#ident_"),

    72 		Calc ("Atools.is'_const",eval_const "#is_const_"),

    73 		Calc ("Atools.occurs'_in",eval_occurs_in ""),

    74 		Calc ("Tools.matches",eval_matches "")

    75 	       ],

    76       scr = Script ((term_of o the o (parse thy))

    77       "empty_script")

    78       }:rls);

    79 ruleset' := overwritelthy @{theory}

    80 		(!ruleset',

    81 		 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)

    82 		  ]);

    83 *}

    84 ML{*

    86 (** problem types **)

    88 store_pbt

    89  (prep_pbt thy "pbl_fun_max" [] e_pblID

    90  (["maximum_of","function"],

    91   [("#Given" ,["fixedValues f_ix"]),

    92    ("#Find"  ,["maximum m_m","valuesFor v_s"]),

    93    ("#Relate",["relations r_s"])

    94   ],

    95   e_rls, NONE, []));

    97 store_pbt

    98  (prep_pbt thy "pbl_fun_make" [] e_pblID

    99  (["make","function"]:pblID,

   100   [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   101    ("#Find"  ,["functionEq f_1"])

   102   ],

   103   e_rls, NONE, []));

   104 store_pbt

   105  (prep_pbt thy "pbl_fun_max_expl" [] e_pblID

   106  (["by_explicit","make","function"]:pblID,

   107   [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   108    ("#Find"  ,["functionEq f_1"])

   109   ],

   110   e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));

   111 store_pbt

   112  (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID

   113  (["by_new_variable","make","function"]:pblID,

   114   [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   115    (*WN.12.5.03: precond for distinction still missing*)

   116    ("#Find"  ,["functionEq f_1"])

   117   ],

   118   e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));

   120 store_pbt

   121  (prep_pbt thy "pbl_fun_max_interv" [] e_pblID

   122  (["on_interval","maximum_of","function"]:pblID,

   123   [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),

   124    (*WN.12.5.03: precond for distinction still missing*)

   125    ("#Find"  ,["maxArgument v_0"])

   126   ],

   127   e_rls, NONE, []));

   129 store_pbt

   130  (prep_pbt thy "pbl_tool" [] e_pblID

   131  (["tool"]:pblID,

   132   [],

   133   e_rls, NONE, []));

   135 store_pbt

   136  (prep_pbt thy "pbl_tool_findvals" [] e_pblID

   137  (["find_values","tool"]:pblID,

   138   [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),

   139    ("#Find"  ,["valuesFor v_ls"]),

   140    ("#Relate",["additionalRels r_s"])

   141   ],

   142   e_rls, NONE, []));

   144 *}

   145 ML{*

   147 (** methods, scripts not yet implemented **)

   149 store_met

   150  (prep_met thy "met_diffapp" [] e_metID

   151  (["DiffApp"],

   152    [],

   153    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

   154     crls = Atools_erls, nrls=norm_Rational

   155     (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));

   156 *}

   157 ML{*

   158 store_met

   159  (prep_met thy "met_diffapp_max" [] e_metID

   160  (["DiffApp","max_by_calculus"]:metID,

   161   [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s",

   162 	       "boundVariable v_v","interval i_tv","errorBound e_rr"]),

   163     ("#Find"  ,["valuesFor v_s"]),

   164     ("#Relate",[])

   165     ],

   166   {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,

   167     crls = eval_rls, nrls=norm_Rational

   168    (*,  asm_rls=[],asm_thm=[]*)},

   169   "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)       " ^

   170   "      (v_v::real) (itv_v::real set) (e_rr::bool) =                       " ^

   171   " (let e_e = (hd o (filterVar m_m)) r_s;                                  " ^

   172   "      t_t = (if 1 < LENGTH r_s                                         " ^

   173   "           then (SubProblem (DiffApp',[make,function],[no_met])        " ^

   174   "                     [REAL m_m, REAL v_v, BOOL_LIST r_s])             " ^

   175   "           else (hd r_s));                                             " ^

   176   "      (m_x::real) =                                                    " ^

   177   "SubProblem(DiffApp',[on_interval,maximum_of,function],                 " ^

   178   "                                [DiffApp,max_on_interval_by_calculus]) " ^

   179   "                               [BOOL t_t, REAL v_v, REAL_SET i_tv]    " ^

   180   " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values])      " ^

   181   "      [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m,                  " ^

   182   "       BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))            "

   183  ));

   184 *}

   185 ML{*

   186 store_met

   187  (prep_met thy "met_diffapp_funnew" [] e_metID

   188  (["DiffApp","make_fun_by_new_variable"]:metID,

   189    [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   190     ("#Find"  ,["functionEq f_1"])

   191     ],

   192    {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,

   193     calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},

   194   "Script Make_fun_by_new_variable (f_f::real) (v_v::real)                " ^

   195   "      (eqs::bool list) =                                            " ^

   196   "(let h_h = (hd o (filterVar f_f)) eqs;                                " ^

   197   "     e_s = dropWhile (ident h_h) eqs;                                " ^

   198   "     v_s = dropWhile (ident f_f) (Vars h_h);                           " ^

   199   "     v_1 = NTH 1 v_s;                                               " ^

   200   "     v_2 = NTH 2 v_s;                                               " ^

   201   "     e_1 = (hd o (filterVar v_1)) e_s;                               " ^

   202   "     e_2 = (hd o (filterVar v_2)) e_s;                               " ^

   203   "  (s_1::bool list) =                                                 " ^

   204   "                (SubProblem (DiffApp',[univariate,equation],[no_met])" ^

   205   "                    [BOOL e_1, REAL v_1]);                         " ^

   206   "  (s_2::bool list) =                                                 " ^

   207   "                (SubProblem (DiffApp',[univariate,equation],[no_met])" ^

   208   "                    [BOOL e_2, REAL v_2])" ^

   209   "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"

   210 ));

   211 *}

   212 ML{*

   213 store_met

   214 (prep_met thy "met_diffapp_funexp" [] e_metID

   215 (["DiffApp","make_fun_by_explicit"]:metID,

   216    [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),

   217     ("#Find"  ,["functionEq f_1"])

   218     ],

   219    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,

   220     crls = eval_rls, nrls=norm_Rational

   221     (*, asm_rls=[],asm_thm=[]*)},

   222    "Script Make_fun_by_explicit (f_f::real) (v_v::real)                 " ^

   223    "      (eqs::bool list) =                                         " ^

   224    " (let h_h = (hd o (filterVar f_f)) eqs;                            " ^

   225    "      e_1 = hd (dropWhile (ident h_h) eqs);                       " ^

   226    "      v_s = dropWhile (ident f_f) (Vars h_h);                       " ^

   227    "      v_1 = hd (dropWhile (ident v_v) v_s);                        " ^

   228    "      (s_1::bool list)=                                           " ^

   229    "              (SubProblem(DiffApp',[univariate,equation],[no_met])" ^

   230    "                          [BOOL e_1, REAL v_1])                 " ^

   231    " in Substitute [(v_1 = (rhs o hd) s_1)] h_h)                       "

   232    ));

   233 *}

   234 ML{*

   235 store_met

   236  (prep_met thy "met_diffapp_max_oninterval" [] e_metID

   237  (["DiffApp","max_on_interval_by_calculus"]:metID,

   238    [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*,

   239 		"errorBound e_rr"*)]),

   240     ("#Find"  ,["maxArgument v_0"])

   241     ],

   242    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,

   243     crls = eval_rls, nrls=norm_Rational

   244     (*, asm_rls=[],asm_thm=[]*)},

   245    "empty_script"

   246    ));

   247 *}

   248 ML{*

   249 store_met

   250  (prep_met thy "met_diffapp_findvals" [] e_metID

   251  (["DiffApp","find_values"]:metID,

   252    [],

   253    {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,

   254     crls = eval_rls, nrls=norm_Rational(*,

   255     asm_rls=[],asm_thm=[]*)},

   256    "empty_script"));

   258 val list_rls = append_rls "list_rls" list_rls

   259 			  [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),

   260 			   Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})

   261 			   ];

   262 ruleset' := overwritelthy @{theory} (!ruleset',

   263   [("list_rls",list_rls)

   264    ]);

   265 *}

   267 end

author	Thomas Leh <t.leh@gmx.at>
	Tue, 26 Jul 2011 13:27:59 +0200
branch	decompose-isar
changeset 42197	7497ff20f1e8
parent 41905	b772eb34c16c
child 42211	51c3c007d7fd
permissions	-rw-r--r--