1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/DiffApp.ML Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,181 @@
1.4 +(* tools for applications of differetiation
1.5 + use"DiffApp.ML";
1.6 + use"knowledge/DiffApp.ML";
1.7 + use"../knowledge/DiffApp.ML";
1.8 + *)
1.9 +
1.10 +
1.11 +(** interface isabelle -- isac **)
1.12 +
1.13 +theory' := overwritel (!theory', [("DiffApp.thy",DiffApp.thy)]);
1.14 +
1.15 +val eval_rls =
1.16 + Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
1.17 + erls = e_rls, srls = Erls, calc = [], asm_thm = [],
1.18 + rules = [Thm ("refl",num_str refl),
1.19 + Thm ("le_refl",num_str le_refl),
1.20 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.21 + Thm ("not_true",num_str not_true),
1.22 + Thm ("not_false",num_str not_false),
1.23 + Thm ("and_true",and_true),
1.24 + Thm ("and_false",and_false),
1.25 + Thm ("or_true",or_true),
1.26 + Thm ("or_false",or_false),
1.27 + Thm ("and_commute",num_str and_commute),
1.28 + Thm ("or_commute",num_str or_commute),
1.29 +
1.30 + Calc ("op <",eval_equ "#less_"),
1.31 + Calc ("op <=",eval_equ "#less_equal_"),
1.32 +
1.33 + Calc ("Atools.ident",eval_ident "#ident_"),
1.34 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.35 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.36 + Calc ("Tools.matches",eval_matches "")
1.37 + ],
1.38 + scr = Script ((term_of o the o (parse thy))
1.39 + "empty_script")
1.40 + }:rls;
1.41 +ruleset' := overwritel
1.42 + (!ruleset',
1.43 + [("eval_rls",atools_erls)(*FIXXXME:del with rls.rls'*)
1.44 + ]);
1.45 +
1.46 +
1.47 +(** problem types **)
1.48 +
1.49 +store_pbt
1.50 + (prep_pbt DiffApp.thy
1.51 + (["maximum_of","function"],
1.52 + [("#Given" ,["fixedValues fix_"]),
1.53 + ("#Find" ,["maximum m_","valuesFor vs_"]),
1.54 + ("#Relate",["relations rs_"])
1.55 + ],
1.56 + e_rls, None, []));
1.57 +
1.58 +store_pbt
1.59 + (prep_pbt DiffApp.thy
1.60 + (["make","function"]:pblID,
1.61 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.62 + ("#Find" ,["functionTerm f_1_"])
1.63 + ],
1.64 + e_rls, None, []));
1.65 +
1.66 +store_pbt
1.67 + (prep_pbt DiffApp.thy
1.68 + (["on_interval","maximum_of","function"]:pblID,
1.69 + [("#Given" ,["functionTerm t_","boundVariable v_","interval itv_"]),
1.70 + ("#Find" ,["maxArgument v_0_"])
1.71 + ],
1.72 + e_rls, None, []));
1.73 +
1.74 +store_pbt
1.75 + (prep_pbt DiffApp.thy
1.76 + (["tool"]:pblID,
1.77 + [],
1.78 + e_rls, None, []));
1.79 +
1.80 +store_pbt
1.81 + (prep_pbt DiffApp.thy
1.82 + (["find_values","tool"]:pblID,
1.83 + [("#Given" ,["maxArgument ma_","functionTerm f_","boundVariable v_"]),
1.84 + ("#Find" ,["valuesFor vls_"]),
1.85 + ("#Relate",["additionalRels rs_"])
1.86 + ],
1.87 + e_rls, None, []));
1.88 +
1.89 +
1.90 +(** methods, scripts not yet implemented **)
1.91 +
1.92 +methods:= overwritel (!methods,
1.93 +[
1.94 + prep_met
1.95 + (("DiffApp.thy","max_by_calculus"):metID,
1.96 + [("#Given" ,["fixedValues fix_","boundVariable v_","interval itv_",
1.97 + "errorBound err_"]),
1.98 + ("#Find" ,["maximum m_","valuesFor vs_"]),
1.99 + ("#Relate",["relations rs_"])
1.100 + ],
1.101 + {rew_ord'="tless_true",rls'=eval_rls,calc=[], srls = e_rls,prls=e_rls,
1.102 + asm_rls=[],asm_thm=[]},
1.103 +(*---- see test-script.sml
1.104 + "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.105 + \ (v_::real) (itv_::real set) (err_::bool) = \
1.106 + \ (let e_ = (hd o (filter (Testvar m_))) rs_; \
1.107 + \ t_ = (if 1 < Length rs_ \
1.108 + \ then (SubProblem (Reals_,[make,function],(Isac_,no_met))\
1.109 + \ [real_ m_, real_ v_, bool_list_ rs_])\
1.110 + \ else (hd rs_)); \
1.111 + \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
1.112 + \ (Isac_,maximum_on_interval))\
1.113 + \ [bool_ t_, real_ v_, real_set_ itv_]\
1.114 + \ in ((SubProblem (Reals_,[find_values,tool],(Isac_,find_values)) \
1.115 + \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.116 + \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))"*)
1.117 + "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.118 + \ (v_::real) (itv_::real set) (err_::bool) = \
1.119 + \ (let (t_::bool) = ((SubProblem (Reals_,[make,function],(Isac_,no_met)) \
1.120 + \ [real_ m_, real_ v_, bool_list_ rs_])::bool)\
1.121 + \ in (rs_ ::bool list))"
1.122 + )
1.123 +,
1.124 + prep_met
1.125 + (("DiffApp.thy","make_fun_by_new_variable"):metID,
1.126 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.127 + ("#Find" ,["functionTerm f_1_"])
1.128 + ],
1.129 + {rew_ord'="tless_true",rls'=eval_rls,srls = list_rls,prls=e_rls,
1.130 + calc=[],asm_rls=[],asm_thm=[]},
1.131 + "Script Make_fun_by_new_variable (f_::real) (v_::real) \
1.132 + \ (eqs_::bool list) = \
1.133 + \(let h_ = (hd o (filter (Testvar m_))) eqs_; \
1.134 + \ es_ = dropWhile (ident h_) eqs_; \
1.135 + \ vs_ = dropWhile (ident f_) (Var h_); \
1.136 + \ v1_ = Nth 1 vs_; \
1.137 + \ v2_ = Nth 2 vs_; \
1.138 + \ e1_ = (hd o (filter (Testvar v1_))) es_; \
1.139 + \ e2_ = (hd o (filter (Testvar v2_))) es_; \
1.140 + \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],(Isac_,no_met))\
1.141 + \ [bool_ e1_, real_ v1_]);\
1.142 + \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],(Isac_,no_met))\
1.143 + \ [bool_ e2_, real_ v2_])\
1.144 + \in Substitute [(v_1, (Rhs o hd) s_1),(v_2, (Rhs o hd) s_2)] h_)"
1.145 +)
1.146 +,
1.147 + prep_met
1.148 +(("DiffApp.thy","make_fun_by_explicit"):metID,
1.149 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.150 + ("#Find" ,["functionTerm f_1_"])
1.151 + ],
1.152 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
1.153 + asm_rls=[],asm_thm=[]},
1.154 + "Script Make_fun_by_explicit (f_::real) (v_::real) \
1.155 + \ (eqs_::bool list) = \
1.156 + \ (let h_ = (hd o (filter (Testvar m_))) eqs_; \
1.157 + \ e1_ = hd (dropWhile (ident h_) eqs_); \
1.158 + \ vs_ = dropWhile (ident f_) (Var h_); \
1.159 + \ v1_ = hd (dropWhile (ident v_) vs_); \
1.160 + \ (s1::bool list)=(SubProblem(Reals_,[univar,equation],(Isac_,no_met))\
1.161 + \ [bool_ e1_, real_ v1_])\
1.162 + \ in Substitute [(v_1, (Rhs o hd) s_1)] h_)"
1.163 + )
1.164 +,
1.165 + prep_met
1.166 + (("DiffApp.thy","max_on_interval_by_calculus"):metID,
1.167 + [("#Given" ,["functionTerm t_","boundVariable v_","interval itv_",
1.168 + "errorBound err_"]),
1.169 + ("#Find" ,["maxArgument v_0_"])
1.170 + ],
1.171 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
1.172 + asm_rls=[],asm_thm=[]},
1.173 + "Undef"
1.174 + )
1.175 +,
1.176 + prep_met
1.177 + (("DiffApp.thy","find_values"):metID,
1.178 + [],
1.179 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
1.180 + asm_rls=[],asm_thm=[]},
1.181 + "Undef")
1.182 +]);
1.183 +
1.184 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/DiffApp.sml Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,105 @@
2.4 +(* = DiffAppl.ML
2.5 + +++ outcommented tests
2.6 +*)
2.7 +
2.8 +
2.9 +theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);
2.10 +
2.11 +(*
2.12 +> get_pbt ["DiffAppl.thy","maximum_of","function"];
2.13 +> get_met ("Script.thy","max_on_interval_by_calculus");
2.14 +> !pbltypes;
2.15 + *)
2.16 +pbltypes:= overwritel (!pbltypes,
2.17 +[
2.18 + prep_pbt DiffAppl.thy
2.19 + (["DiffAppl.thy","maximum_of","function"],
2.20 + [("#Given" ,"fixedValues fix_"),
2.21 + ("#Find" ,"maximum m_"),
2.22 + ("#Find" ,"valuesFor vs_"),
2.23 + ("#Relate","relations rs_") (*,
2.24 + ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
2.25 + ("#with" ,"Ex_frees ((foldl (op &) True rs_) & \
2.26 + \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
2.27 + \ --> m' <= m_)))") *)
2.28 + ]),
2.29 +
2.30 + prep_pbt DiffAppl.thy
2.31 + (["DiffAppl.thy","make","function"]:pblID,
2.32 + [("#Given" ,"functionOf f_"),
2.33 + ("#Given" ,"boundVariable v_"),
2.34 + ("#Given" ,"equalities eqs_"),
2.35 + ("#Find" ,"functionTerm f_0_")
2.36 + ]),
2.37 +
2.38 + prep_pbt DiffAppl.thy
2.39 + (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,
2.40 + [("#Given" ,"functionTerm t_"),
2.41 + ("#Given" ,"boundVariable v_"),
2.42 + ("#Given" ,"interval itv_"),
2.43 + ("#Find" ,"maxArgument v_0_")
2.44 + ]),
2.45 +
2.46 + prep_pbt DiffAppl.thy
2.47 + (["DiffAppl.thy","find_values","tool"]:pblID,
2.48 + [("#Given" ,"maxArgument ma_"),
2.49 + ("#Given" ,"functionTerm f_"),
2.50 + ("#Given" ,"boundVariable v_"),
2.51 + ("#Find" ,"valuesFor vls_"),
2.52 + ("#Relate","additionalRels rs_")
2.53 + ])
2.54 +]);
2.55 +
2.56 +
2.57 +methods:= overwritel (!methods,
2.58 +[
2.59 + (("DiffAppl.thy","max_by_calculus"):metID,
2.60 + {ppc = prep_met DiffAppl.thy
2.61 + [("#Given" ,"fixedValues fix_"),
2.62 + ("#Given" ,"boundVariable v_"),
2.63 + ("#Given" ,"interval itv_"),
2.64 + ("#Given" ,"errorBound err_"),
2.65 + ("#Find" ,"maximum m_"),
2.66 + ("#Find" ,"valuesFor vs_"),
2.67 + ("#Relate","relations rs_")
2.68 + ],
2.69 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
2.70 + scr=EmptyScr} : meth'),
2.71 +
2.72 + (("DiffAppl.thy","make_fun_by_new_variable"):metID,
2.73 + {ppc = prep_met DiffAppl.thy
2.74 + [("#Given" ,"functionOf f_"),
2.75 + ("#Given" ,"boundVariable v_"),
2.76 + ("#Given" ,"equalities eqs_"),
2.77 + ("#Find" ,"functionTerm f_0_")
2.78 + ],
2.79 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
2.80 + scr=EmptyScr} : meth'),
2.81 +
2.82 + (("DiffAppl.thy","make_fun_by_explicit"):metID,
2.83 + {ppc = prep_met DiffAppl.thy
2.84 + [("#Given" ,"functionOf f_"),
2.85 + ("#Given" ,"boundVariable v_"),
2.86 + ("#Given" ,"equalities eqs_"),
2.87 + ("#Find" ,"functionTerm f_0_")
2.88 + ],
2.89 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
2.90 + scr=EmptyScr} : meth'),
2.91 +
2.92 + (("DiffAppl.thy","max_on_interval_by_calculus"):metID,
2.93 + {ppc = prep_met DiffAppl.thy
2.94 + [("#Given" ,"functionTerm t_"),
2.95 + ("#Given" ,"boundVariable v_"),
2.96 + ("#Given" ,"interval itv_"),
2.97 + ("#Given" ,"errorBound err_"),
2.98 + ("#Find" ,"maxArgument v_0_")
2.99 + ],
2.100 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
2.101 + scr=EmptyScr} : meth'),
2.102 +
2.103 + (("DiffAppl.thy","find_values"):metID,
2.104 + {ppc = prep_met DiffAppl.thy
2.105 + [],
2.106 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
2.107 + scr=EmptyScr} : meth')
2.108 +]);
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/IsacKnowledge/DiffApp.thy Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,29 @@
3.4 +(* application of differential calculus
3.5 + WN.3.01
3.6 + todo
3.7 + *)
3.8 +
3.9 +
3.10 +DiffApp = Diff +
3.11 +
3.12 +consts
3.13 +
3.14 + Maximum'_value
3.15 + :: "[bool list,real,bool list,real,real set,bool,\
3.16 + \ bool list] => bool list"
3.17 + ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
3.18 +
3.19 + Make'_fun'_by'_new'_variable
3.20 + :: "[real,real,bool list, \
3.21 + \ bool] => bool"
3.22 + ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// \
3.23 + \(_))" 9)
3.24 + Make'_fun'_by'_explicit
3.25 + :: "[real,real,bool list, \
3.26 + \ bool] => bool"
3.27 + ("((Script Make'_fun'_by'_explicit (_ _ _ =))// \
3.28 + \(_))" 9)
3.29 +
3.30 + dummy :: real
3.31 +
3.32 +end
3.33 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/IsacKnowledge/Equation.ML Thu Apr 17 18:01:03 2003 +0200
4.3 @@ -0,0 +1,34 @@
4.4 +(* (c) by Richard Lang
4.5 + defines equation and univariate-equation
4.6 + created by: rlang
4.7 + date: 02.09
4.8 + changed by: rlang
4.9 + last change by: rlang
4.10 + date: 02.11.29
4.11 +*)
4.12 +
4.13 +(* use"knowledge/Equation.ML";
4.14 + use"Equation.ML";
4.15 + *)
4.16 +
4.17 +theory' := overwritel (!theory', [("Equation.thy",Equation.thy)]);
4.18 +
4.19 +store_pbt
4.20 + (prep_pbt Equation.thy
4.21 + (["equation"],
4.22 + [("#Given" ,["equality e_","solveFor v_"]),
4.23 + ("#Where" ,["matches (?a = ?b) e_"]),
4.24 + ("#Find" ,["solutions v_i_"])
4.25 + ],
4.26 + append_rls "equation_prls" e_rls
4.27 + [Calc ("Tools.matches",eval_matches "")],None,[]));
4.28 +store_pbt
4.29 + (prep_pbt Equation.thy
4.30 + (["univariate","equation"],
4.31 + [("#Given" ,["equality e_","solveFor v_"]),
4.32 + ("#Where" ,["matches (?a = ?b) e_"]),
4.33 + ("#Find" ,["solutions v_i_"])
4.34 + ],
4.35 + append_rls "univariate_equation_prls" e_rls
4.36 + [Calc ("Tools.matches",eval_matches "")],None,[]));
4.37 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/IsacKnowledge/Equation.thy Thu Apr 17 18:01:03 2003 +0200
5.3 @@ -0,0 +1,4 @@
5.4 +
5.5 +Equation = Atools +
5.6 +
5.7 +end
5.8 \ No newline at end of file
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/sml/IsacKnowledge/Float.ML Thu Apr 17 18:01:03 2003 +0200
6.3 @@ -0,0 +1,124 @@
6.4 +(* use"Float.ML";
6.5 + *)
6.6 +
6.7 +(*WN.28.3.03 fuer Matthias*)
6.8 +(*Floatingpointnumbers, direkte Darstellung der abstrakten Syntax:*)
6.9 + val t = (term_of o the o (parse thy)) "Float ((1,2),(0,0))";
6.10 + atomt t;
6.11 + val t = (term_of o the o (parse thy))
6.12 + "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * \
6.13 + \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
6.14 + atomt t;
6.15 +(*die konkrete Syntax wird noch verschoenert*)
6.16 +
6.17 +(*--- 15.4.03
6.18 +fun calc "op +" (n1, n2) = n1+n2
6.19 + | calc "op -" (n1, n2) = n1-n2
6.20 + | calc "op *" (n1, n2) = n1*n2
6.21 + | calc "HOL.divide"(n1, n2) = n1 div n2
6.22 + | calc "Atools.pow"(n1, n2) = power n1 n2
6.23 + | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");
6.24 +---*)
6.25 +(*.used for calculating built in binary operations in Isabelle2002.
6.26 + integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
6.27 +fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int) =
6.28 + if b < d
6.29 + then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
6.30 + else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
6.31 + | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
6.32 + ((a - c,0),(0,0))
6.33 + | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
6.34 + ((a * c, b + d), (0, 0))
6.35 + | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
6.36 + ((a div c, 0), (0, 0))
6.37 + | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
6.38 + ((power a c, 0), (0, 0))
6.39 + | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
6.40 + raise error ("calc: not impl. for Float (("^
6.41 + (string_of_int a )^","^(string_of_int b )^"), ("^
6.42 + (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
6.43 + (string_of_int c )^","^(string_of_int d )^"), ("^
6.44 + (string_of_int p21)^","^(string_of_int p22)^"))");
6.45 +(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
6.46 +val it = ((1,0),(0,0))*)
6.47 +
6.48 +
6.49 +(*.convert int and float to internal floatingpoint prepresentation.*)
6.50 +fun numeral (Free (str, T)) =
6.51 + (case int_of_str str of
6.52 + Some i => Some ((i, 0), (0, 0))
6.53 + | None => None)
6.54 + | numeral (Const ("Float.Float", _) $
6.55 + (Const ("Pair", _) $
6.56 + (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
6.57 + (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
6.58 + (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
6.59 + (Some v1', Some v2', Some p1', Some p2') =>
6.60 + Some ((v1', v2'), (p1', p2'))
6.61 + | _ => None)
6.62 + | numeral _ = None;
6.63 +
6.64 +(*.convert internal floatingpoint prepresentation to int and float.*)
6.65 +fun term_of_float T ((val1, 0), ( 0, 0)) =
6.66 + term_of_num T val1
6.67 + | term_of_float T ((val1, val2), (precision1, precision2)) =
6.68 + let val pT = pairT T T
6.69 + in Const ("Float.Float", (pairT pT pT) --> T)
6.70 + $ (pairt (pairt (Free (str_of_int val1, T))
6.71 + (Free (str_of_int val2, T)))
6.72 + (pairt (Free (str_of_int precision1, T))
6.73 + (Free (str_of_int precision2, T))))
6.74 + end;
6.75 +(*> val t = str2term "Float ((1,2),(0,0))";
6.76 +> val Const ("Float.Float", fT) $ _ = t;
6.77 +> atomtyp fT;
6.78 +> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
6.79 +> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
6.80 +> atomtyp ffT;
6.81 +> fT = ffT;
6.82 +val it = true : bool
6.83 +
6.84 +t = float_term_of_num HOLogic.realT ((1,2),(0,0));
6.85 +val it = true : bool*)
6.86 +
6.87 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
6.88 +fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
6.89 + var_op_num v op_ optype ntyp v1
6.90 + | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
6.91 + let val pT = pairT T T
6.92 + in Const (op_, optype) $ v $
6.93 + (Const ("Float.Float", (pairT pT pT) --> T)
6.94 + $ (pairt (pairt (Free (str_of_int v1, T))
6.95 + (Free (str_of_int v2, T)))
6.96 + (pairt (Free (str_of_int p1, T))
6.97 + (Free (str_of_int p2, T)))))
6.98 + end;
6.99 +(*> val t = str2term "a + b";
6.100 +> val Const ("op +", optype) $ _ $ _ = t;
6.101 +> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
6.102 +> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
6.103 +val it = true : bool*)
6.104 +
6.105 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
6.106 +fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
6.107 + num_op_var v op_ optype ntyp v1
6.108 + | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
6.109 + let val pT = pairT T T
6.110 + in Const (op_,optype) $
6.111 + (Const ("Float.Float", (pairT pT pT) --> T)
6.112 + $ (pairt (pairt (Free (str_of_int v1, T))
6.113 + (Free (str_of_int v2, T)))
6.114 + (pairt (Free (str_of_int p1, T))
6.115 + (Free (str_of_int p2, T))))) $ v
6.116 + end;
6.117 +(*> val t = str2term "a + b";
6.118 +> val Const ("op +", optype) $ _ $ _ = t;
6.119 +> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
6.120 +> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
6.121 +val it = true : bool*)
6.122 +
6.123 +
6.124 +
6.125 +
6.126 +
6.127 +
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/sml/IsacKnowledge/Float.thy Thu Apr 17 18:01:03 2003 +0200
7.3 @@ -0,0 +1,11 @@
7.4 +(* use_thy"Float";
7.5 + use_thy_only"Float";
7.6 + *)
7.7 +
7.8 +Float = Typefix +
7.9 +
7.10 +consts
7.11 +
7.12 + Float :: "((real * real) * (real * real)) => real"
7.13 +
7.14 +end
7.15 \ No newline at end of file
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/sml/IsacKnowledge/InsSort.ML Thu Apr 17 18:01:03 2003 +0200
8.3 @@ -0,0 +1,71 @@
8.4 +(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
8.5 +
8.6 +Proving equations for primrec function(s) "InsSort.foldr" ...
8.7 +GC #1.17.30.54.345.21479: (10 ms)
8.8 +*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
8.9 +*** imposes additional sort constraints on the declared type of the constant
8.10 +*** The error(s) above occurred in definition "InsSort.ins.ins_list_def"
8.11 +*)
8.12 +
8.13 +(* tools for insertion sort
8.14 + use"knowledge/InsSort.ML";
8.15 +*)
8.16 +
8.17 +(** interface isabelle -- isac **)
8.18 +
8.19 +theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
8.20 +
8.21 +(** rule set **)
8.22 +
8.23 +val ins_sort =
8.24 + Rls{preconds = [], rew_ord = ("tless_true",tless_true),
8.25 + rules = [Thm ("foldr_base",(*num_str*) foldr_base),
8.26 + Thm ("foldr_rec",foldr_rec),
8.27 + Thm ("ins_base",ins_base),
8.28 + Thm ("ins_rec",ins_rec),
8.29 + Thm ("sort_def",sort_def),
8.30 +
8.31 + Calc ("op <",eval_equ "#less_"),
8.32 + Thm ("if_True", if_True),
8.33 + Thm ("if_False", if_False)
8.34 + ],
8.35 + scr = Script ((term_of o the o (parse thy))
8.36 + "empty_script")
8.37 + }:rls;
8.38 +
8.39 +(** problem type **)
8.40 +
8.41 +store_pbt
8.42 + (prep_pbt InsSort.thy
8.43 + (["functional"]:pblID,
8.44 + [("#Given" ,["unsorted u_"]),
8.45 + ("#Find" ,["sorted s_"])
8.46 + ],
8.47 + []));
8.48 +
8.49 +store_pbt
8.50 + (prep_pbt InsSort.thy
8.51 + (["inssort","functional"]:pblID,
8.52 + [("#Given" ,["unsorted u_"]),
8.53 + ("#Find" ,["sorted s_"])
8.54 + ],
8.55 + []));
8.56 +
8.57 +(** method,
8.58 + todo: implementation needs extra object-level lists **)
8.59 +
8.60 +methods:= (!methods) @
8.61 +[
8.62 + prep_met (*test-version for [#1,#3,#2] only: see *.sml*)
8.63 + (("InsSort.thy","sort"):metID,
8.64 + [("#Given" ,["unsorted u_"]),
8.65 + ("#Find" ,["sorted s_"])
8.66 + ],
8.67 + {rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[]},
8.68 + "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
8.69 + )
8.70 +];
8.71 +
8.72 +ruleset' := overwritel (!ruleset',
8.73 + [(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
8.74 + ]:(string * rls) list);
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/sml/IsacKnowledge/InsSort.sml Thu Apr 17 18:01:03 2003 +0200
9.3 @@ -0,0 +1,395 @@
9.4 +
9.5 +
9.6 +(*-------------------------from InsSort.thy 8.3.01----------------------*)
9.7 +(*List.thy:
9.8 + foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
9.9 +primrec
9.10 + foldl_Nil "foldl f a [] = a"
9.11 + foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
9.12 +
9.13 +above in sml:
9.14 +fun foldr f [] a = a
9.15 + | foldr f (x::xs) a = foldr f xs (f a x);
9.16 +(*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
9.17 +fun ins [] a = [a]
9.18 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.19 +fun sort xs = foldr ins xs [];
9.20 +*)
9.21 +(*-------------------------from InsSort.thy 8.3.01----------------------*)
9.22 +
9.23 +
9.24 +(*-------------------------from InsSort.ML 8.3.01----------------------*)
9.25 +
9.26 +theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
9.27 +
9.28 +val ins_sort =
9.29 + Rls{preconds = [], rew_ord = ("tless_true",tless_true),
9.30 + rules = [Thm ("foldr_base",(*num_str*) foldr_base),
9.31 + Thm ("foldr_rec",foldr_rec),
9.32 + Thm ("ins_base",ins_base),
9.33 + Thm ("ins_rec",ins_rec),
9.34 + Thm ("sort_def",sort_def),
9.35 +
9.36 + Calc ("op <",eval_equ "#less_"),
9.37 + Thm ("if_True", if_True),
9.38 + Thm ("if_False", if_False)
9.39 + ],
9.40 + scr = Script ((term_of o the o (parse thy))
9.41 + "empty_script")
9.42 + }:rls;
9.43 +
9.44 +
9.45 +
9.46 +
9.47 +(*
9.48 +> get_pbt ["Script.thy","squareroot","univariate","equation"];
9.49 +> get_met ("Script.thy","max_on_interval_by_calculus");
9.50 +*)
9.51 +pbltypes:= (!pbltypes) @
9.52 +[
9.53 + prep_pbt InsSort.thy
9.54 + (["InsSort.thy","inssort"]:pblID,
9.55 + [("#Given" ,"unsorted u_"),
9.56 + ("#Find" ,"sorted s_")
9.57 + ])
9.58 +];
9.59 +
9.60 +methods:= (!methods) @
9.61 +[
9.62 +(*, -------17.6.00,
9.63 + (("InsSort.thy","inssort"):metID,
9.64 + {ppc = prep_met
9.65 + [("#Given" ,"unsorted u_"),
9.66 + ("#Find" ,"sorted s_")
9.67 + ],
9.68 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
9.69 + scr=Script (((inst_abs (assoc_thm "InsSort.thy"))
9.70 + o term_of o the o (parse thy)) (*for [#1,#3,#2] only*)
9.71 + "Script Ins_sort (u_::'a list) = \
9.72 + \ (let u_ = Rewrite sort_def False u_; \
9.73 + \ u_ = Rewrite foldr_rec False u_; \
9.74 + \ u_ = Rewrite ins_base False u_; \
9.75 + \ u_ = Rewrite foldr_rec False u_; \
9.76 + \ u_ = Rewrite ins_rec False u_; \
9.77 + \ u_ = Calculate le u_; \
9.78 + \ u_ = Rewrite if_True False u_; \
9.79 + \ u_ = Rewrite ins_base False u_; \
9.80 + \ u_ = Rewrite foldr_rec False u_; \
9.81 + \ u_ = Rewrite ins_rec False u_; \
9.82 + \ u_ = Calculate le u_; \
9.83 + \ u_ = Rewrite if_True False u_; \
9.84 + \ u_ = Rewrite ins_rec False u_; \
9.85 + \ u_ = Calculate le u_; \
9.86 + \ u_ = Rewrite if_False False u_; \
9.87 + \ u_ = Rewrite foldr_base False u_ \
9.88 + \ in u_)")
9.89 + } : meth'),
9.90 +
9.91 + (("InsSort.thy","sort"):metID,
9.92 + {ppc = prep_met
9.93 + [("#Given" ,"unsorted u_"),
9.94 + ("#Find" ,"sorted s_")
9.95 + ],
9.96 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
9.97 + scr=Script ((inst_abs o term_of o the o (parse thy))
9.98 + "Script Sort (u_::'a list) = \
9.99 + \ Rewrite_Set ins_sort False u_")
9.100 + } : meth')
9.101 +------- *)
9.102 +(*,
9.103 +
9.104 + (("",""):metID,
9.105 + {ppc = prep_met
9.106 + [("#Given" ,""),
9.107 + ("#Find" ,""),
9.108 + ("#Relate","")
9.109 + ],
9.110 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
9.111 + scr=EmptyScr} : meth'),
9.112 +*)
9.113 +];
9.114 +(*-------------------------from InsSort.ML 8.3.01----------------------*)
9.115 +
9.116 +
9.117 +(*------------------------- nipkow ----------------------*)
9.118 +consts
9.119 + sort :: 'a list => 'a list
9.120 + ins :: ['a,'a list] => 'a list
9.121 +(*foldl :: [['a,'b] => 'a, 'a, 'b list] => 'a
9.122 +*)
9.123 +rules
9.124 + ins_base "ins e [] = [e]"
9.125 + ins_rec "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))"
9.126 +
9.127 +rules
9.128 + sort_def "sort ls = (foldl ins ls [])"
9.129 +end
9.130 +
9.131 +
9.132 +(** swp: ..L **)
9.133 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
9.134 +fun foldL f [] e = e
9.135 + | foldL f (l::ls) e = f(l,foldL f ls e);
9.136 +
9.137 +(* fn : int * int list -> int list *)
9.138 +fun insL (e,[]) = [e]
9.139 + | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls);
9.140 +
9.141 +fun sortL ls = foldL insL ls [];
9.142 +
9.143 +sortL [2,3,1]; (* [1,2,3] *)
9.144 +
9.145 +
9.146 +(** swp, curried: ..LC **)
9.147 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
9.148 +fun foldLC f [] e = e
9.149 + | foldLC f (x::xs) e = f x (foldLC f xs e);
9.150 +
9.151 +(* fn : int * int list -> int list *)
9.152 +fun insLC e [] = [e]
9.153 + | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls);
9.154 +
9.155 +fun sortLC ls = foldLC insLC ls [];
9.156 +
9.157 +sortLC [2,3,1]; (* [1,2,3] *)
9.158 +
9.159 +
9.160 +(** sml110: ..l **)
9.161 +(* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *)
9.162 +foldl;
9.163 +(* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a : ANDERS !!!
9.164 +fun foldl f e [] = e
9.165 + | foldl f e (l::ls) = f e (foldl f (e,ls)); 0+...+0+0
9.166 +
9.167 +foldl op+ (0,[100,11,1]);
9.168 +val it = 0 : int ... GEHT NICHT !!! *)
9.169 +
9.170 +fun insl (e,[]) = [e]
9.171 + | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls);
9.172 +
9.173 +fun sortl ls = foldl insl [] ls;
9.174 +
9.175 +sortl [2,3,1]; (* [1,2,3] *)
9.176 +
9.177 +
9.178 +(** sml110, curried: ..lC **)
9.179 +(* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *)
9.180 +fun foldlC f e [] = e
9.181 + | foldlC f e (l::ls) = f e (foldlC f e ls);
9.182 +
9.183 +(* fn : int -> int list -> int list *)
9.184 +fun inslC e [] = [e]
9.185 + | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls);
9.186 +
9.187 +fun sortlC ls = foldlC inslC [] ls;
9.188 +
9.189 +sortlC [2,3,1];
9.190 +
9.191 +(*--- 15.6.00 ---*)
9.192 +
9.193 +
9.194 +fun Foldl f a [] = a
9.195 + | Foldl f a (x::xs) = Foldl f (f a x) xs;
9.196 +(*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*)
9.197 +
9.198 +fun add a b = a+b:int;
9.199 +
9.200 +Foldl add 0 [1,2,3];
9.201 +
9.202 +fun ins0 a [] = [a]
9.203 + | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs);
9.204 +(*val ins = fn : int -> int list -> int list*)
9.205 +
9.206 +fun ins [] a = [a]
9.207 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.208 +(*val ins = fn : int -> int list -> int list*)
9.209 +
9.210 +ins 3 [1,2,4];
9.211 +
9.212 +fun sort xs = Foldl ins0 xs [];
9.213 +(*operator domain: int -> int list -> int
9.214 + operand: int -> int list -> int list
9.215 + in expression:
9.216 + Foldl ins
9.217 + *)
9.218 +fun sort xs = Foldl ins xs [];
9.219 +
9.220 +
9.221 +
9.222 +(*--- 17.6.00 ---*)
9.223 +
9.224 +
9.225 +fun foldr f [] a = a
9.226 + | foldr f (x::xs) a = foldr f xs (f a x);
9.227 +(*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
9.228 +
9.229 +fun add a b = a+b:int;
9.230 +
9.231 +fold add [1,2,3] 0;
9.232 +
9.233 +fun ins [] a = [a]
9.234 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.235 +(*val ins = fn : int list -> int -> int list*)
9.236 +
9.237 +ins [1,2,4] 3;
9.238 +
9.239 +fun sort xs = foldr ins xs [];
9.240 +
9.241 +sort [3,1,4,2];
9.242 +
9.243 +
9.244 +
9.245 +(*--- 17.6.00 II ---*)
9.246 +
9.247 +fun foldl f a [] = a
9.248 + | foldl f a (x::xs) = foldl f (f a x) xs;
9.249 +
9.250 +fun ins [] a = [a]
9.251 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.252 +
9.253 +fun sort xs = foldl ins xs [];
9.254 +
9.255 +sort [3,1,4,2];
9.256 +(*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*)
9.257 +
9.258 +(*------------------------- nipkow ----------------------*)
9.259 +consts
9.260 + sort :: 'a list => 'a list
9.261 + ins :: ['a,'a list] => 'a list
9.262 +(*foldl :: [['a,'b] => 'a, 'a, 'b list] => 'a
9.263 +*)
9.264 +rules
9.265 + ins_base "ins e [] = [e]"
9.266 + ins_rec "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))"
9.267 +
9.268 +rules
9.269 + sort_def "sort ls = (foldl ins ls [])"
9.270 +end
9.271 +
9.272 +
9.273 +(** swp: ..L **)
9.274 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
9.275 +fun foldL f [] e = e
9.276 + | foldL f (l::ls) e = f(l,foldL f ls e);
9.277 +
9.278 +(* fn : int * int list -> int list *)
9.279 +fun insL (e,[]) = [e]
9.280 + | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls);
9.281 +
9.282 +fun sortL ls = foldL insL ls [];
9.283 +
9.284 +sortL [2,3,1]; (* [1,2,3] *)
9.285 +
9.286 +
9.287 +(** swp, curried: ..LC **)
9.288 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
9.289 +fun foldLC f [] e = e
9.290 + | foldLC f (x::xs) e = f x (foldLC f xs e);
9.291 +
9.292 +(* fn : int * int list -> int list *)
9.293 +fun insLC e [] = [e]
9.294 + | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls);
9.295 +
9.296 +fun sortLC ls = foldLC insLC ls [];
9.297 +
9.298 +sortLC [2,3,1]; (* [1,2,3] *)
9.299 +
9.300 +
9.301 +(** sml110: ..l **)
9.302 +(* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *)
9.303 +foldl;
9.304 +(* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a : ANDERS !!!
9.305 +fun foldl f e [] = e
9.306 + | foldl f e (l::ls) = f e (foldl f (e,ls)); 0+...+0+0
9.307 +
9.308 +foldl op+ (0,[100,11,1]);
9.309 +val it = 0 : int ... GEHT NICHT !!! *)
9.310 +
9.311 +fun insl (e,[]) = [e]
9.312 + | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls);
9.313 +
9.314 +fun sortl ls = foldl insl [] ls;
9.315 +
9.316 +sortl [2,3,1]; (* [1,2,3] *)
9.317 +
9.318 +
9.319 +(** sml110, curried: ..lC **)
9.320 +(* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *)
9.321 +fun foldlC f e [] = e
9.322 + | foldlC f e (l::ls) = f e (foldlC f e ls);
9.323 +
9.324 +(* fn : int -> int list -> int list *)
9.325 +fun inslC e [] = [e]
9.326 + | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls);
9.327 +
9.328 +fun sortlC ls = foldlC inslC [] ls;
9.329 +
9.330 +sortlC [2,3,1];
9.331 +
9.332 +(*--- 15.6.00 ---*)
9.333 +
9.334 +
9.335 +fun Foldl f a [] = a
9.336 + | Foldl f a (x::xs) = Foldl f (f a x) xs;
9.337 +(*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*)
9.338 +
9.339 +fun add a b = a+b:int;
9.340 +
9.341 +Foldl add 0 [1,2,3];
9.342 +
9.343 +fun ins0 a [] = [a]
9.344 + | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs);
9.345 +(*val ins = fn : int -> int list -> int list*)
9.346 +
9.347 +fun ins [] a = [a]
9.348 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.349 +(*val ins = fn : int -> int list -> int list*)
9.350 +
9.351 +ins 3 [1,2,4];
9.352 +
9.353 +fun sort xs = Foldl ins0 xs [];
9.354 +(*operator domain: int -> int list -> int
9.355 + operand: int -> int list -> int list
9.356 + in expression:
9.357 + Foldl ins
9.358 + *)
9.359 +fun sort xs = Foldl ins xs [];
9.360 +
9.361 +
9.362 +
9.363 +(*--- 17.6.00 ---*)
9.364 +
9.365 +
9.366 +fun foldr f [] a = a
9.367 + | foldr f (x::xs) a = foldr f xs (f a x);
9.368 +(*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
9.369 +
9.370 +fun add a b = a+b:int;
9.371 +
9.372 +fold add [1,2,3] 0;
9.373 +
9.374 +fun ins [] a = [a]
9.375 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.376 +(*val ins = fn : int list -> int -> int list*)
9.377 +
9.378 +ins [1,2,4] 3;
9.379 +
9.380 +fun sort xs = foldr ins xs [];
9.381 +
9.382 +sort [3,1,4,2];
9.383 +
9.384 +
9.385 +
9.386 +(*--- 17.6.00 II ---*)
9.387 +
9.388 +fun foldl f a [] = a
9.389 + | foldl f a (x::xs) = foldl f (f a x) xs;
9.390 +
9.391 +fun ins [] a = [a]
9.392 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
9.393 +
9.394 +fun sort xs = foldl ins xs [];
9.395 +
9.396 +sort [3,1,4,2];
9.397 +(*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*)
9.398 +(*------------------------- nipkow ----------------------*)
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/sml/IsacKnowledge/InsSort.thy Thu Apr 17 18:01:03 2003 +0200
10.3 @@ -0,0 +1,47 @@
10.4 +(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
10.5 +
10.6 +Proving equations for primrec function(s) "InsSort.foldr" ...
10.7 +GC #1.17.30.54.345.21479: (10 ms)
10.8 +*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
10.9 +*** imposes additional sort constraints on the declared type of the constant
10.10 +*** The error(s) above occurred in definition "InsSort.ins.ins_list_def"
10.11 +*)
10.12 +
10.13 +(* insertion sort, would need lists different from script-lists
10.14 + WN.11.00
10.15 + *)
10.16 +
10.17 +InsSort = Script +
10.18 +
10.19 +consts
10.20 +
10.21 + foldr :: [['a,'b] => 'a, 'b list, 'a] => 'a
10.22 + ins :: ['a list,'a] => 'a list
10.23 + sort :: 'a list => 'a list
10.24 +
10.25 +(*descriptions, script-id*)
10.26 + unsorted :: 'a list => una
10.27 + sorted :: 'a list => toreall
10.28 +
10.29 +(*subproblem and script-name*)
10.30 + Ins'_sort :: "['a list, \
10.31 + \ 'a list] => 'a list"
10.32 + ("((Script Ins'_sort (_ =))// \
10.33 + \ (_))" 9)
10.34 + Sort :: "['a list, \
10.35 + \ 'a list] => 'a list"
10.36 + ("((Script Sort (_ =))// \
10.37 + \ (_))" 9)
10.38 +
10.39 +primrec
10.40 + foldr_base "foldr f [] a = a"
10.41 + foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)"
10.42 +primrec
10.43 + ins_base "ins [] a = [a]"
10.44 + ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"
10.45 +
10.46 +rules
10.47 +
10.48 + sort_def "sort ls = foldr ins ls []"
10.49 +
10.50 +end