src/Tools/isac/Knowledge/DiffApp-oldscr.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:20:07 +0200
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37906 src/Tools/isac/IsacKnowledge/DiffApp-oldscr.sml@e2b23ba9df13
child 37981 b2877b9d455a
permissions -rw-r--r--
renamed isac's directories and Build_Isac.thy

Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge
neuper@37906
     1
(*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
neuper@37906
     2
neuper@37906
     3
(* Das erste Script aus dem Maximum-Beispiel.
neuper@37906
     4
   parse erzeugt aus dem string 's' den 
neuper@37906
     5
  'cterm 's' im Isabelle-Format (pretty-printing !)*)
neuper@37906
     6
neuper@37906
     7
ML> ...
neuper@37906
     8
ML> val c = (the o (parse thy)) s; 
neuper@37906
     9
val c =
neuper@37906
    10
  "Script1 Maximum_value fix_ m_ rs_ v_ itv_ err_ =
neuper@37906
    11
    let e_ = (hd o filter (Testvar m_)) rs_;
neuper@37906
    12
        t_ =
neuper@37906
    13
          if #1 < Length rs_
neuper@37906
    14
          then make_fun (R, [make, function], no_met) m_ v_ rs_
neuper@37906
    15
          else (Lhs o hd) rs_;
neuper@37906
    16
        mx_ =
neuper@37906
    17
          max_on_interval (R, [on_interval, max_of, function],
neuper@37906
    18
                           maximum_on_interval) t_ v_ itv_
neuper@37906
    19
    in find_vals (R, [find_values, tool], find_values)
neuper@37906
    20
       mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
neuper@37906
    21
neuper@37906
    22
ML> set show_types;
neuper@37906
    23
ML> c;
neuper@37906
    24
val c =
neuper@37906
    25
  "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_::real itv_::real set err_::bool =
neuper@37906
    26
    let e_::bool = (hd o filter (Testvar m_)) rs_;
neuper@37906
    27
        t_::real =
neuper@37906
    28
          if (#1::real) < Length rs_
neuper@37906
    29
          then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_ rs_
neuper@37906
    30
          else (Lhs o hd) rs_;
neuper@37906
    31
        mx_::real =
neuper@37906
    32
          max_on_interval (R, [on_interval::ID, max_of::ID, function],
neuper@37906
    33
                           maximum_on_interval::ID) t_ v_ itv_
neuper@37906
    34
    in find_vals (R, [find_values::ID, tool::ID], find_values)
neuper@37906
    35
       mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
neuper@37906
    36
neuper@37906
    37
neuper@37906
    38
neuper@37906
    39
(* Die ersten 3 Scripts aus dem Maximum-Beispiel.
neuper@37906
    40
   parse erzeugt aus dem string 's' den 
neuper@37906
    41
  'cterm 's' im Isabelle-Format (pretty-printing !)*)
neuper@37906
    42
neuper@37906
    43
ML> ...
neuper@37906
    44
ML> val c = (the o (parse thy)) s; 
neuper@37906
    45
val c =
neuper@37906
    46
  "Script maximum =
neuper@37906
    47
    Input [Bool fix_, Real m_, BoolList rs_, Real v_, RealSet itv_, Bool err_]
neuper@37906
    48
    Local [Bool e_, Real t_, Real mx_, RealList vs_]
neuper@37906
    49
    Tacs [SEQU
neuper@37906
    50
           [let e_ = (hd o filter (Testvar m_)) rs_
neuper@37906
    51
            in if #1 < Length rs_
neuper@37906
    52
               then Subproblem Spec (R, [make, function], no_met)
neuper@37906
    53
                     InOut [In m_, In v_, In rs_, Out t_]
neuper@37906
    54
               else t_ := (Lhs o hd) rs_ ;
neuper@37906
    55
            Subproblem Spec (R, [on_interval, max_of, function],
neuper@37906
    56
                             maximum_on_interval)
neuper@37906
    57
             InOut [In t_, In v_, In itv_, In err_, Out mx_] ;
neuper@37906
    58
            Subproblem Spec (R, [find_values, tool], find_values)
neuper@37906
    59
             InOut [In mx_, In t_, In v_, In m_, In (dropWhile (op = e_) rs_),
neuper@37906
    60
                    Out vs_]]]
neuper@37906
    61
    Return []" : cterm
neuper@37906
    62
neuper@37906
    63
ML> ...
neuper@37906
    64
ML> val c = (the o (parse thy)) s; 
neuper@37906
    65
val c =
neuper@37906
    66
  "Script make_fun_by_new_variable =
neuper@37906
    67
    Input [Real f_, Real v_, BoolList eqs_]
neuper@37906
    68
    Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
neuper@37906
    69
           Bool e2_, BoolList s_1, BoolList s_2]
neuper@37906
    70
    Tacs [SEQU
neuper@37906
    71
           [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];
neuper@37906
    72
                vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
neuper@37906
    73
                e1_ = (hd o filter (Testvar v1_)) es_;
neuper@37906
    74
                e2_ = (hd o filter (Testvar v2_)) es_
neuper@37906
    75
            in Subproblem Spec (R, [univar, equation], no_met)
neuper@37906
    76
                InOut [In e1_, In v1_, Out s_1] ;
neuper@37906
    77
               Subproblem Spec (R, [univar, equation], no_met)
neuper@37906
    78
                InOut [In e2_, In v2_, Out s_2]],
neuper@37906
    79
          Take (Bool h_) ;
neuper@37906
    80
          Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
neuper@37906
    81
    Return [Currform]" : cterm
neuper@37906
    82
neuper@37906
    83
ML> ...
neuper@37906
    84
ML> val c = (the o (parse thy)) s; 
neuper@37906
    85
val c =
neuper@37906
    86
  "Script make_fun_explicit =
neuper@37906
    87
    Input [Real f_, Real v_, BoolList eqs_]
neuper@37906
    88
    Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
neuper@37906
    89
    Tacs [SEQU
neuper@37906
    90
           [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);
neuper@37906
    91
                vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
neuper@37906
    92
            in Subproblem Spec (R, [univar, equation], no_met)
neuper@37906
    93
                InOut [In eq_, In v1_, Out ss_]],
neuper@37906
    94
          Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
neuper@37906
    95
    Return [Currform]" : cterm
neuper@37906
    96
ML>