1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Test.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,159 @@
1.4 +val ttt = (term_of o the o (parse thy))
1.5 +"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_";
1.6 +val ttt = (term_of o the o (parse thy))
1.7 +"(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_)";
1.8 +
1.9 +val ttt = (term_of o the o (parse thy))
1.10 + "(Rewrite_Set SqRoot_simplify False) e_ ";
1.11 +val ttt = (term_of o the o (parseold thy))
1.12 + "%e_. (Rewrite_Set SqRoot_simplify False) e_";
1.13 +val ttt = (term_of o the o (parseold thy))
1.14 + "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_";
1.15 +
1.16 +val ttt = (term_of o the o (parse thy))
1.17 + "Script Solve_linear (e_::bool) (v_::real)= \
1.18 + \[e_]";
1.19 +val ttt = (term_of o the o (parse thy))
1.20 + "Script Solve_linear (e_::bool) (v_::real)= \
1.21 + \((%e_. [e_]) e_)";
1.22 +val ttt = (term_of o the o (parse thy))
1.23 + "Script Solve_linear (e_::bool) (v_::real)= \
1.24 + \((%e_. (let e_ = e_ in [e_])) e_)";
1.25 +val ttt = (term_of o the o (parse thy))
1.26 + "Script Solve_linear (e_::bool) (v_::real)= \
1.27 + \((%e_. \
1.28 + \ (let e_ = ((Rewrite_Set SqRoot_simplify False) e_)\
1.29 + \ in [e_]))\
1.30 + \ e_)";
1.31 +val ttt = (term_of o the o (parse thy))
1.32 + "Script Solve_linear (e_::bool) (v_::real)= \
1.33 + \((%ee_. (let e_ = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_)";
1.34 +
1.35 +val ttt = (term_of o the o (parse thy))
1.36 + "Script Solve_linear (e_::bool) (v_::real)= \
1.37 + \(let e_ = \
1.38 + \ (Repeat ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False)) e_)\
1.39 + \ in [e_])";
1.40 +(*----*)
1.41 +val ttt = (term_of o the o (parse thy))
1.42 +
1.43 +(*----*)
1.44 +val ttt = (term_of o the o (parse thy))
1.45 + "Script Solve_linear (e_::bool) (v_::real)= \
1.46 + \(let e_ = \
1.47 + \ (Repeat\
1.48 + \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
1.49 + \ e_)\
1.50 + \ e_)\
1.51 + \ in [e_])";
1.52 +val ttt = (term_of o the o (parse thy))
1.53 + "Script Solve_linear (e_::bool) (v_::real)= \
1.54 + \(let e_ = \
1.55 + \ (Repeat\
1.56 + \ ((%ee_.\
1.57 + \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_))\
1.58 + \ e_)\
1.59 + \ e_)\
1.60 + \ in [e_])";
1.61 +val ttt = (term_of o the o (parse thy))
1.62 + "Script Solve_linear (e_::bool) (v_::real)= \
1.63 + \(let e_ = \
1.64 + \ (Repeat\
1.65 + \ ((%ee_.\
1.66 + \ (let e_ = ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
1.67 + \ in ((Rewrite_Set SqRoot_simplify False) e_)) )\
1.68 + \ e_)\
1.69 + \ e_)\
1.70 + \ in [e_])";
1.71 +atomty thy ttt;
1.72 +atomt ttt;
1.73 +
1.74 +val ttt = (term_of o the o (parse thy))
1.75 + "Script Testterm (g_::real) = \
1.76 + \Repeat\
1.77 + \ (Rewrite rmult_1 False) g_";
1.78 +val ttt = (term_of o the o (parse thy))
1.79 + "Script Testterm (g_::real) = \
1.80 + \Repeat\
1.81 + \ (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_";
1.82 +val ttt = (term_of o the o (parse thy))
1.83 + "Script Testterm (g_::real) = \
1.84 + \Repeat\
1.85 + \ ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_";
1.86 +val ttt = (term_of o the o (parse thy))
1.87 + "Script Testterm (g_::real) = \
1.88 + \Repeat\
1.89 + \ ((Repeat (Rewrite rmult_1 False)) Or\
1.90 + \ (Repeat (Rewrite rmult_0 False))) g_";
1.91 +val ttt = (term_of o the o (parse thy))
1.92 + "Script Testterm (g_::real) = \
1.93 + \Repeat\
1.94 + \ ((Repeat (Rewrite rmult_1 False)) Or\
1.95 + \ (Repeat (Rewrite rmult_0 False)) Or\
1.96 + \ (Repeat (Rewrite rmult_0 False))) g_";
1.97 +val ttt = (term_of o the o (parse thy))
1.98 + "Script Testterm (g_::real) = \
1.99 + \Repeat\
1.100 + \ ((Try Repeat (Rewrite rmult_1 False)) Or\
1.101 + \ (Try Repeat (Rewrite rmult_0 False)) Or\
1.102 + \ (Try Repeat (Rewrite rmult_0 False))) g_";
1.103 +
1.104 +
1.105 +
1.106 +
1.107 +
1.108 +
1.109 +
1.110 +
1.111 +
1.112 +
1.113 +
1.114 +
1.115 +
1.116 +(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
1.117 +(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
1.118 +(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
1.119 +
1.120 +
1.121 +
1.122 +atomt ttt;
1.123 +val ttt = (term_of o the o (parse thy))
1.124 + "Script Solve_linear (e_::bool) (v_::real)= \
1.125 + \(let e_ = \
1.126 + \ ((Repeat\
1.127 + \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.128 + \ (Rewrite_Set SqRoot_simplify False)))) e_)\
1.129 + \ in [e_])";
1.130 +atomty thy ttt;
1.131 +
1.132 +
1.133 +val ttt = (term_of o the o (parse thy))
1.134 +"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@ yyy";
1.135 +atomty thy ttt;
1.136 +val ttt = (term_of o the o (parse thy))
1.137 + "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.138 + \ (Rewrite_Set SqRoot_simplify False)";
1.139 +atomty thy ttt;
1.140 +val ttt = (term_of o the o (parse thy))
1.141 + "(Repeat\
1.142 + \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.143 + \ (Rewrite_Set SqRoot_simplify False))) e_";
1.144 +atomty thy ttt;
1.145 +val ttt = (term_of o the o (parseold thy))
1.146 +"(let e_ = Repeat xxx e_ in [e_::bool])";
1.147 +atomty thy ttt;
1.148 +val ttt = (term_of o the o (parseold thy))
1.149 + "Script Solve_linear (e_::bool) (v_::real)= \
1.150 + \(let e_ = Repeat (xxx) e_ in [e_::bool])";
1.151 +atomty thy ttt;
1.152 +val ttt = (term_of o the o (parseold thy))
1.153 + "Script Solve_linear (e_::bool) (v_::real)= \
1.154 + \(let e_ =\
1.155 + \ Repeat\
1.156 + \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.157 + \ (Rewrite_Set SqRoot_simplify False))) e_\
1.158 + \ in [e_::bool])"
1.159 +;
1.160 +atomty thy ttt;
1.161 +
1.162 +use"RatArith.ML";