1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Test_thy.ML Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,174 @@
1.4 +structure Test =
1.5 +struct
1.6 +
1.7 +local
1.8 + val parse_ast_translation = [];
1.9 + val parse_translation = [];
1.10 + val print_translation = [];
1.11 + val typed_print_translation = [];
1.12 + val print_ast_translation = [];
1.13 + val token_translation = [];
1.14 +in
1.15 +
1.16 +
1.17 +
1.18 +val thy = IsarThy.begin_theory "Test" ["Atools", "Rational", "Root", "Poly"] []
1.19 +
1.20 +|> Theory.add_trfuns
1.21 +(parse_ast_translation, parse_translation, print_translation, print_ast_translation)
1.22 +|> Theory.add_trfunsT typed_print_translation
1.23 +|> Theory.add_tokentrfuns token_translation
1.24 +
1.25 +|> Theory.add_consts
1.26 +[("Expand'_binomtest", "['y, \
1.27 + \ 'y] => 'y", Mixfix ("((Script Expand'_binomtest (_ =))// \
1.28 + \ (_))", [], 9)),
1.29 + ("Solve'_univar'_err", "[bool,real,bool, \
1.30 + \ bool list] => bool list", Mixfix ("((Script Solve'_univar'_err (_ _ _ =))// \
1.31 + \ (_))", [], 9)),
1.32 + ("Solve'_linear", "[bool,real, \
1.33 + \ bool list] => bool list", Mixfix ("((Script Solve'_linear (_ _ =))// \
1.34 + \ (_))", [], 9)),
1.35 + ("is'_root'_free", "'a => bool ", Mixfix ("is'_root'_free _", [], 10)),
1.36 + ("contains'_root", "'a => bool ", Mixfix ("contains'_root _", [], 10)),
1.37 + ("Solve'_root'_equation", "[bool,real,bool, \
1.38 + \ bool list] => bool list", Mixfix ("((Script Solve'_root'_equation (_ _ _ =))// \
1.39 + \ (_))", [], 9)),
1.40 + ("Solve'_plain'_square", "[bool,real, \
1.41 + \ bool list] => bool list", Mixfix ("((Script Solve'_plain'_square (_ _ =))// \
1.42 + \ (_))", [], 9)),
1.43 + ("Norm'_univar'_equation", "[bool,real, \
1.44 + \ bool] => bool", Mixfix ("((Script Norm'_univar'_equation (_ _ =))// \
1.45 + \ (_))", [], 9)),
1.46 + ("STest'_simplify", "[real, \
1.47 + \ real] => real", Mixfix ("((Script STest'_simplify (_ =))// \
1.48 + \ (_))", [], 9))]
1.49 +
1.50 +|> (#1 oo (PureThy.add_axioms o map Thm.no_attributes))
1.51 +[("radd_mult_distrib2", "(k::real) * (m + n) = k * m + k * n"),
1.52 + ("rdistr_right_assoc", "(k::real) + l * n + m * n = k + (l + m) * n"),
1.53 + ("rdistr_right_assoc_p", "l * n + (m * n + (k::real)) = (l + m) * n + k"),
1.54 + ("rdistr_div_right", "((k::real) + l) / n = k / n + l / n"),
1.55 + ("rcollect_right", "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"),
1.56 + ("rcollect_one_left", "m is_const ==> (n::real) + m * n = (1 + m) * n"),
1.57 + ("rcollect_one_left_assoc", "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"),
1.58 + ("rcollect_one_left_assoc_p", "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"),
1.59 + ("rtwo_of_the_same", "a + a = 2 * a"),
1.60 + ("rtwo_of_the_same_assoc", "(x + a) + a = x + 2 * a"),
1.61 + ("rtwo_of_the_same_assoc_p", "a + (a + x) = 2 * a + x"),
1.62 + ("rcancel_den", "not(a=0) ==> a * (b / a) = b"),
1.63 + ("rcancel_const", "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"),
1.64 + ("rshift_nominator", "(a::real) * b / c = a / c * b"),
1.65 + ("exp_pow", "(a ^^^ b) ^^^ c = a ^^^ (b * c)"),
1.66 + ("rsqare", "(a::real) * a = a ^^^ 2"),
1.67 + ("power_1", "(a::real) ^^^ 1 = a"),
1.68 + ("rbinom_power_2", "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"),
1.69 + ("rmult_1", "1 * k = (k::real)"),
1.70 + ("rmult_1_right", "k * 1 = (k::real)"),
1.71 + ("rmult_0", "0 * k = (0::real)"),
1.72 + ("rmult_0_right", "k * 0 = (0::real)"),
1.73 + ("radd_0", "0 + k = (k::real)"),
1.74 + ("radd_0_right", "k + 0 = (k::real)"),
1.75 + ("radd_real_const_eq", "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"),
1.76 + ("radd_real_const", "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"),
1.77 + ("radd_commute", "(m::real) + (n::real) = n + m"),
1.78 + ("radd_left_commute", "(x::real) + (y + z) = y + (x + z)"),
1.79 + ("radd_assoc", "(m::real) + n + k = m + (n + k)"),
1.80 + ("rmult_commute", "(m::real) * n = n * m"),
1.81 + ("rmult_left_commute", "(x::real) * (y * z) = y * (x * z)"),
1.82 + ("rmult_assoc", "(m::real) * n * k = m * (n * k)"),
1.83 + ("risolate_bdv_add", "((k::real) + bdv = m) = (bdv = m + (-1)*k)"),
1.84 + ("risolate_bdv_mult_add", "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"),
1.85 + ("risolate_bdv_mult", "((n::real) * bdv = m) = (bdv = m / n)"),
1.86 + ("rnorm_equation_add", "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"),
1.87 + ("root_ge0", "0 <= a ==> 0 <= sqrt a"),
1.88 + ("root_add_ge0", "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"),
1.89 + ("root_ge0_1", "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"),
1.90 + ("root_ge0_2", "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"),
1.91 + ("rroot_square_inv", "(sqrt a)^^^ 2 = a"),
1.92 + ("rroot_times_root", "sqrt a * sqrt b = sqrt(a*b)"),
1.93 + ("rroot_times_root_assoc", "(a * sqrt b) * sqrt c = a * sqrt(b*c)"),
1.94 + ("rroot_times_root_assoc_p", "sqrt b * (sqrt c * a)= sqrt(b*c) * a"),
1.95 + ("square_equation_left", "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"),
1.96 + ("square_equation_right", "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"),
1.97 + ("square_equation", "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"),
1.98 + ("risolate_root_add", "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"),
1.99 + ("risolate_root_mult", "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"),
1.100 + ("risolate_root_div", "(a * sqrt c = d) = ( sqrt c = d / a)"),
1.101 + ("mult_square", "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"),
1.102 + ("constant_square", "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"),
1.103 + ("constant_mult_square", "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"),
1.104 + ("square_equality", "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"),
1.105 + ("square_equality_0", "(x^^^2 = 0) = (x = 0)"),
1.106 + ("rroot_to_lhs", "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"),
1.107 + ("rroot_to_lhs_mult", "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"),
1.108 + ("rroot_to_lhs_add_mult", "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)")]
1.109 +
1.110 +|> IsarThy.end_theory;
1.111 +
1.112 +val _ = context thy;
1.113 +
1.114 +
1.115 +val radd_mult_distrib2 = PureThy.get_thm thy "radd_mult_distrib2";
1.116 +val rdistr_right_assoc = PureThy.get_thm thy "rdistr_right_assoc";
1.117 +val rdistr_right_assoc_p = PureThy.get_thm thy "rdistr_right_assoc_p";
1.118 +val rdistr_div_right = PureThy.get_thm thy "rdistr_div_right";
1.119 +val rcollect_right = PureThy.get_thm thy "rcollect_right";
1.120 +val rcollect_one_left = PureThy.get_thm thy "rcollect_one_left";
1.121 +val rcollect_one_left_assoc = PureThy.get_thm thy "rcollect_one_left_assoc";
1.122 +val rcollect_one_left_assoc_p = PureThy.get_thm thy "rcollect_one_left_assoc_p";
1.123 +val rtwo_of_the_same = PureThy.get_thm thy "rtwo_of_the_same";
1.124 +val rtwo_of_the_same_assoc = PureThy.get_thm thy "rtwo_of_the_same_assoc";
1.125 +val rtwo_of_the_same_assoc_p = PureThy.get_thm thy "rtwo_of_the_same_assoc_p";
1.126 +val rcancel_den = PureThy.get_thm thy "rcancel_den";
1.127 +val rcancel_const = PureThy.get_thm thy "rcancel_const";
1.128 +val rshift_nominator = PureThy.get_thm thy "rshift_nominator";
1.129 +val exp_pow = PureThy.get_thm thy "exp_pow";
1.130 +val rsqare = PureThy.get_thm thy "rsqare";
1.131 +val power_1 = PureThy.get_thm thy "power_1";
1.132 +val rbinom_power_2 = PureThy.get_thm thy "rbinom_power_2";
1.133 +val rmult_1 = PureThy.get_thm thy "rmult_1";
1.134 +val rmult_1_right = PureThy.get_thm thy "rmult_1_right";
1.135 +val rmult_0 = PureThy.get_thm thy "rmult_0";
1.136 +val rmult_0_right = PureThy.get_thm thy "rmult_0_right";
1.137 +val radd_0 = PureThy.get_thm thy "radd_0";
1.138 +val radd_0_right = PureThy.get_thm thy "radd_0_right";
1.139 +val radd_real_const_eq = PureThy.get_thm thy "radd_real_const_eq";
1.140 +val radd_real_const = PureThy.get_thm thy "radd_real_const";
1.141 +val radd_commute = PureThy.get_thm thy "radd_commute";
1.142 +val radd_left_commute = PureThy.get_thm thy "radd_left_commute";
1.143 +val radd_assoc = PureThy.get_thm thy "radd_assoc";
1.144 +val rmult_commute = PureThy.get_thm thy "rmult_commute";
1.145 +val rmult_left_commute = PureThy.get_thm thy "rmult_left_commute";
1.146 +val rmult_assoc = PureThy.get_thm thy "rmult_assoc";
1.147 +val risolate_bdv_add = PureThy.get_thm thy "risolate_bdv_add";
1.148 +val risolate_bdv_mult_add = PureThy.get_thm thy "risolate_bdv_mult_add";
1.149 +val risolate_bdv_mult = PureThy.get_thm thy "risolate_bdv_mult";
1.150 +val rnorm_equation_add = PureThy.get_thm thy "rnorm_equation_add";
1.151 +val root_ge0 = PureThy.get_thm thy "root_ge0";
1.152 +val root_add_ge0 = PureThy.get_thm thy "root_add_ge0";
1.153 +val root_ge0_1 = PureThy.get_thm thy "root_ge0_1";
1.154 +val root_ge0_2 = PureThy.get_thm thy "root_ge0_2";
1.155 +val rroot_square_inv = PureThy.get_thm thy "rroot_square_inv";
1.156 +val rroot_times_root = PureThy.get_thm thy "rroot_times_root";
1.157 +val rroot_times_root_assoc = PureThy.get_thm thy "rroot_times_root_assoc";
1.158 +val rroot_times_root_assoc_p = PureThy.get_thm thy "rroot_times_root_assoc_p";
1.159 +val square_equation_left = PureThy.get_thm thy "square_equation_left";
1.160 +val square_equation_right = PureThy.get_thm thy "square_equation_right";
1.161 +val square_equation = PureThy.get_thm thy "square_equation";
1.162 +val risolate_root_add = PureThy.get_thm thy "risolate_root_add";
1.163 +val risolate_root_mult = PureThy.get_thm thy "risolate_root_mult";
1.164 +val risolate_root_div = PureThy.get_thm thy "risolate_root_div";
1.165 +val mult_square = PureThy.get_thm thy "mult_square";
1.166 +val constant_square = PureThy.get_thm thy "constant_square";
1.167 +val constant_mult_square = PureThy.get_thm thy "constant_mult_square";
1.168 +val square_equality = PureThy.get_thm thy "square_equality";
1.169 +val square_equality_0 = PureThy.get_thm thy "square_equality_0";
1.170 +val rroot_to_lhs = PureThy.get_thm thy "rroot_to_lhs";
1.171 +val rroot_to_lhs_mult = PureThy.get_thm thy "rroot_to_lhs_mult";
1.172 +val rroot_to_lhs_add_mult = PureThy.get_thm thy "rroot_to_lhs_add_mult";
1.173 +
1.174 +end;
1.175 +end;
1.176 +
1.177 +open Test;