1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc/mat-eng.sml Thu Apr 17 18:01:02 2003 +0200
1.3 @@ -0,0 +1,324 @@
1.4 +(* cut and paste for math.tex
1.5 +*)
1.6 +
1.7 +(*2.2. Theories and parsing*)
1.8 + thy;
1.9 + parse;
1.10 + parse thy "a + b * #3";
1.11 + val t = (term_of o the) it;
1.12 + term_of;
1.13 +
1.14 +(*2.3. Displaying terms*)
1.15 + Compiler.Control.Print.printDepth;
1.16 + Compiler.Control.Print.printDepth:= 2;
1.17 + t;
1.18 + Compiler.Control.Print.printDepth:= 6;
1.19 + t;
1.20 + Compiler.Control.Print.printLength;
1.21 + Compiler.Control.Print.stringDepth;
1.22 + atomt;
1.23 + atomt t;
1.24 + atomty;
1.25 + atomty thy t;
1.26 +(*Give it a try: the mathematics knowledge grows*)
1.27 + parse HOL.thy "#2^^^#3";
1.28 + parse HOL.thy "d_d x (a + x)";
1.29 + parse RatArith.thy "#2^^^#3";
1.30 + parse RatArith.thy "d_d x (a + x)";
1.31 + parse Differentiate.thy "d_d x (a + x)";
1.32 + parse Differentiate.thy "#2^^^#3";
1.33 +(*don't trust the string representation*)
1.34 + val thy = RatArith.thy;
1.35 + ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
1.36 + val thy = Differentiate.thy;
1.37 + ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
1.38 +
1.39 +(*2.4. Converting terms*)
1.40 + term_of;
1.41 + the;
1.42 + val t = (term_of o the o (parse thy)) "a + b * #3";
1.43 +
1.44 + sign_of;
1.45 + cterm_of;
1.46 + val ct = cterm_of (sign_of thy) t;
1.47 +
1.48 + Sign.string_of_term;
1.49 + Sign.string_of_term (sign_of thy) t;
1.50 +
1.51 + string_of_cterm;
1.52 + string_of_cterm ct;
1.53 +
1.54 +(*2.5. Theorems *)
1.55 + theorem' := overwritel (!theorem',
1.56 + [("diff_const",num_str diff_const)
1.57 + ]);
1.58 +
1.59 +(** 3. Rewriting **)
1.60 +(*3.1. The arguments for rewriting*)
1.61 + HOL.thy;
1.62 + "HOL.thy" : theory';
1.63 + sqrt_right;
1.64 + "sqrt_right" : rew_ord';
1.65 + eval_rls;
1.66 + "eval_rls" : rls';
1.67 + diff_sum;
1.68 + ("diff_sum", "") : thm';
1.69 +
1.70 +(*3.2. The functions for rewriting*)
1.71 + rewrite_;
1.72 + rewrite;
1.73 +(*Give it a try: rewriting*)
1.74 + val thy' = "Differentiate.thy";
1.75 + val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
1.76 + val thm = ("diff_sum","");
1.77 + val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.78 + [("bdv","x::real")] thm ct;
1.79 + val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.80 + [("bdv","x::real")] thm ct;
1.81 + val thm = ("diff_prod_const","");
1.82 + val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.83 + [("bdv","x::real")] thm ct;
1.84 +(*Give it a try: conditional rewriting*)
1.85 + val thy' = "Isac.thy";
1.86 + val ct' = "#3 * a + #2 * (a + #1)";
1.87 + val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
1.88 + (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.89 + val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
1.90 + (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.91 + val thm' = ("rcollect_right",
1.92 + "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
1.93 + (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.94 + (*4*) val Some (ct',_) = calculate thy' "plus" ct';
1.95 + (*5*) val Some (ct',_) = calculate thy' "times" ct';
1.96 +
1.97 +(*Give it a try: functional programming*)
1.98 + val thy' = "InsSort.thy";
1.99 + val ct = "sort [#1,#3,#2]" : cterm';
1.100 +
1.101 + val thm = ("sort_def","");
1.102 + val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.103 +
1.104 + val thm = ("foldr_rec","");
1.105 + val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.106 +
1.107 + val thm = ("ins_base","");
1.108 + val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.109 +
1.110 + val thm = ("foldr_rec","");
1.111 + val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.112 +
1.113 + val thm = ("ins_rec","");
1.114 + val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.115 +
1.116 + val (ct,_) = the (calculate thy' "le" ct);
1.117 +
1.118 + val thm = ("if_True","(if True then ?x else ?y) = ?x");
1.119 + val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.120 +
1.121 +(*3.3. Variants of rewriting*)
1.122 + rewrite_inst_;
1.123 + rewrite_inst;
1.124 +
1.125 + rewrite_set_;
1.126 + rewrite_set;
1.127 +
1.128 + rewrite_set_inst_;
1.129 + rewrite_set_inst;
1.130 +
1.131 + toggle;
1.132 + toggle trace_rewrite;
1.133 +
1.134 +(*3.4. Rule sets*)
1.135 + sym;
1.136 + rearrange_assoc;
1.137 +
1.138 +(*Give it a try: remove parentheses*)
1.139 + val ct = (string_of_cterm o the o (parse RatArith.thy))
1.140 + "a + (b * (c * d) + e)";
1.141 + rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
1.142 +
1.143 + toggle trace_rewrite;
1.144 + rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
1.145 +
1.146 +(*3.5. Calculate numeric constants*)
1.147 + calculate;
1.148 + calculate_;
1.149 +
1.150 + calc_list;
1.151 + calculate "Isac.thy" "plus" "#1 + #2";
1.152 + calculate "Isac.thy" "times" "#2 * #3";
1.153 + calculate "Isac.thy" "power" "#2 ^^^ #3";
1.154 + calculate "Isac.thy" "cancel_" "#9 // #12";
1.155 +
1.156 +
1.157 +(** 4. Term orders **)
1.158 +(*4.1. Exmpales for term orders*)
1.159 + sqrt_right;
1.160 + tless_true;
1.161 +
1.162 + val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
1.163 + val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
1.164 + sqrt_right false SqRoot.thy (t1, t2);
1.165 + sqrt_right false SqRoot.thy (t2, t1);
1.166 +
1.167 + val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
1.168 + val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
1.169 + sqrt_right true SqRoot.thy (t1, t2);
1.170 +
1.171 +(*4.2. Ordered rewriting*)
1.172 + ac_plus_times;
1.173 +
1.174 +(*Give it a try: polynomial (normal) form*)
1.175 + val ct' = "#3 * a + b + #2 * a";
1.176 + val thm' = ("radd_commute","") : thm';
1.177 + val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.178 + val thm' = ("rdistr_right_assoc_p","") : thm';
1.179 + val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.180 + val Some (ct',_) = calculate thy' "plus" ct';
1.181 +
1.182 + val ct' = "#3 * a + b + #2 * a" : cterm';
1.183 + val thm' = ("radd_commute","") : thm';
1.184 + val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.185 + val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.186 + val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.187 +
1.188 + toggle trace_rewrite;
1.189 + rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
1.190 +
1.191 +
1.192 +(** 5. The hierarchy of problem types **)
1.193 +(*5.1. The standard-function for 'matching'*)
1.194 + matches;
1.195 +
1.196 + val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";
1.197 + val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";
1.198 + atomt p;
1.199 + free2var;
1.200 + val pat = free2var p;
1.201 + matches thy t pat;
1.202 +
1.203 + val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";
1.204 + matches thy t2 pat;
1.205 +
1.206 + val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";
1.207 + matches thy t2 pat2;
1.208 +
1.209 +(*5.2. Accessing the hierarchy*)
1.210 + show_ptyps;
1.211 + show_ptyps();
1.212 + get_pbt;
1.213 + get_pbt ["squareroot", "univariate", "equation"];
1.214 +
1.215 + store_pbt;
1.216 + store_pbt
1.217 + (prep_pbt SqRoot.thy
1.218 + (["newtype","univariate","equation"],
1.219 + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1.220 + ("#Where" ,["contains_root (e_::bool)"]),
1.221 + ("#Find" ,["solutions v_i_"])
1.222 + ],
1.223 + [("SqRoot.thy","square_equation")]));
1.224 + show_ptyps();
1.225 +
1.226 +(*5.3. Internals of the datastructure*)
1.227 +(*5.4. Match a problem with a problem type*)
1.228 + val fmz = ["equality (#1 + #2 * x = #0)",
1.229 + "solveFor x",
1.230 + "solutions L"] : fmz;
1.231 + match_pbl;
1.232 + match_pbl fmz (get_pbt ["univariate","equation"]);
1.233 + match_pbl fmz (get_pbt ["linear","univariate","equation"]);
1.234 + match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
1.235 +
1.236 +(*5.5. Refine a problem specification *)
1.237 + refine;
1.238 + val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1.239 + "solveFor x","errorBound (eps=#0)",
1.240 + "solutions L"];
1.241 + refine fmz ["univariate","equation"];
1.242 +
1.243 + val fmz = ["equality (x+#1=#2)",
1.244 + "solveFor x","errorBound (eps=#0)",
1.245 + "solutions L"];
1.246 + refine fmz ["univariate","equation"];
1.247 +
1.248 +
1.249 +(* 6. Do a calculational proof *)
1.250 + val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x",
1.251 + "errorBound (eps=#0)","solutions L"];
1.252 + val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
1.253 + ("SqRoot.thy","no_met"));
1.254 +
1.255 +(*6.1. Initialize the calculation*)
1.256 + val p = e_pos'; val c = [];
1.257 + val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1.258 + val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree;
1.259 +
1.260 + Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
1.261 +
1.262 + nxt;
1.263 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.264 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.265 +
1.266 +(*6.2. The phase of modeling*)
1.267 + nxt;
1.268 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.269 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.270 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.271 +
1.272 + Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
1.273 +
1.274 +(*6.3. The phase of specification*)
1.275 + nxt;
1.276 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.277 +
1.278 +
1.279 + val nxt = ("Specify_Problem",
1.280 + Specify_Problem ["polynomial","univariate","equation"]);
1.281 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.282 +
1.283 + val nxt = ("Specify_Problem",
1.284 + Specify_Problem ["linear","univariate","equation"]);
1.285 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.286 + Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
1.287 +
1.288 + val nxt = ("Refine_Problem",
1.289 + Refine_Problem ["linear","univariate","equation"]);
1.290 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.291 + Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1.292 +
1.293 + val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
1.294 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.295 + Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1.296 +
1.297 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.298 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.299 +
1.300 +(*6.4. The phase of solving*)
1.301 + nxt;
1.302 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.303 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.304 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.305 +
1.306 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.307 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.308 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.309 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.310 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.311 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.312 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.313 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.314 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.315 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.316 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.317 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.318 +
1.319 +(*6.5. The final phase: check the postcondition*)
1.320 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.321 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.322 +
1.323 +
1.324 +
1.325 +
1.326 +
1.327 +