1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/Scripts/ListG.ML Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,51 @@
1.4 +(* use"Isa99/ListG.ML";
1.5 + W.N. 8.01
1.6 +*)
1.7 +
1.8 +
1.9 +
1.10 +theory' := overwritel (!theory',
1.11 + [("ListG.thy",ListG.thy)]);
1.12 +(*rule set for listexpr in scripts:
1.13 + in knowledge/interface_ME_ISA.sml .. needs eval_binop from Atools.ML
1.14 +*)
1.15 +theorem' := overwritel (!theorem',
1.16 + [("length_Cons_",num_str length_Cons_),
1.17 +(* ("",num_str ),
1.18 + ("",num_str ),
1.19 + ("",num_str ),
1.20 + ("",num_str ),
1.21 +*)
1.22 + ("length_Nil_",num_str length_Nil_)]);
1.23 +
1.24 +(*Length; could be done on the object-level*)
1.25 +(*("Length",("Tools.Length",eval_Length "#Length_")):calc*)
1.26 +fun eval_Length (thmid:string) (op_:string)
1.27 + (t as (Const(op0,t0) $ arg)) thy =
1.28 + let
1.29 + val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
1.30 + val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
1.31 + in Some (thmId, Trueprop $ (mk_equality (t,t'))) end
1.32 + | eval_Length _ _ _ _ = None;
1.33 +
1.34 +(*Nth; could be done on the object-level*)
1.35 +(*("Nth" ,("Tools.Nth",eval_Nth "#Nth_")):calc*)
1.36 +fun eval_Nth (thmid:string) (op_:string)
1.37 + (t as (Const (op0,t0) $ t1 $ t2 )) thy =
1.38 + if is_num t1 andalso is_list t2
1.39 + then
1.40 + (let
1.41 + val t' = (nth (num_of_term t1) (isalist2list t2))
1.42 + val thmId = thmid^(Sign.string_of_term (sign_of thy) t1)^
1.43 + "_"^(Sign.string_of_term (sign_of thy) t2)^
1.44 + " = "^(Sign.string_of_term (sign_of thy) t');
1.45 + in Some (thmId, Trueprop $ (mk_equality (t,t'))) end)
1.46 + handle _ => None (*31.8.01: strange??*)
1.47 + else None
1.48 + | eval_Nth _ _ _ _ = None;
1.49 +
1.50 +(*19.9.02----------------------------
1.51 +calc_list:= overwritel (! calc_list,
1.52 + [
1.53 + ]);
1.54 +-------------------------------------*)
1.55 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/Scripts/ListG.thy Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,130 @@
2.4 +(* use_thy_only"Isa99/ListG";
2.5 + use_thy"Isa99/ListG";
2.6 + W.N. 8.01
2.7 + attaches identifiers to definition of listfuns,
2.8 + for storing them in list_rls
2.9 +*)
2.10 +
2.11 +ListG = Real +
2.12 +
2.13 +consts (*'nat' in List.thy replaced by 'real'*)
2.14 + length_ :: 'a list => real
2.15 +(*-----
2.16 + nth_ :: ['a list, real] => 'a
2.17 + list_update_ :: 'a list => real => 'a => 'a list
2.18 + take_, drop_ :: [real, 'a list] => 'a list
2.19 + upt_ :: real => real => real list ("(1[_../_'(])")
2.20 + replicate_ :: real => 'a => 'a list
2.21 +-----*)
2.22 + Length :: 'a list => real (*DONT USE!!! 18.9.02:check testexpls*)
2.23 + Nth :: [real, 'a list] => 'a (*take nth_ instead, DONT USE!!!*)
2.24 + del :: "['a list, 'a] => 'a list"
2.25 +
2.26 +primrec
2.27 + length_Nil_ "length_ [] = 0" (*length: 'a list => nat*)
2.28 + length_Cons_ "length_ (x#xs) = 1 + length_ xs"
2.29 +
2.30 + primrec
2.31 + del_base "del [] x = []"
2.32 + del_rec "del (y#ys) x = (if x = y then ys else y#(del ys x))"
2.33 +
2.34 +constdefs
2.35 +
2.36 + list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *)
2.37 + ("(_ --/ _)" [66, 66] 65) "a -- b == foldl del a b"
2.38 +
2.39 +consts
2.40 +
2.41 + DropWhile :: "('a => bool) => 'a list => 'a list" (*DONT USE!!!*)
2.42 + primrec
2.43 + DropWhile_base "DropWhile P [] = []"
2.44 + DropWhile_rec "DropWhile P (x#xs) = (if P x then DropWhile P xs else x#xs)"
2.45 +
2.46 +(*-----
2.47 +primrec
2.48 + hdNil "hd([]) = arbitrary"
2.49 + hdCons "hd(x#xs) = x"
2.50 +primrec
2.51 + tlNil "tl([]) = []"
2.52 + tlrCons "tl(x#xs) = xs"
2.53 +primrec
2.54 + lastNil "last [] = arbitrary"
2.55 + lastCons "last(x#xs) = (if xs=[] then x else last xs)"
2.56 +primrec
2.57 + butlastNil "butlast [] = []"
2.58 + butlastCons "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
2.59 +primrec
2.60 + memNil "x mem [] = False"
2.61 + memCons "x mem (y#ys) = (if y=x then True else x mem ys)"
2.62 +primrec
2.63 + setNil "set [] = {}"
2.64 + setCons "set (x#xs) = insert x (set xs)"
2.65 +primrec
2.66 + list_all_Nil "list_all P [] = True"
2.67 + list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
2.68 +primrec
2.69 + mapNil "map f [] = []"
2.70 + mapCons "map f (x#xs) = f(x)#map f xs"
2.71 +primrec
2.72 + append_Nil "[] @ys = ys"
2.73 + append_Cons "(x#xs)@ys = x#(xs@ys)"
2.74 +primrec
2.75 + revNil "rev([]) = []"
2.76 + revCons "rev(x#xs) = rev(xs) @ [x]"
2.77 +primrec
2.78 + filterNil "filter P [] = []"
2.79 + filterCons "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
2.80 +primrec
2.81 + foldl_Nil "foldl f a [] = a"
2.82 + foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
2.83 +primrec
2.84 + concatNil "concat([]) = []"
2.85 + concatCons "concat(x#xs) = x @ concat(xs)"
2.86 +primrec
2.87 + drop_Nil "drop n [] = []"
2.88 + drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
2.89 + (* Warning: simpset does not contain this definition but separate theorems
2.90 + for n=0 / n=Suc k*)
2.91 +primrec
2.92 + take_Nil "take'_ n [] = []"
2.93 + take_Cons "take'_ n (x#xs) = (case n of 0 => [] | Suc(m) => x # take'_ m xs)"
2.94 + (* Warning: simpset does not contain this definition but separate theorems
2.95 + for n=0 / n=Suc k*)
2.96 +primrec
2.97 + nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
2.98 + (* Warning: simpset does not contain this definition but separate theorems
2.99 + for n=0 / n=Suc k*)
2.100 +(*
2.101 +primrec
2.102 + " [][i:=v] = []"
2.103 + "(x#xs)[i:=v] = (case i of 0 => v # xs
2.104 + | Suc j => x # xs[j:=v])"
2.105 +*)
2.106 +primrec
2.107 + takeWhileNil "takeWhile P [] = []"
2.108 + takeWhileCons "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
2.109 +primrec
2.110 + dropWhileNil "dropWhile P [] = []"
2.111 + dropWhileCons "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
2.112 +primrec
2.113 + zipNil "zip xs [] = []"
2.114 + zipCons "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
2.115 + (* Warning: simpset does not contain this definition but separate theorems
2.116 + for xs=[] / xs=z#zs *)
2.117 +(*
2.118 +primrec
2.119 + "[i..0(] = []"
2.120 + "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
2.121 +*)
2.122 +primrec
2.123 + nodupsNil "nodups [] = True"
2.124 + nodupsCons "nodups (x#xs) = (x ~: set xs & nodups xs)"
2.125 +primrec
2.126 + remdupsNil "remdups [] = []"
2.127 + remdupsCons "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
2.128 +primrec
2.129 + replicate_0 "replicate 0 x = []"
2.130 + replicate_Suc "replicate (Suc n) x = x # replicate n x"
2.131 +
2.132 +-----*)
2.133 +end
2.134 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/Scripts/Real2002-theorems.sml Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,993 @@
3.4 +(*
3.5 + cd ~/Isabelle2002/src/HOL/Real
3.6 + grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml
3.7 + WN 9.8.02
3.8 +
3.9 +ML> thy;
3.10 +val it =
3.11 + {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type,
3.12 + Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion,
3.13 + NatDef, Nat, NatArith, Divides, Power, SetInterval, Finite_Set, Equiv,
3.14 + IntDef, Int, Datatype_Universe, Datatype, Numeral, Bin, IntArith,
3.15 + Wellfounded_Relations, Recdef, IntDiv, IntPower, NatBin, NatSimprocs,
3.16 + Relation_Power, PreList, List, Map, Hilbert_Choice, Main, Lubs, PNat, PRat,
3.17 + PReal, RealDef, RealOrd, RealInt, RealBin, RealArith0, RealArith,
3.18 + RComplete, RealAbs, RealPow, Ring_and_Field, Complex_Numbers, Real}
3.19 + : theory
3.20 +
3.21 +theories with their respective theorems found by
3.22 +grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml;
3.23 +theories listed in the the order as found in Real.thy above
3.24 +
3.25 +comments
3.26 + (**)"...theorem..." : first choice for one of the rule-sets
3.27 + "...theorem..."(*??*): to be investigated
3.28 + "...theorem... : just for documenting the contents
3.29 +*)
3.30 +
3.31 +Lubs.ML:qed -----------------------------------------------------------------
3.32 + "setleI"; "ALL y::?'a:?S::?'a set. y <= (?x::?'a) ==> ?S *<= ?x"
3.33 + "setleD"; "[| (?S::?'a set) *<= (?x::?'a); (?y::?'a) : ?S |] ==> ?y <= ?x"
3.34 + "setgeI"; "Ball (?S::?'a set) (op <= (?x::?'a)) ==> ?x <=* ?S"
3.35 + "setgeD"; "[| (?x::?'a) <=* (?S::?'a set); (?y::?'a) : ?S |] ==> ?x <= ?y"
3.36 + "leastPD1";
3.37 + "leastPD2";
3.38 + "leastPD3";
3.39 + "isLubD1";
3.40 + "isLubD1a";
3.41 + "isLub_isUb";
3.42 + "isLubD2";
3.43 + "isLubD3";
3.44 + "isLubI1";
3.45 + "isLubI2";
3.46 + "isUbD";
3.47 + "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |]
3.48 + ==> ?y <= ?x" "isUbD2";
3.49 + "isUbD2a";
3.50 + "isUbI";
3.51 + "isLub_le_isUb";
3.52 + "isLub_ubs";
3.53 +PNat.ML:qed ------------------------------------------------------------------
3.54 + "pnat_fun_mono"; "mono (%X::nat set. {Suc (0::nat)} Un Suc ` X)"
3.55 + "one_RepI"; "Suc (0::nat) : pnat"
3.56 + "pnat_Suc_RepI";
3.57 + "two_RepI";
3.58 + "PNat_induct";
3.59 + "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat));
3.60 + !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i"
3.61 + "pnat_induct";
3.62 + "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |]
3.63 + ==> ?P (?n::pnat)"
3.64 + "pnat_diff_induct";
3.65 + "pnatE";
3.66 + "inj_on_Abs_pnat";
3.67 + "inj_Rep_pnat";
3.68 + "zero_not_mem_pnat";
3.69 + "mem_pnat_gt_zero";
3.70 + "gt_0_mem_pnat";
3.71 + "mem_pnat_gt_0_iff";
3.72 + "Rep_pnat_gt_zero";
3.73 + "pnat_add_commute"; "(?x::pnat) + (?y::pnat) = ?y + ?x"
3.74 + "Collect_pnat_gt_0";
3.75 + "pSuc_not_one";
3.76 + "inj_pSuc";
3.77 + "pSuc_pSuc_eq";
3.78 + "n_not_pSuc_n";
3.79 + "not1_implies_pSuc";
3.80 + "pSuc_is_plus_one";
3.81 + "sum_Rep_pnat";
3.82 + "sum_Rep_pnat_sum";
3.83 + "pnat_add_assoc";
3.84 + "pnat_add_left_commute";
3.85 + "pnat_add_left_cancel";
3.86 + "pnat_add_right_cancel";
3.87 + "pnat_no_add_ident";
3.88 + "pnat_less_not_refl";
3.89 + "pnat_less_not_refl2";
3.90 + "Rep_pnat_not_less0";
3.91 + "Rep_pnat_not_less_one";
3.92 + "Rep_pnat_gt_implies_not0";
3.93 + "pnat_less_linear";
3.94 + "Rep_pnat_le_one";
3.95 + "lemma_less_ex_sum_Rep_pnat";
3.96 + "pnat_le_iff_Rep_pnat_le";
3.97 + "pnat_add_left_cancel_le";
3.98 + "pnat_add_left_cancel_less";
3.99 + "pnat_add_lessD1";
3.100 + "pnat_not_add_less1";
3.101 + "pnat_not_add_less2";
3.102 +PNat.ML:qed_spec_mp
3.103 + "pnat_add_leD1";
3.104 + "pnat_add_leD2";
3.105 +PNat.ML:qed
3.106 + "pnat_less_add_eq_less";
3.107 + "pnat_less_iff";
3.108 + "pnat_linear_Ex_eq";
3.109 + "pnat_eq_lessI";
3.110 + "Rep_pnat_mult_1";
3.111 + "Rep_pnat_mult_1_right";
3.112 + "mult_Rep_pnat";
3.113 + "mult_Rep_pnat_mult";
3.114 + "pnat_mult_commute"; "(?m::pnat) * (?n::pnat) = ?n * ?m"
3.115 + "pnat_add_mult_distrib";
3.116 + "pnat_add_mult_distrib2";
3.117 + "pnat_mult_assoc";
3.118 + "pnat_mult_left_commute";
3.119 + "pnat_mult_1";
3.120 + "pnat_mult_1_left";
3.121 + "pnat_mult_less_mono2";
3.122 + "pnat_mult_less_mono1";
3.123 + "pnat_mult_less_cancel2";
3.124 + "pnat_mult_less_cancel1";
3.125 + "pnat_mult_cancel2";
3.126 + "pnat_mult_cancel1";
3.127 + "pnat_same_multI2";
3.128 + "eq_Abs_pnat";
3.129 + "pnat_one_iff";
3.130 + "pnat_two_eq";
3.131 + "inj_pnat_of_nat";
3.132 + "nat_add_one_less";
3.133 + "nat_add_one_less1";
3.134 + "pnat_of_nat_add";
3.135 + "pnat_of_nat_less_iff";
3.136 + "pnat_of_nat_mult";
3.137 +PRat.ML:qed ------------------------------------------------------------------
3.138 + "prat_trans_lemma";
3.139 + "[| (?x1.0::pnat) * (?y2.0::pnat) = (?x2.0::pnat) * (?y1.0::pnat);
3.140 + ?x2.0 * (?y3.0::pnat) = (?x3.0::pnat) * ?y2.0 |]
3.141 + ==> ?x1.0 * ?y3.0 = ?x3.0 * ?y1.0"
3.142 + "ratrel_iff";
3.143 + "ratrelI";
3.144 + "ratrelE_lemma";
3.145 + "ratrelE";
3.146 + "ratrel_refl";
3.147 + "equiv_ratrel";
3.148 + "ratrel_in_prat";
3.149 + "inj_on_Abs_prat";
3.150 + "inj_Rep_prat";
3.151 + "inj_prat_of_pnat";
3.152 + "eq_Abs_prat";
3.153 + "qinv_congruent";
3.154 + "qinv";
3.155 + "qinv_qinv";
3.156 + "inj_qinv";
3.157 + "qinv_1";
3.158 + "prat_add_congruent2_lemma";
3.159 + "prat_add_congruent2";
3.160 + "prat_add";
3.161 + "prat_add_commute";
3.162 + "prat_add_assoc";
3.163 + "prat_add_left_commute";
3.164 + "pnat_mult_congruent2";
3.165 + "prat_mult";
3.166 + "prat_mult_commute";
3.167 + "prat_mult_assoc";
3.168 + "prat_mult_left_commute";
3.169 + "prat_mult_1";
3.170 + "prat_mult_1_right";
3.171 + "prat_of_pnat_add";
3.172 + "prat_of_pnat_mult";
3.173 + "prat_mult_qinv";
3.174 + "prat_mult_qinv_right";
3.175 + "prat_qinv_ex";
3.176 + "prat_qinv_ex1";
3.177 + "prat_qinv_left_ex1";
3.178 + "prat_mult_inv_qinv";
3.179 + "prat_as_inverse_ex";
3.180 + "qinv_mult_eq";
3.181 + "prat_add_mult_distrib";
3.182 + "prat_add_mult_distrib2";
3.183 + "prat_less_iff";
3.184 + "prat_lessI";
3.185 + "prat_lessE_lemma";
3.186 + "prat_lessE";
3.187 + "prat_less_trans";
3.188 + "prat_less_not_refl";
3.189 + "prat_less_not_sym";
3.190 + "lemma_prat_dense";
3.191 + "prat_lemma_dense";
3.192 + "prat_dense";
3.193 + "prat_add_less2_mono1";
3.194 + "prat_add_less2_mono2";
3.195 + "prat_mult_less2_mono1";
3.196 + "prat_mult_left_less2_mono1";
3.197 + "lemma_prat_add_mult_mono";
3.198 + "qless_Ex";
3.199 + "lemma_prat_less_linear";
3.200 + "prat_linear";
3.201 + "prat_linear_less2";
3.202 + "lemma1_qinv_prat_less";
3.203 + "lemma2_qinv_prat_less";
3.204 + "qinv_prat_less";
3.205 + "prat_qinv_gt_1";
3.206 + "prat_qinv_is_gt_1";
3.207 + "prat_less_1_2";
3.208 + "prat_less_qinv_2_1";
3.209 + "prat_mult_qinv_less_1";
3.210 + "prat_self_less_add_self";
3.211 + "prat_self_less_add_right";
3.212 + "prat_self_less_add_left";
3.213 + "prat_self_less_mult_right";
3.214 + "prat_leI";
3.215 + "prat_leD";
3.216 + "prat_less_le_iff";
3.217 + "not_prat_leE";
3.218 + "prat_less_imp_le";
3.219 + "prat_le_imp_less_or_eq";
3.220 + "prat_less_or_eq_imp_le";
3.221 + "prat_le_eq_less_or_eq";
3.222 + "prat_le_refl";
3.223 + "prat_le_less_trans";
3.224 + "prat_le_trans";
3.225 + "not_less_not_eq_prat_less";
3.226 + "prat_add_less_mono";
3.227 + "prat_mult_less_mono";
3.228 + "prat_mult_left_le2_mono1";
3.229 + "prat_mult_le2_mono1";
3.230 + "qinv_prat_le";
3.231 + "prat_add_left_le2_mono1";
3.232 + "prat_add_le2_mono1";
3.233 + "prat_add_le_mono";
3.234 + "prat_add_right_less_cancel";
3.235 + "prat_add_left_less_cancel";
3.236 + "Abs_prat_mult_qinv";
3.237 + "lemma_Abs_prat_le1";
3.238 + "lemma_Abs_prat_le2";
3.239 + "lemma_Abs_prat_le3";
3.240 + "pre_lemma_gleason9_34";
3.241 + "pre_lemma_gleason9_34b";
3.242 + "prat_of_pnat_less_iff";
3.243 + "lemma_prat_less_1_memEx";
3.244 + "lemma_prat_less_1_set_non_empty";
3.245 + "empty_set_psubset_lemma_prat_less_1_set";
3.246 + "lemma_prat_less_1_not_memEx";
3.247 + "lemma_prat_less_1_set_not_rat_set";
3.248 + "lemma_prat_less_1_set_psubset_rat_set";
3.249 + "preal_1";
3.250 + "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))}
3.251 + : {A::prat set.
3.252 + {} < A &
3.253 + A < UNIV &
3.254 + (ALL y::prat:A. (ALL z::prat. z < y --> z : A) & Bex A (op < y))}"
3.255 +PReal.ML:qed -----------------------------------------------------------------
3.256 + "inj_on_Abs_preal"; "inj_on Abs_preal preal"
3.257 + "inj_Rep_preal";
3.258 + "empty_not_mem_preal";
3.259 + "one_set_mem_preal";
3.260 + "preal_psubset_empty";
3.261 + "Rep_preal_psubset_empty";
3.262 + "mem_Rep_preal_Ex";
3.263 + "prealI1";
3.264 + "[| {} < (?A::prat set); ?A < UNIV;
3.265 + ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |]
3.266 + ==> ?A : preal"
3.267 + "prealI2";
3.268 + "prealE_lemma";
3.269 + "prealE_lemma1";
3.270 + "prealE_lemma2";
3.271 + "prealE_lemma3";
3.272 + "prealE_lemma3a";
3.273 + "prealE_lemma3b";
3.274 + "prealE_lemma4";
3.275 + "prealE_lemma4a";
3.276 + "not_mem_Rep_preal_Ex";
3.277 + "lemma_prat_less_set_mem_preal";
3.278 + "lemma_prat_set_eq";
3.279 + "inj_preal_of_prat";
3.280 + "not_in_preal_ub";
3.281 + "preal_less_not_refl";
3.282 + "preal_not_refl2";
3.283 + "preal_less_trans";
3.284 + "preal_less_not_sym";
3.285 + "preal_linear";
3.286 + "(?r1.0::preal) < (?r2.0::preal) | ?r1.0 = ?r2.0 | ?r2.0 < ?r1.0"
3.287 + "preal_linear_less2";
3.288 + "preal_add_commute"; "(?x::preal) + (?y::preal) = ?y + ?x"
3.289 + "preal_add_set_not_empty";
3.290 + "preal_not_mem_add_set_Ex";
3.291 + "preal_add_set_not_prat_set";
3.292 + "preal_add_set_lemma3";
3.293 + "preal_add_set_lemma4";
3.294 + "preal_mem_add_set";
3.295 + "preal_add_assoc";
3.296 + "preal_add_left_commute";
3.297 + "preal_mult_commute"; "(?x::preal) * (?y::preal) = ?y * ?x"
3.298 + "preal_mult_set_not_empty";
3.299 + "preal_not_mem_mult_set_Ex";
3.300 + "preal_mult_set_not_prat_set";
3.301 + "preal_mult_set_lemma3";
3.302 + "preal_mult_set_lemma4";
3.303 + "preal_mem_mult_set";
3.304 + "preal_mult_assoc";
3.305 + "preal_mult_left_commute";
3.306 + "preal_mult_1";
3.307 + "preal_mult_1_right";
3.308 + "preal_add_assoc_cong";
3.309 + "preal_add_assoc_swap";
3.310 + "mem_Rep_preal_addD";
3.311 + "mem_Rep_preal_addI";
3.312 + "mem_Rep_preal_add_iff";
3.313 + "mem_Rep_preal_multD";
3.314 + "mem_Rep_preal_multI";
3.315 + "mem_Rep_preal_mult_iff";
3.316 + "lemma_add_mult_mem_Rep_preal";
3.317 + "lemma_add_mult_mem_Rep_preal1";
3.318 + "lemma_preal_add_mult_distrib";
3.319 + "lemma_preal_add_mult_distrib2";
3.320 + "preal_add_mult_distrib2";
3.321 + "preal_add_mult_distrib";
3.322 + "qinv_not_mem_Rep_preal_Ex";
3.323 + "lemma_preal_mem_inv_set_ex";
3.324 + "preal_inv_set_not_empty";
3.325 + "qinv_mem_Rep_preal_Ex";
3.326 + "preal_not_mem_inv_set_Ex";
3.327 + "preal_inv_set_not_prat_set";
3.328 + "preal_inv_set_lemma3";
3.329 + "preal_inv_set_lemma4";
3.330 + "preal_mem_inv_set";
3.331 + "preal_mem_mult_invD";
3.332 + "lemma1_gleason9_34";
3.333 + "lemma1b_gleason9_34";
3.334 + "lemma_gleason9_34a";
3.335 + "lemma_gleason9_34";
3.336 + "lemma1_gleason9_36";
3.337 + "lemma2_gleason9_36";
3.338 + "lemma_gleason9_36";
3.339 + "lemma_gleason9_36a";
3.340 + "preal_mem_mult_invI";
3.341 + "preal_mult_inv";
3.342 + "preal_mult_inv_right";
3.343 + "eq_Abs_preal";
3.344 + "Rep_preal_self_subset";
3.345 + "Rep_preal_sum_not_subset";
3.346 + "Rep_preal_sum_not_eq";
3.347 + "preal_self_less_add_left";
3.348 + "preal_self_less_add_right";
3.349 + "preal_leD";
3.350 + "not_preal_leE";
3.351 + "preal_leI";
3.352 + "preal_less_le_iff";
3.353 + "preal_less_imp_le";
3.354 + "preal_le_imp_less_or_eq";
3.355 + "preal_less_or_eq_imp_le";
3.356 + "preal_le_refl";
3.357 + "preal_le_trans";
3.358 + "preal_le_anti_sym";
3.359 + "preal_neq_iff";
3.360 + "preal_less_le";
3.361 + "lemma_psubset_mem";
3.362 + "lemma_psubset_not_refl";
3.363 + "psubset_trans";
3.364 + "subset_psubset_trans";
3.365 + "subset_psubset_trans2";
3.366 + "psubsetD";
3.367 + "lemma_ex_mem_less_left_add1";
3.368 + "preal_less_set_not_empty";
3.369 + "lemma_ex_not_mem_less_left_add1";
3.370 + "preal_less_set_not_prat_set";
3.371 + "preal_less_set_lemma3";
3.372 + "preal_less_set_lemma4";
3.373 + "preal_mem_less_set";
3.374 + "preal_less_add_left_subsetI";
3.375 + "lemma_sum_mem_Rep_preal_ex";
3.376 + "preal_less_add_left_subsetI2";
3.377 + "preal_less_add_left";
3.378 + "preal_less_add_left_Ex";
3.379 + "preal_add_less2_mono1";
3.380 + "preal_add_less2_mono2";
3.381 + "preal_mult_less_mono1";
3.382 + "preal_mult_left_less_mono1";
3.383 + "preal_mult_left_le_mono1";
3.384 + "preal_mult_le_mono1";
3.385 + "preal_add_left_le_mono1";
3.386 + "preal_add_le_mono1";
3.387 + "preal_add_right_less_cancel";
3.388 + "preal_add_left_less_cancel";
3.389 + "preal_add_less_iff1";
3.390 + "preal_add_less_iff2";
3.391 + "preal_add_less_mono";
3.392 + "preal_mult_less_mono";
3.393 + "preal_add_right_cancel";
3.394 + "preal_add_left_cancel";
3.395 + "preal_add_left_cancel_iff";
3.396 + "preal_add_right_cancel_iff";
3.397 + "preal_sup_mem_Ex";
3.398 + "preal_sup_set_not_empty";
3.399 + "preal_sup_not_mem_Ex";
3.400 + "preal_sup_not_mem_Ex1";
3.401 + "preal_sup_set_not_prat_set";
3.402 + "preal_sup_set_not_prat_set1";
3.403 + "preal_sup_set_lemma3";
3.404 + "preal_sup_set_lemma3_1";
3.405 + "preal_sup_set_lemma4";
3.406 + "preal_sup_set_lemma4_1";
3.407 + "preal_sup";
3.408 + "preal_sup1";
3.409 + "preal_psup_leI";
3.410 + "preal_psup_leI2";
3.411 + "preal_psup_leI2b";
3.412 + "preal_psup_leI2a";
3.413 + "psup_le_ub";
3.414 + "psup_le_ub1";
3.415 + "preal_complete";
3.416 + "lemma_preal_rat_less";
3.417 + "lemma_preal_rat_less2";
3.418 + "preal_of_prat_add";
3.419 + "lemma_preal_rat_less3";
3.420 + "lemma_preal_rat_less4";
3.421 + "preal_of_prat_mult";
3.422 + "preal_of_prat_less_iff"; "(preal_of_prat ?p < preal_of_prat ?q) = (?p < ?q)"
3.423 +RealDef.ML:qed ---------------------------------------------------------------
3.424 + "preal_trans_lemma";
3.425 + "realrel_iff";
3.426 + "realrelI";
3.427 + "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel"
3.428 + "realrelE_lemma";
3.429 + "realrelE";
3.430 + "realrel_refl";
3.431 + "equiv_realrel";
3.432 + "realrel_in_real";
3.433 + "inj_on_Abs_REAL";
3.434 + "inj_Rep_REAL";
3.435 + "inj_real_of_preal";
3.436 + "eq_Abs_REAL";
3.437 + "real_minus_congruent";
3.438 + "real_minus";
3.439 + "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})"
3.440 + "real_minus_minus"; (**)"- (- (?z::real)) = ?z"
3.441 + "inj_real_minus"; "inj uminus"
3.442 + "real_minus_zero"; (**)"- 0 = 0"
3.443 + "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)"
3.444 + "real_add_congruent2";
3.445 + "congruent2 realrel
3.446 + (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)"
3.447 + "real_add";
3.448 + "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) +
3.449 + Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
3.450 + Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})"
3.451 + "real_add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
3.452 + "real_add_assoc"; (**)
3.453 + "real_add_left_commute"; (**)
3.454 + "real_add_zero_left"; (**)"0 + ?z = ?z"
3.455 + "real_add_zero_right"; (**)
3.456 + "real_add_minus"; (**)"?z + - ?z = 0"
3.457 + "real_add_minus_left"; (**)
3.458 + "real_add_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
3.459 + "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w"
3.460 + "real_minus_ex"; "EX y. ?x + y = 0"
3.461 + "real_minus_ex1";
3.462 + "real_minus_left_ex1"; "EX! y. y + ?x = 0"
3.463 + "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
3.464 + "real_as_add_inverse_ex"; "EX y. ?x = - y"
3.465 + "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y"
3.466 + "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)"
3.467 + "real_add_right_cancel"; "(?y + ?x = ?z + ?x) = (?y = ?z)"
3.468 + "real_diff_0"; (**)"0 - ?x = - ?x"
3.469 + "real_diff_0_right"; (**)"?x - 0 = ?x"
3.470 + "real_diff_self"; (**)"?x - ?x = 0"
3.471 + "real_mult_congruent2_lemma";
3.472 + "real_mult_congruent2";
3.473 + "congruent2 realrel
3.474 + (%p1 p2.
3.475 + (%(x1, y1).
3.476 + (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)})
3.477 + p2) p1)"
3.478 + "real_mult";
3.479 + "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) *
3.480 + Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
3.481 + Abs_REAL
3.482 + (realrel ``
3.483 + {(?x1.0 * ?x2.0 + ?y1.0 * ?y2.0, ?x1.0 * ?y2.0 + ?x2.0 * ?y1.0)})"
3.484 + "real_mult_commute"; (**)"?z * ?w = ?w * ?z"
3.485 + "real_mult_assoc"; (**)
3.486 + "real_mult_left_commute";
3.487 + (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"
3.488 + "real_mult_1"; (**)"1 * ?z = ?z"
3.489 + "real_mult_1_right"; (**)"?z * 1 = ?z"
3.490 + "real_mult_0"; (**)
3.491 + "real_mult_0_right"; (**)"?z * 0 = 0"
3.492 + "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)"
3.493 + "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)"
3.494 + "real_mult_minus_1"; (**)"- 1 * ?z = - ?z"
3.495 + "real_mult_minus_1_right";(**)"?z * - 1 = - ?z"
3.496 + "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y"
3.497 + "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y"
3.498 + "real_add_assoc_cong";
3.499 + "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)"
3.500 + "real_add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
3.501 + "real_add_mult_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
3.502 + "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
3.503 + "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
3.504 + "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
3.505 + "real_zero_not_eq_one";
3.506 + "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})"
3.507 + "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1"
3.508 + "real_mult_inv_left_ex"; "?x ~= 0 ==> inverse ?x * ?x = 1"
3.509 + "real_mult_inv_left";
3.510 + "real_mult_inv_right"; "?x ~= 0 ==> ?x * inverse ?x = 1"
3.511 + "INVERSE_ZERO"; "inverse 0 = 0"
3.512 + "DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)"?a / 0 = 0"
3.513 + "real_mult_left_cancel"; (**)"?c ~= 0 ==> (?c * ?a = ?c * ?b) = (?a = ?b)"
3.514 + "real_mult_right_cancel"; (**)"?c ~= 0 ==> (?a * ?c = ?b * ?c) = (?a = ?b)"
3.515 + "real_mult_left_cancel_ccontr"; "?c * ?a ~= ?c * ?b ==> ?a ~= ?b"
3.516 + "real_mult_right_cancel_ccontr"; "?a * ?c ~= ?b * ?c ==> ?a ~= ?b"
3.517 + "real_inverse_not_zero"; "?x ~= 0 ==> inverse ?x ~= 0"
3.518 + "real_mult_not_zero"; "[| ?x ~= 0; ?y ~= 0 |] ==> ?x * ?y ~= 0"
3.519 + "real_inverse_inverse"; "inverse (inverse ?x) = ?x"
3.520 + "real_inverse_1"; "inverse 1 = 1"
3.521 + "real_minus_inverse"; "inverse (- ?x) = - inverse ?x"
3.522 + "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y"
3.523 + "real_times_divide1_eq"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
3.524 + "real_times_divide2_eq"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
3.525 + "real_divide_divide1_eq"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
3.526 + "real_divide_divide2_eq"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
3.527 + "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)"
3.528 + "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)"
3.529 + "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
3.530 + "preal_lemma_eq_rev_sum";
3.531 + "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y"
3.532 + "preal_add_left_commute_cancel";
3.533 + "?x + (?b + ?y) = ?x1.0 + (?b + ?y1.0) ==> ?x + ?y = ?x1.0 + ?y1.0"
3.534 + "preal_lemma_for_not_refl";
3.535 + "real_less_not_refl"; "~ ?R < ?R"
3.536 + "real_not_refl2";
3.537 + "preal_lemma_trans";
3.538 + "real_less_trans";
3.539 + "real_less_not_sym";
3.540 + "real_of_preal_add";
3.541 + "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0"
3.542 + "real_of_preal_mult";
3.543 + "real_of_preal_ExI";
3.544 + "real_of_preal_ExD";
3.545 + "real_of_preal_iff";
3.546 + "real_of_preal_trichotomy";
3.547 + "real_of_preal_trichotomyE";
3.548 + "real_of_preal_lessD";
3.549 + "real_of_preal_lessI";
3.550 + "?m1.0 < ?m2.0 ==> real_of_preal ?m1.0 < real_of_preal ?m2.0"
3.551 + "real_of_preal_less_iff1";
3.552 + "real_of_preal_minus_less_self";
3.553 + "real_of_preal_minus_less_zero";
3.554 + "real_of_preal_not_minus_gt_zero";
3.555 + "real_of_preal_zero_less";
3.556 + "real_of_preal_not_less_zero";
3.557 + "real_minus_minus_zero_less";
3.558 + "real_of_preal_sum_zero_less";
3.559 + "real_of_preal_minus_less_all";
3.560 + "real_of_preal_not_minus_gt_all";
3.561 + "real_of_preal_minus_less_rev1";
3.562 + "real_of_preal_minus_less_rev2";
3.563 + "real_of_preal_minus_less_rev_iff";
3.564 + "real_linear"; "?R1.0 < ?R2.0 | ?R1.0 = ?R2.0 | ?R2.0 < ?R1.0"
3.565 + "real_neq_iff";
3.566 + "real_linear_less2";
3.567 + "real_leI";
3.568 + "real_leD"; "~ ?w < ?z ==> ?z <= ?w"
3.569 + "real_less_le_iff";
3.570 + "not_real_leE";
3.571 + "real_le_imp_less_or_eq";
3.572 + "real_less_or_eq_imp_le";
3.573 + "real_le_less";
3.574 + "real_le_refl";
3.575 + "real_le_linear";
3.576 + "real_le_trans"; "[| ?i <= ?j; ?j <= ?k |] ==> ?i <= ?k"
3.577 + "real_le_anti_sym"; "[| ?z <= ?w; ?w <= ?z |] ==> ?z = ?w"
3.578 + "not_less_not_eq_real_less";
3.579 + "real_less_le"; "(?w < ?z) = (?w <= ?z & ?w ~= ?z)"
3.580 + "real_minus_zero_less_iff";
3.581 + "real_minus_zero_less_iff2";
3.582 + "real_less_add_positive_left_Ex";
3.583 + "real_less_sum_gt_zero"; "?W < ?S ==> 0 < ?S + - ?W"
3.584 + "real_lemma_change_eq_subj";
3.585 + "real_sum_gt_zero_less"; "0 < ?S + - ?W ==> ?W < ?S"
3.586 + "real_less_sum_gt_0_iff"; "(0 < ?S + - ?W) = (?W < ?S)"
3.587 + "real_less_eq_diff"; "(?x < ?y) = (?x - ?y < 0)"
3.588 + "real_add_diff_eq"; (**)"?x + (?y - ?z) = ?x + ?y - ?z"
3.589 + "real_diff_add_eq"; (**)"?x - ?y + ?z = ?x + ?z - ?y"
3.590 + "real_diff_diff_eq"; (**)"?x - ?y - ?z = ?x - (?y + ?z)"
3.591 + "real_diff_diff_eq2"; (**)"?x - (?y - ?z) = ?x + ?z - ?y"
3.592 + "real_diff_less_eq"; "(?x - ?y < ?z) = (?x < ?z + ?y)"
3.593 + "real_less_diff_eq";
3.594 + "real_diff_le_eq"; "(?x - ?y <= ?z) = (?x <= ?z + ?y)"
3.595 + "real_le_diff_eq";
3.596 + "real_diff_eq_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
3.597 + "real_eq_diff_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
3.598 + "real_less_eqI";
3.599 + "real_le_eqI";
3.600 + "real_eq_eqI"; "?x - ?y = ?x' - ?y' ==> (?x = ?y) = (?x' = ?y')"
3.601 +RealOrd.ML:qed ---------------------------------------------------------------
3.602 + "real_add_cancel_21"; "(?x + (?y + ?z) = ?y + ?u) = (?x + ?z = ?u)"
3.603 + "real_add_cancel_end"; "(?x + (?y + ?z) = ?y) = (?x = - ?z)"
3.604 + "real_minus_diff_eq"; (*??*)"- (?x - ?y) = ?y - ?x"
3.605 + "real_gt_zero_preal_Ex";
3.606 + "real_gt_preal_preal_Ex";
3.607 + "real_ge_preal_preal_Ex";
3.608 + "real_less_all_preal"; "?y <= 0 ==> ALL x. ?y < real_of_preal x"
3.609 + "real_less_all_real2";
3.610 + "real_lemma_add_positive_imp_less";
3.611 + "real_ex_add_positive_left_less";"EX T. 0 < T & ?R + T = ?S ==> ?R < ?S"
3.612 + "real_less_iff_add";
3.613 + "real_of_preal_le_iff";
3.614 + "real_mult_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x * ?y"
3.615 + "neg_real_mult_order";
3.616 + "real_mult_less_0"; "[| 0 < ?x; ?y < 0 |] ==> ?x * ?y < 0"
3.617 + "real_zero_less_one"; "0 < 1"
3.618 + "real_add_right_cancel_less";
3.619 + "real_add_left_cancel_less";
3.620 + "real_add_right_cancel_le";
3.621 + "real_add_left_cancel_le";
3.622 + "real_add_less_le_mono";
3.623 + "real_add_le_less_mono"; "[| ?w' <= ?w; ?z' < ?z |] ==> ?w' + ?z' < ?w + ?z"
3.624 + "real_add_less_mono2";
3.625 + "real_less_add_right_cancel";
3.626 + "real_less_add_left_cancel"; "?C + ?A < ?C + ?B ==> ?A < ?B"
3.627 + "real_le_add_right_cancel";
3.628 + "real_le_add_left_cancel"; "?C + ?A <= ?C + ?B ==> ?A <= ?B"
3.629 + "real_add_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x + ?y"
3.630 + "real_le_add_order";
3.631 + "real_add_less_mono";
3.632 + "real_add_left_le_mono1";
3.633 + "real_add_le_mono";
3.634 + "real_less_Ex";
3.635 + "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
3.636 + "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)"
3.637 + "real_le_square";
3.638 + "real_of_posnat_one";
3.639 + "real_of_posnat_two";
3.640 + "real_of_posnat_add"; "real_of_posnat ?n1.0 + real_of_posnat ?n2.0 =
3.641 + real_of_posnat (?n1.0 + ?n2.0) + 1"
3.642 + "real_of_posnat_add_one";
3.643 + "real_of_posnat_Suc";
3.644 + "inj_real_of_posnat";
3.645 + "real_of_nat_zero";
3.646 + "real_of_nat_one"; "real (Suc 0) = 1"
3.647 + "real_of_nat_add";
3.648 + "real_of_nat_Suc";
3.649 + "real_of_nat_less_iff";
3.650 + "real_of_nat_le_iff";
3.651 + "inj_real_of_nat";
3.652 + "real_of_nat_ge_zero";
3.653 + "real_of_nat_mult";
3.654 + "real_of_nat_inject";
3.655 +RealOrd.ML:qed_spec_mp
3.656 + "real_of_nat_diff";
3.657 +RealOrd.ML:qed
3.658 + "real_of_nat_zero_iff";
3.659 + "real_of_nat_neg_int";
3.660 + "real_inverse_gt_0";
3.661 + "real_inverse_less_0";
3.662 + "real_mult_less_mono1";
3.663 + "real_mult_less_mono2";
3.664 + "real_mult_less_cancel1";
3.665 + "(?k * ?m < ?k * ?n) = (0 < ?k & ?m < ?n | ?k < 0 & ?n < ?m)"
3.666 + "real_mult_less_cancel2";
3.667 + "real_mult_less_iff1";
3.668 + "real_mult_less_iff2";
3.669 + "real_mult_le_cancel_iff1";
3.670 + "real_mult_le_cancel_iff2";
3.671 + "real_mult_le_less_mono1";
3.672 + "real_mult_less_mono";
3.673 + "real_mult_less_mono'";
3.674 + "real_gt_zero"; "1 <= ?x ==> 0 < ?x"
3.675 + "real_mult_self_le"; "[| 1 < ?r; 1 <= ?x |] ==> ?x <= ?r * ?x"
3.676 + "real_mult_self_le2";
3.677 + "real_inverse_less_swap";
3.678 + "real_mult_is_0";
3.679 + "real_inverse_add";
3.680 + "real_minus_zero_le_iff";
3.681 + "real_minus_zero_le_iff2";
3.682 + "real_sum_squares_cancel"; "?x * ?x + ?y * ?y = 0 ==> ?x = 0"
3.683 + "real_sum_squares_cancel2"; "?x * ?x + ?y * ?y = 0 ==> ?y = 0"
3.684 + "real_0_less_mult_iff";
3.685 + "real_0_le_mult_iff";
3.686 + "real_mult_less_0_iff"; "(?x * ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"
3.687 + "real_mult_le_0_iff";
3.688 +RealInt.ML:qed ---------------------------------------------------------------
3.689 + "real_of_int_congruent";
3.690 + "real_of_int"; "real (Abs_Integ (intrel `` {(?i, ?j)})) =
3.691 + Abs_REAL
3.692 + (realrel ``
3.693 + {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)),
3.694 + preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})"
3.695 + "inj_real_of_int";
3.696 + "real_of_int_zero";
3.697 + "real_of_one";
3.698 + "real_of_int_add"; "real ?x + real ?y = real (?x + ?y)"
3.699 + "real_of_int_minus";
3.700 + "real_of_int_diff";
3.701 + "real_of_int_mult"; "real ?x * real ?y = real (?x * ?y)"
3.702 + "real_of_int_Suc";
3.703 + "real_of_int_real_of_nat";
3.704 + "real_of_nat_real_of_int";
3.705 + "real_of_int_zero_cancel";
3.706 + "real_of_int_less_cancel";
3.707 + "real_of_int_inject";
3.708 + "real_of_int_less_mono";
3.709 + "real_of_int_less_iff";
3.710 + "real_of_int_le_iff";
3.711 +RealBin.ML:qed ---------------------------------------------------------------
3.712 + "real_number_of"; "real (number_of ?w) = number_of ?w"
3.713 + "real_numeral_0_eq_0";
3.714 + "real_numeral_1_eq_1";
3.715 + "add_real_number_of";
3.716 + "minus_real_number_of";
3.717 + "diff_real_number_of";
3.718 + "mult_real_number_of";
3.719 + "real_mult_2"; (**)"2 * ?z = ?z + ?z"
3.720 + "real_mult_2_right"; (**)"?z * 2 = ?z + ?z"
3.721 + "eq_real_number_of";
3.722 + "less_real_number_of";
3.723 + "le_real_number_of_eq_not_less";
3.724 + "real_minus_1_eq_m1"; "- 1 = -1"(*uminus.. = "-.."*)
3.725 + "real_mult_minus1"; (**)"-1 * ?z = - ?z"
3.726 + "real_mult_minus1_right"; (**)"?z * -1 = - ?z"
3.727 + "zero_less_real_of_nat_iff";"(0 < real ?n) = (0 < ?n)"
3.728 + "zero_le_real_of_nat_iff";
3.729 + "real_add_number_of_left";
3.730 + "real_mult_number_of_left";
3.731 + "number_of ?v * (number_of ?w * ?z) = number_of (bin_mult ?v ?w) * ?z"
3.732 + "real_add_number_of_diff1";
3.733 + "real_add_number_of_diff2";"number_of ?v + (?c - number_of ?w) =
3.734 + number_of (bin_add ?v (bin_minus ?w)) + ?c"
3.735 + "real_of_nat_number_of";
3.736 + "real (number_of ?v) = (if neg (number_of ?v) then 0 else number_of ?v)"
3.737 + "real_less_iff_diff_less_0"; "(?x < ?y) = (?x - ?y < 0)"
3.738 + "real_eq_iff_diff_eq_0";
3.739 + "real_le_iff_diff_le_0";
3.740 + "left_real_add_mult_distrib";
3.741 + (**)"?i * ?u + (?j * ?u + ?k) = (?i + ?j) * ?u + ?k"
3.742 + "real_eq_add_iff1";
3.743 + "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)"
3.744 + "real_eq_add_iff2";
3.745 + "real_less_add_iff1";
3.746 + "real_less_add_iff2";
3.747 + "real_le_add_iff1";
3.748 + "real_le_add_iff2";
3.749 + "real_mult_le_mono1";
3.750 + "real_mult_le_mono2";
3.751 + "real_mult_le_mono";
3.752 + "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l"
3.753 +RealArith0.ML:qed ------------------------------------------------------------
3.754 + "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y"
3.755 + "real_0_divide"; (**)"0 / ?x = 0"
3.756 + "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)"
3.757 + "real_inverse_less_0_iff";
3.758 + "real_0_le_inverse_iff";
3.759 + "real_inverse_le_0_iff";
3.760 + "REAL_DIVIDE_ZERO"; "?x / 0 = 0"(*!!!*)
3.761 + "real_inverse_eq_divide";
3.762 + "real_0_less_divide_iff";"(0 < ?x / ?y) = (0 < ?x & 0 < ?y | ?x < 0 & ?y < 0)"
3.763 + "real_divide_less_0_iff";
3.764 + "real_0_le_divide_iff";
3.765 + "real_divide_le_0_iff";
3.766 + "real_inverse_zero_iff";
3.767 + "real_divide_eq_0_iff";
3.768 + "real_divide_self_eq"; "?h ~= 0 ==> ?h / ?h = 1"(**)
3.769 + "real_minus_less_minus"; "(- ?y < - ?x) = (?x < ?y)"
3.770 + "real_mult_less_mono1_neg"; "[| ?i < ?j; ?k < 0 |] ==> ?j * ?k < ?i * ?k"
3.771 + "real_mult_less_mono2_neg";
3.772 + "real_mult_le_mono1_neg";
3.773 + "real_mult_le_mono2_neg";
3.774 + "real_mult_less_cancel2";
3.775 + "real_mult_le_cancel2";
3.776 + "real_mult_less_cancel1";
3.777 + "real_mult_le_cancel1";
3.778 + "real_mult_eq_cancel1"; "(?k * ?m = ?k * ?n) = (?k = 0 | ?m = ?n)"
3.779 + "real_mult_eq_cancel2"; "(?m * ?k = ?n * ?k) = (?k = 0 | ?m = ?n)"
3.780 + "real_mult_div_cancel1"; (**)"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
3.781 + "real_mult_div_cancel_disj";
3.782 + "?k * ?m / (?k * ?n) = (if ?k = 0 then 0 else ?m / ?n)"
3.783 + "pos_real_le_divide_eq";
3.784 + "neg_real_le_divide_eq";
3.785 + "pos_real_divide_le_eq";
3.786 + "neg_real_divide_le_eq";
3.787 + "pos_real_less_divide_eq";
3.788 + "neg_real_less_divide_eq";
3.789 + "pos_real_divide_less_eq";
3.790 + "neg_real_divide_less_eq";
3.791 + "real_eq_divide_eq"; (**)"?z ~= 0 ==> (?x = ?y / ?z) = (?x * ?z = ?y)"
3.792 + "real_divide_eq_eq"; (**)"?z ~= 0 ==> (?y / ?z = ?x) = (?y = ?x * ?z)"
3.793 + "real_divide_eq_cancel2"; "(?m / ?k = ?n / ?k) = (?k = 0 | ?m = ?n)"
3.794 + "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)"
3.795 + "real_inverse_less_iff";
3.796 + "real_inverse_le_iff";
3.797 + "real_divide_1"; (**)"?x / 1 = ?x"
3.798 + "real_divide_minus1"; (**)"?x / -1 = - ?x"
3.799 + "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)"
3.800 + "real_lbound_gt_zero";
3.801 + "[| 0 < ?d1.0; 0 < ?d2.0 |] ==> EX e. 0 < e & e < ?d1.0 & e < ?d2.0"
3.802 + "real_inverse_eq_iff"; "(inverse ?x = inverse ?y) = (?x = ?y)"
3.803 + "real_divide_eq_iff"; "(?z / ?x = ?z / ?y) = (?z = 0 | ?x = ?y)"
3.804 + "real_less_minus"; "(?x < - ?y) = (?y < - ?x)"
3.805 + "real_minus_less"; "(- ?x < ?y) = (- ?y < ?x)"
3.806 + "real_le_minus";
3.807 + "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)"
3.808 + "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)"
3.809 + "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)"
3.810 + "real_add_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
3.811 + "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)"
3.812 + "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)"
3.813 + "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)"
3.814 + "real_0_less_add_iff";
3.815 + "real_add_le_0_iff";
3.816 + "real_0_le_add_iff";
3.817 + "real_0_less_diff_iff"; "(0 < ?x - ?y) = (?y < ?x)"
3.818 + "real_0_le_diff_iff";
3.819 + "real_minus_diff_eq"; (**)"- (?x - ?y) = ?y - ?x"
3.820 + "real_less_half_sum"; "?x < ?y ==> ?x < (?x + ?y) / 2"
3.821 + "real_gt_half_sum";
3.822 + "real_dense"; "?x < ?y ==> EX r. ?x < r & r < ?y"
3.823 +RealArith ///!!!///-----------------------------------------------------------
3.824 +RComplete.ML:qed -------------------------------------------------------------
3.825 + "real_sum_of_halves"; (**)"?x / 2 + ?x / 2 = ?x"
3.826 + "real_sup_lemma1";
3.827 + "real_sup_lemma2";
3.828 + "posreal_complete";
3.829 + "real_isLub_unique";
3.830 + "real_order_restrict";
3.831 + "posreals_complete";
3.832 + "real_sup_lemma3";
3.833 + "lemma_le_swap2";
3.834 + "lemma_real_complete2b";
3.835 + "reals_complete";
3.836 + "real_of_nat_Suc_gt_zero";
3.837 + "reals_Archimedean"; "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x"
3.838 + "reals_Archimedean2";
3.839 +RealAbs.ML:qed
3.840 + "abs_nat_number_of";
3.841 + "abs (number_of ?v) =
3.842 + (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)"
3.843 + "abs_split";
3.844 + "abs_iff";
3.845 + "abs_zero"; "abs 0 = 0"
3.846 + "abs_one";
3.847 + "abs_eqI1";
3.848 + "abs_eqI2";
3.849 + "abs_minus_eqI2";
3.850 + "abs_minus_eqI1";
3.851 + "abs_ge_zero"; "0 <= abs ?x"
3.852 + "abs_idempotent"; "abs (abs ?x) = abs ?x"
3.853 + "abs_zero_iff"; "(abs ?x = 0) = (?x = 0)"
3.854 + "abs_ge_self"; "?x <= abs ?x"
3.855 + "abs_ge_minus_self";
3.856 + "abs_mult"; "abs (?x * ?y) = abs ?x * abs ?y"
3.857 + "abs_inverse"; "abs (inverse ?x) = inverse (abs ?x)"
3.858 + "abs_mult_inverse";
3.859 + "abs_triangle_ineq"; "abs (?x + ?y) <= abs ?x + abs ?y"
3.860 + "abs_triangle_ineq_four";
3.861 + "abs_minus_cancel";
3.862 + "abs_minus_add_cancel";
3.863 + "abs_triangle_minus_ineq";
3.864 +RealAbs.ML:qed_spec_mp
3.865 + "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s"
3.866 +RealAbs.ML:qed
3.867 + "abs_add_minus_less";
3.868 + "real_mult_0_less"; "(0 * ?x < ?r) = (0 < ?r)"
3.869 + "real_mult_less_trans";
3.870 + "real_mult_le_less_trans";
3.871 + "abs_mult_less";
3.872 + "abs_mult_less2";
3.873 + "abs_less_gt_zero";
3.874 + "abs_minus_one"; "abs -1 = 1"
3.875 + "abs_disj"; "abs ?x = ?x | abs ?x = - ?x"
3.876 + "abs_interval_iff";
3.877 + "abs_le_interval_iff";
3.878 + "abs_add_pos_gt_zero";
3.879 + "abs_add_one_gt_zero";
3.880 + "abs_not_less_zero";
3.881 + "abs_circle"; "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y"
3.882 + "abs_le_zero_iff";
3.883 + "real_0_less_abs_iff";
3.884 + "abs_real_of_nat_cancel";
3.885 + "abs_add_one_not_less_self";
3.886 + "abs_triangle_ineq_three"; "abs (?w + ?x + ?y) <= abs ?w + abs ?x + abs ?y"
3.887 + "abs_diff_less_imp_gt_zero";
3.888 + "abs_diff_less_imp_gt_zero2";
3.889 + "abs_diff_less_imp_gt_zero3";
3.890 + "abs_diff_less_imp_gt_zero4";
3.891 + "abs_triangle_ineq_minus_cancel";
3.892 + "abs_sum_triangle_ineq";
3.893 + "abs (?x + ?y + (- ?l + - ?m)) <= abs (?x + - ?l) + abs (?y + - ?m)"
3.894 +RealPow.ML:qed
3.895 + "realpow_zero"; "0 ^ Suc ?n = 0"
3.896 +RealPow.ML:qed_spec_mp
3.897 + "realpow_not_zero"; "?r ~= 0 ==> ?r ^ ?n ~= 0"
3.898 + "realpow_zero_zero"; "?r ^ ?n = 0 ==> ?r = 0"
3.899 + "realpow_inverse"; "inverse (?r ^ ?n) = inverse ?r ^ ?n"
3.900 + "realpow_abs"; "abs (?r ^ ?n) = abs ?r ^ ?n"
3.901 + "realpow_add"; (**)"?r ^ (?n + ?m) = ?r ^ ?n * ?r ^ ?m"
3.902 + "realpow_one"; (**)"?r ^ 1 = ?r"
3.903 + "realpow_two"; (**)"?r ^ Suc (Suc 0) = ?r * ?r"
3.904 +RealPow.ML:qed_spec_mp
3.905 + "realpow_gt_zero"; "0 < ?r ==> 0 < ?r ^ ?n"
3.906 + "realpow_ge_zero"; "0 <= ?r ==> 0 <= ?r ^ ?n"
3.907 + "realpow_le"; "0 <= ?x & ?x <= ?y ==> ?x ^ ?n <= ?y ^ ?n"
3.908 + "realpow_less";
3.909 +RealPow.ML:qed
3.910 + "realpow_eq_one"; (**)"1 ^ ?n = 1"
3.911 + "abs_realpow_minus_one"; "abs (-1 ^ ?n) = 1"
3.912 + "realpow_mult"; (**)"(?r * ?s) ^ ?n = ?r ^ ?n * ?s ^ ?n"
3.913 + "realpow_two_le"; "0 <= ?r ^ Suc (Suc 0)"
3.914 + "abs_realpow_two";
3.915 + "realpow_two_abs"; "abs ?x ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"
3.916 + "realpow_two_gt_one";
3.917 +RealPow.ML:qed_spec_mp
3.918 + "realpow_ge_one"; "1 < ?r ==> 1 <= ?r ^ ?n"
3.919 +RealPow.ML:qed
3.920 + "realpow_ge_one2";
3.921 + "two_realpow_ge_one";
3.922 + "two_realpow_gt";
3.923 + "realpow_minus_one"; (**)"-1 ^ (2 * ?n) = 1"
3.924 + "realpow_minus_one_odd"; "-1 ^ Suc (2 * ?n) = - 1"
3.925 + "realpow_minus_one_even";
3.926 +RealPow.ML:qed_spec_mp
3.927 + "realpow_Suc_less";
3.928 + "realpow_Suc_le"; "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n"
3.929 +RealPow.ML:qed
3.930 + "realpow_zero_le"; "0 <= 0 ^ ?n"
3.931 +RealPow.ML:qed_spec_mp
3.932 + "realpow_Suc_le2";
3.933 +RealPow.ML:qed
3.934 + "realpow_Suc_le3";
3.935 +RealPow.ML:qed_spec_mp
3.936 + "realpow_less_le"; "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n"
3.937 +RealPow.ML:qed
3.938 + "realpow_le_le"; "[| 0 <= ?r; ?r < 1; ?n <= ?N |] ==> ?r ^ ?N <= ?r ^ ?n"
3.939 + "realpow_Suc_le_self";
3.940 + "realpow_Suc_less_one";
3.941 +RealPow.ML:qed_spec_mp
3.942 + "realpow_le_Suc";
3.943 + "realpow_less_Suc";
3.944 + "realpow_le_Suc2";
3.945 + "realpow_gt_ge";
3.946 + "realpow_gt_ge2";
3.947 +RealPow.ML:qed
3.948 + "realpow_ge_ge"; "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N"
3.949 + "realpow_ge_ge2";
3.950 +RealPow.ML:qed_spec_mp
3.951 + "realpow_Suc_ge_self";
3.952 + "realpow_Suc_ge_self2";
3.953 +RealPow.ML:qed
3.954 + "realpow_ge_self";
3.955 + "realpow_ge_self2";
3.956 +RealPow.ML:qed_spec_mp
3.957 + "realpow_minus_mult"; "0 < ?n ==> ?x ^ (?n - 1) * ?x = ?x ^ ?n"
3.958 + "realpow_two_mult_inverse";
3.959 + "?r ~= 0 ==> ?r * inverse ?r ^ Suc (Suc 0) = inverse ?r"
3.960 + "realpow_two_minus"; "(- ?x) ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"
3.961 + "realpow_two_diff";
3.962 + "realpow_two_disj";
3.963 + "realpow_diff";
3.964 + "[| ?x ~= 0; ?m <= ?n |] ==> ?x ^ (?n - ?m) = ?x ^ ?n * inverse (?x ^ ?m)"
3.965 + "realpow_real_of_nat";
3.966 + "realpow_real_of_nat_two_pos"; "0 < real (Suc (Suc 0) ^ ?n)"
3.967 +RealPow.ML:qed_spec_mp
3.968 + "realpow_increasing";
3.969 + "realpow_Suc_cancel_eq";
3.970 + "[| 0 <= ?x; 0 <= ?y; ?x ^ Suc ?n = ?y ^ Suc ?n |] ==> ?x = ?y"
3.971 +RealPow.ML:qed
3.972 + "realpow_eq_0_iff"; "(?x ^ ?n = 0) = (?x = 0 & 0 < ?n)"
3.973 + "zero_less_realpow_abs_iff";
3.974 + "zero_le_realpow_abs";
3.975 + "real_of_int_power"; "real ?x ^ ?n = real (?x ^ ?n)"
3.976 + "power_real_number_of"; "number_of ?v ^ ?n = real (number_of ?v ^ ?n)"
3.977 +Ring_and_Field ---///!!!///---------------------------------------------------
3.978 +Complex_Numbers --///!!!///---------------------------------------------------
3.979 +Real -------------///!!!///---------------------------------------------------
3.980 +real_arith0.ML:qed "";
3.981 +real_arith0.ML:qed "";
3.982 +real_arith0.ML:qed "";
3.983 +real_arith0.ML:qed "";
3.984 +real_arith0.ML:qed "";
3.985 +real_arith0.ML:qed "";
3.986 +real_arith0.ML:qed "";
3.987 +real_arith0.ML:qed "";
3.988 +real_arith0.ML:qed "";
3.989 +
3.990 +
3.991 +
3.992 +
3.993 +
3.994 +
3.995 +
3.996 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/Scripts/Script.ML Thu Apr 17 18:01:03 2003 +0200
4.3 @@ -0,0 +1,62 @@
4.4 +(* lists of tactics, script-expressions etc.
4.5 + WN.14.3.00
4.6 + *)
4.7 +
4.8 +theory' := overwritel (! theory',
4.9 + [(e_domID,Script.thy),
4.10 + ("Script.thy",Script.thy)
4.11 + ]);
4.12 +
4.13 +(*--vvv----- SHIFT? or delete ?*)
4.14 +val IDTyp = Type("Script.ID",[]);
4.15 +
4.16 +
4.17 +val tacs = ref (distinct
4.18 + ["Calculate",
4.19 + "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",
4.20 + "Substitute","Mstep","Check'_elementswise",
4.21 + "Subproblem","Or'_to'_List"] \ "");
4.22 +
4.23 +val screxpr = ref (distinct
4.24 + ["Let","If","Repeat","While","Try","Or"] \ "");
4.25 +
4.26 +(*25.9.01---
4.27 +val subpbls = ref (distinct
4.28 + ["find'_vals",
4.29 + "make'_fun",
4.30 + "make'_solution'_set",
4.31 + "max'_on'_interval",
4.32 + "solve'_univar","solve'_univar'_err",
4.33 + "Testeq"] \ "");*)
4.34 +
4.35 +val listfuns = ref [(*_all_ functions in Isa99.List.thy *)
4.36 + "@","filter","concat","foldl","hd","last","set","list_all",
4.37 + "map","mem","nth","list_update","take","drop",
4.38 + "takeWhile","dropWhile","tl","butlast",
4.39 + "rev","zip","upt","remdups","nodups","replicate",
4.40 +
4.41 + "Cons","Nil"];
4.42 +
4.43 +val scrfuns = ref (distinct
4.44 + ["Testvar"] \ "");
4.45 +
4.46 +val listexpr = ref ((!listfuns) union (!scrfuns));
4.47 +
4.48 +val notsimp = ref
4.49 + (distinct (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns) \ "");
4.50 +
4.51 +val negotiable = ref ((!tacs (*@ !subpbls*)));
4.52 +
4.53 +val tacpbl = ref
4.54 + (distinct (!tacs (*@ !subpbls*)) \ "");
4.55 +(*--^^^----- SHIFT? or delete ?*)
4.56 +
4.57 +
4.58 +
4.59 +
4.60 +
4.61 +
4.62 +
4.63 +
4.64 +
4.65 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/Scripts/Script.thy Thu Apr 17 18:01:03 2003 +0200
5.3 @@ -0,0 +1,130 @@
5.4 +(* tactics, tacticals etc. for scripts
5.5 + W.N.24.2.00
5.6 + use_thy"Script";
5.7 + *)
5.8 +
5.9 +Script = ListG + Tools +
5.10 +
5.11 +types
5.12 +
5.13 + ID (* identifiers for thy, ruleset,... *)
5.14 + arg (* argument of subproblem *)
5.15 +
5.16 +arities
5.17 +
5.18 + ID, arg :: type
5.19 +
5.20 +consts
5.21 +
5.22 +(*types of subproblems' arguments*)
5.23 + real_ :: real => arg
5.24 + real_list_ :: (real list) => arg
5.25 + real_set_ :: (real set) => arg
5.26 + bool_ :: bool => arg
5.27 + bool_list_ :: (bool list) => arg
5.28 +
5.29 +(*tactics*)
5.30 + Rewrite :: "[ID, bool, 'a] => 'a"
5.31 + Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
5.32 + ("(Rewrite'_Inst (_ _ _))" 11)
5.33 + Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
5.34 + Rewrite'_Set'_Inst
5.35 + :: "[(real * real) list, ID, bool, 'a] => 'a"
5.36 + ("(Rewrite'_Set'_Inst (_ _ _))" 11)
5.37 + Calculate :: "[ID, 'a] => 'a"
5.38 + Substitute :: "[(real * real) list, 'a] => 'a"
5.39 + Mstep :: "ID => 'a"
5.40 + Check'_elementwise ::
5.41 + "['a list, 'b set] => 'a list"
5.42 + ("Check'_elementwise (_ _)" 11)
5.43 + Assumptions :: bool
5.44 + SubProblem :: "[ID * ID list * (ID * ID), arg list] => 'a"
5.45 +
5.46 + Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
5.47 + (*=========== record these ^^^ in 'tacs' in Script.ML =========*)
5.48 +
5.49 +(*special formulas for frontend 'CAS format'*)
5.50 + Subproblem :: "(ID * ID list) => 'a"
5.51 +
5.52 +(*script-expressions (tacticals)*)
5.53 + Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
5.54 + Try :: "['a => 'a, 'a] => 'a"
5.55 + Repeat :: "['a => 'a, 'a] => 'a"
5.56 + Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
5.57 + While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
5.58 + (*'b => bool doesn't work with "contains_root _"*)
5.59 + Letpar :: "['a, 'a => 'b] => 'b"
5.60 + (*--- defined in Isabelle/scr/HOL/HOL.thy:
5.61 + Let :: "['a, 'a => 'b] => 'b"
5.62 + "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
5.63 + If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
5.64 + %x. P x .. lambda is defined in Isabelles meta logic
5.65 + --- *)
5.66 +
5.67 +
5.68 + failtac, idletac :: 'a
5.69 + (*... + RECORD IN 'screxpr' in Script.ML *)
5.70 +
5.71 +
5.72 +(*SHIFT -> resp.thys ----vvv---------------------------------------------*)
5.73 +(*script-names: initial capital letter,
5.74 + type of last arg (=script-body) == result-type !
5.75 + Xxxx :: script ids, duplicate result-type 'r in last argument:
5.76 + "['a, ... , \
5.77 + \ 'r] => 'r
5.78 +*)
5.79 +
5.80 +(*make'_solution'_set :: "bool => bool list"
5.81 + ("(make'_solution'_set (_))" 11)
5.82 +
5.83 + max'_on'_interval
5.84 + :: "[ID * (ID list) * ID, bool,real,real set] => real"
5.85 + ("(max'_on'_interval (_)/ (_ _ _))" 9)
5.86 + find'_vals
5.87 + :: "[ID * (ID list) * ID,
5.88 + real,real,real,real,bool list] => bool list"
5.89 + ("(find'_vals (_)/ (_ _ _ _ _))" 9)
5.90 +
5.91 + make'_fun :: "[ID * (ID list) * ID, real,real,bool list] => bool"
5.92 + ("(make'_fun (_)/ (_ _ _))" 9)
5.93 +
5.94 + solve'_univar
5.95 + :: "[ID * (ID list) * ID, bool,real] => bool list"
5.96 + ("(solve'_univar (_)/ (_ _ ))" 9)
5.97 + solve'_univar'_err
5.98 + :: "[ID * (ID list) * ID, bool,real,bool] => bool list"
5.99 + ("(solve'_univar (_)/ (_ _ _))" 9)
5.100 +----------*)
5.101 +
5.102 + Testeq :: "[bool, \
5.103 + \ bool] => bool"
5.104 + ("((Script Testeq (_ =))// \
5.105 + \ (_))" 9)
5.106 +
5.107 + Testeq2 :: "[bool, \
5.108 + \ bool list] => bool list"
5.109 + ("((Script Testeq2 (_ =))// \
5.110 + \ (_))" 9)
5.111 +
5.112 + Testterm :: "[real, \
5.113 + \ real] => real"
5.114 + ("((Script Testterm (_ =))// \
5.115 + \ (_))" 9)
5.116 +
5.117 + Testchk :: "[bool, real, \
5.118 + \ real list] => real list"
5.119 + ("((Script Testchk (_ _ =))// \
5.120 + \ (_))" 9)
5.121 + (*... + RECORD IN 'subpbls' in Script.ML *)
5.122 +(*SHIFT -> resp.thys ----^^^----------------------------*)
5.123 +
5.124 +syntax
5.125 +
5.126 + "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
5.127 +
5.128 +translations
5.129 +
5.130 + "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
5.131 + "letpar x = a in e" == "Letpar a (%x. e)"
5.132 +
5.133 +end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/sml/Scripts/Tools.ML Thu Apr 17 18:01:03 2003 +0200
6.3 @@ -0,0 +1,136 @@
6.4 +(* auxiliary functions for scripts
6.5 + WN.9.00
6.6 +*)
6.7 +(* use"Isa99/Tools.ML";
6.8 + *)
6.9 +
6.10 +
6.11 +(*11.02: for equation solving only*)
6.12 +val UniversalList = (term_of o the o (parse Tools.thy)) "UniversalList";
6.13 +val EmptyList = (term_of o the o (parse Tools.thy)) "[]::bool list";
6.14 +
6.15 +
6.16 +
6.17 +(*+ for Or_to_List +*)
6.18 +fun or2list (Const ("True",_)) = UniversalList
6.19 + | or2list (Const ("False",_)) = EmptyList
6.20 + | or2list (t as Const ("op =",_) $ _ $ _) = list2isalist bool [t]
6.21 + | or2list ors =
6.22 + let fun get ls (Const ("op |",_) $ o1 $ o2) =
6.23 + case o2 of
6.24 + Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
6.25 + | _ => ls @ [o1, o2]
6.26 + in (((list2isalist bool) o (get [])) ors)
6.27 + handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end;
6.28 +(*>val t = HOLogic.true_const;
6.29 +> val t' = or2list t;
6.30 +> term2str t';
6.31 +"Atools.UniversalList"
6.32 +> val t = HOLogic.false_const;
6.33 +> val t' = or2list t;
6.34 +> term2str t';
6.35 +"[]"
6.36 +> val t=(term_of o the o (parse thy)) "x=3";
6.37 +> val t' = or2list t;
6.38 +> term2str t';
6.39 +"[x = 3]"
6.40 +> val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
6.41 +> val t' = or2list t;
6.42 +> term2str t';
6.43 +"[x = #3, x = #-3, x = #0]" : string *)
6.44 +
6.45 +
6.46 +
6.47 +
6.48 +(** evaluation on the meta-level **)
6.49 +
6.50 +(*. evaluate the predicate matches .*)
6.51 +(*("matches",("Tools.matches",eval_matches "#matches_")):calc*)
6.52 +fun eval_matches (thmid:string) (op_:string)
6.53 + (t as Const ("Tools.matches",_) $ pat $ tst) thy =
6.54 + if matches thy tst pat
6.55 + then let val prop = Trueprop $ (mk_equality (t, true_as_term))
6.56 + in Some ((string_of_cterm o cterm_of (sign_of thy)) prop,
6.57 + prop) end
6.58 + else let val prop = Trueprop $ (mk_equality (t, false_as_term))
6.59 + in Some ((string_of_cterm o cterm_of (sign_of thy)) prop,
6.60 + prop) end
6.61 + | eval_matches _ _ _ _ = None;
6.62 +(*
6.63 +> val t = (term_of o the o (parse thy))
6.64 + "matches (?x = 0) (1 * x ^^^ 2 = 0)";
6.65 +> eval_matches "/thmid/" "/op_/" t thy;
6.66 +val it =
6.67 + Some
6.68 + ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
6.69 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
6.70 +
6.71 +> val t = (term_of o the o (parse thy))
6.72 + "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
6.73 +> eval_matches "/thmid/" "/op_/" t thy;
6.74 +val it =
6.75 + Some
6.76 + ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
6.77 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
6.78 +
6.79 +> val t = (term_of o the o (parse thy))
6.80 + "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
6.81 +> eval_matches "/thmid/" "/op_/" t thy;
6.82 +val it =
6.83 + Some
6.84 + ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
6.85 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
6.86 +
6.87 +> val t = (term_of o the o (parse thy))
6.88 + "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
6.89 +> eval_matches "/thmid/" "/op_/" t thy;
6.90 +val it =
6.91 + Some
6.92 + ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
6.93 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
6.94 +----- before ?patterns ---:
6.95 +> val t = (term_of o the o (parse thy))
6.96 + "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
6.97 +> eval_matches "/thmid/" "/op_/" t thy;
6.98 +Some
6.99 + ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
6.100 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
6.101 + : (string * term) option
6.102 +
6.103 +> val t = (term_of o the o (parse thy))
6.104 + "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
6.105 +> eval_matches "/thmid/" "/op_/" t thy;
6.106 +Some ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
6.107 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
6.108 +
6.109 +> val t = (term_of o the o (parse thy))
6.110 + "matches (a = b) (x + #1 + #-1 * #2 = #0)";
6.111 +> eval_matches "/thmid/" "/op_/" t thy;
6.112 +Some ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
6.113 +*)
6.114 +
6.115 +
6.116 +(*get the variables in an isabelle-term*)
6.117 +(*("Var" ,("Tools.Var" ,eval_var "#Var_")):calc*)
6.118 +fun eval_var (thmid:string) (op_:string)
6.119 + (t as (Const(op0,t0) $ arg)) thy =
6.120 + let
6.121 + val t' = ((list2isalist HOLogic.realT) o vars) t;
6.122 + val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
6.123 + in Some (thmId, Trueprop $ (mk_equality (t,t'))) end
6.124 + | eval_var _ _ _ _ = None;
6.125 +
6.126 +(*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*)
6.127 +fun eval_lhs _ _
6.128 + (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ =
6.129 + Some ((term2str t) ^ " = " ^ (term2str l),
6.130 + Trueprop $ (mk_equality (t, l)))
6.131 + | eval_lhs _ _ _ _ = None;
6.132 +(*
6.133 +> val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
6.134 +> val Some (id,t') = eval_lhs 0 0 t 0;
6.135 +val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
6.136 +> term2str t';
6.137 +val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
6.138 +*)
6.139 +