1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Thu Dec 27 12:25:27 2007 +0100
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Thu Dec 27 15:20:44 2007 +0100
1.3 @@ -3,6 +3,9 @@
1.4 (c) due to copyright terms
1.5 remove_thy"PolyMinus";
1.6 use_thy"IsacKnowledge/PolyMinus";
1.7 +
1.8 +use_thy"IsacKnowledge/Isac";
1.9 +use"IsacKnowledge/PolyMinus.ML";
1.10 *)
1.11
1.12 (** interface isabelle -- isac **)
1.13 @@ -14,18 +17,29 @@
1.14 attention: num is Free("123",_) *)
1.15 fun identifier (Free (id,_)) = id
1.16 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.17 - if is_numeral num then "|||||||||||||"
1.18 - else id
1.19 + if is_numeral num then id
1.20 + else "|||||||||||||"
1.21 | identifier _ = "|||||||||||||"(*the "largest" string*);
1.22
1.23 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
1.24 -(* order by alphabet w.r.t. var: num < (var | num*var) *)
1.25 +(* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
1.26 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
1.27 - if identifier a < identifier b then
1.28 - Some ((term2str p) ^ " = True",
1.29 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.30 - else Some ((term2str p) ^ " = False",
1.31 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.32 + (writeln ("@@@ eval_kleiner: " ^ term2str p);
1.33 + if is_num a andalso is_num b then
1.34 + if int_of_Free a < int_of_Free b then
1.35 + Some ((term2str p) ^ " = True",
1.36 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.37 + else Some ((term2str p) ^ " = False",
1.38 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.39 + else
1.40 + if identifier a < identifier b then
1.41 + (writeln ("@@@ eval_kleiner: " ^ term2str p ^ " = True");
1.42 + Some ((term2str p) ^ " = True",
1.43 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.44 + )
1.45 + else Some ((term2str p) ^ " = False",
1.46 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.47 + )
1.48 | eval_kleiner _ _ _ _ = None;
1.49
1.50 fun ist_monom (Free (id,_)) = true
1.51 @@ -61,12 +75,16 @@
1.52 erls = erls_ordne_alphabetisch,
1.53 rules = [Thm ("tausche_plus",num_str tausche_plus),
1.54 (*"b kleiner a ==> (b + a) = (a + b)"*)
1.55 + Thm ("tausche_minus",num_str tausche_minus),
1.56 + (*"b kleiner a ==> (b - a) = (-a + b)"*)
1.57 Thm ("tausche_plus_plus",num_str tausche_plus_plus),
1.58 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
1.59 Thm ("tausche_plus_minus",num_str tausche_plus_minus),
1.60 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
1.61 - Thm ("tausche_minus_plus",num_str tausche_minus_plus)
1.62 + Thm ("tausche_minus_plus",num_str tausche_minus_plus),
1.63 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
1.64 + Thm ("tausche_minus_minus",num_str tausche_minus_minus)
1.65 + (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
1.66 ], scr = EmptyScr}:rls;
1.67
1.68 (** problems **)
2.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Thu Dec 27 12:25:27 2007 +0100
2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Thu Dec 27 15:20:44 2007 +0100
2.3 @@ -16,9 +16,11 @@
2.4 rules
2.5
2.6 tausche_plus "[| a kleiner b; b ist_monom |] ==> (b + a) = (a + b)"
2.7 + tausche_minus "[| a kleiner b; b ist_monom |] ==> (b - a) = (-a + b)"
2.8 tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)"
2.9 tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)"
2.10 tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
2.11 + tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
2.12
2.13 end
2.14
3.1 --- a/src/sml/ROOT.ML Thu Dec 27 12:25:27 2007 +0100
3.2 +++ b/src/sml/ROOT.ML Thu Dec 27 15:20:44 2007 +0100
3.3 @@ -151,6 +151,7 @@
3.4 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
3.5 use"logexp.sml";
3.6 use"poly.sml";
3.7 + use"polyminus.sml";
3.8 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
3.9 ? also check others without check 'diff.behav.'*);
3.10 use"rateq.sml";
4.1 --- a/src/sml/RTEST-root.sml Thu Dec 27 12:25:27 2007 +0100
4.2 +++ b/src/sml/RTEST-root.sml Thu Dec 27 15:20:44 2007 +0100
4.3 @@ -61,6 +61,7 @@
4.4 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
4.5 use"logexp.sml";
4.6 use"poly.sml";
4.7 + use"polyminus.sml";
4.8 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
4.9 ? also check others without check 'diff.behav.'*);
4.10 use"rateq.sml";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/Scripts/term_G.sml Thu Dec 27 15:20:44 2007 +0100
5.3 @@ -0,0 +1,1273 @@
5.4 +(* extends Isabelle/src/Pure/term.ML
5.5 + (c) Walther Neuper 1999
5.6 +
5.7 +use"Scripts/term_G.sml";
5.8 +use"term_G.sml";
5.9 +*)
5.10 +
5.11 +(*
5.12 +> cterm_of (sign_of thy) a_term;
5.13 +val it = "empty" : cterm *)
5.14 +
5.15 +
5.16 +
5.17 +fun match thy t pat =
5.18 + (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
5.19 + handle _ => [];
5.20 +fun matches thy t pat = if match thy t pat = [] then false else true;
5.21 +(*
5.22 +> val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
5.23 +> val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
5.24 + !^^^^^^^^!... necessary for Pattern.match
5.25 +> val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
5.26 + val insts =
5.27 + ([],
5.28 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
5.29 + (("a",0),Free ("3","RealDef.real"))])
5.30 + : (indexname * typ) list * (indexname * term) list*)
5.31 +
5.32 +
5.33 +(*
5.34 + datatype typ =
5.35 + Type of string * typ list |
5.36 + TFree of string * sort |
5.37 + TVar of indexname * sort
5.38 +> ("wer",1):indexname;
5.39 +> ["wer"]:sort;
5.40 +*)
5.41 +fun atomtyp t =
5.42 + let
5.43 + fun ato n (Type (s,[])) =
5.44 + ("\n*** "^indent n^"Type ("^s^",[])")
5.45 + | ato n (Type (s,Ts)) =
5.46 + ("\n*** "^indent n^"Type ("^s^",["^ atol (n+1) Ts)
5.47 +
5.48 + | ato n (TFree (s,sort)) =
5.49 + ("\n*** "^indent n^"TFree ("^s^",["^ strs2str' sort)
5.50 +
5.51 + | ato n (TVar ((s,i),sort)) =
5.52 + ("\n*** "^indent n^"TVar (("^s^","^
5.53 + string_of_int i ^ strs2str' sort)
5.54 + and atol n [] =
5.55 + ("\n*** "^indent n^"]")
5.56 + | atol n (T::Ts) = (ato n T ^ atol n Ts)
5.57 +in print (ato 0 t ^ "\n") end;
5.58 +
5.59 +(*
5.60 +> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
5.61 +> atomtyp T;
5.62 +*** Type (fun,[
5.63 +*** Type (RealDef.real,[])
5.64 +*** Type (fun,[
5.65 +*** Type (IntDef.int,[])
5.66 +*** Type (nat,[])
5.67 +*** ]
5.68 +*** ]
5.69 +*)
5.70 +fun atomt t =
5.71 + let fun ato (Const(a,T)) n =
5.72 + print("*** "^indent n^"Const ("^a^")")
5.73 + | ato (Free (a,T)) n =
5.74 + print("*** "^indent n^"Free ("^a^", "^")")
5.75 + | ato (Var ((a,ix),T)) n =
5.76 + print("*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")")
5.77 + | ato (Bound ix) n =
5.78 + print("*** "^indent n^"Bound "^(string_of_int ix))
5.79 + | ato (Abs(a,T,body)) n =
5.80 + (print("*** "^indent n^"Abs("^a^",..");ato body (n+1))
5.81 + | ato (f$t') n = (ato f n; ato t' (n+1))
5.82 + in print"*** -------------"; ato t 0; print"\n" end;
5.83 +
5.84 +fun term_detail2str t =
5.85 + let fun ato (Const(a,T)) n =
5.86 + "\n*** "^indent n^"Const ("^a^", "^
5.87 + (Sign.string_of_typ (sign_of thy) T)^")"
5.88 + | ato (Free (a,T)) n =
5.89 + "\n*** "^indent n^"Free ("^a^", "^
5.90 + (Sign.string_of_typ (sign_of thy) T)^")"
5.91 + | ato (Var ((a,ix),T)) n =
5.92 + "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^
5.93 + (Sign.string_of_typ (sign_of thy) T)^")"
5.94 + | ato (Bound ix) n =
5.95 + "\n*** "^indent n^"Bound "^string_of_int ix
5.96 + | ato (Abs(a,T,body)) n =
5.97 + "\n*** "^indent n^"Abs ("^a^", "^
5.98 + (Sign.string_of_typ (sign_of thy) T)^",.."
5.99 + ^ato body (n+1)
5.100 + | ato (f$t') n = ato f n^ato t' (n+1)
5.101 + in "\n*** "^ato t 0^"\n***\n" end;
5.102 +fun atomty t = (writeln o term_detail2str) t;
5.103 +
5.104 +fun term_str thy (Const(s,_)) = s
5.105 + | term_str thy (Free(s,_)) = s
5.106 + | term_str thy (Var((s,i),_)) = s^(string_of_int i)
5.107 + | term_str thy (Bound i) = "B."^(string_of_int i)
5.108 + | term_str thy (Abs(s,_,_)) = s
5.109 + | term_str thy t = raise error("term_str not for "^
5.110 + (Sign.string_of_term (sign_of thy) t));
5.111 +
5.112 +(*.contains the fst argument the second argument (a leave! of term).*)
5.113 +fun contains_term (Abs(_,_,body)) t = contains_term body t
5.114 + | contains_term (f $ f') t = contains_term f t orelse contains_term f' t
5.115 + | contains_term s t = t = s;
5.116 +
5.117 +(*..*)
5.118 +fun int_of_str str =
5.119 + let val ss = explode str
5.120 + val str' = case ss of
5.121 + "("::s => drop_last s | _ => ss
5.122 + in case BasisLibrary.Int.fromString (implode str') of
5.123 + SOME i => Some i
5.124 + | NONE => None end;
5.125 +(*
5.126 +> int_of_str "123";
5.127 +val it = Some 123 : int option > int_of_str "(-123)";
5.128 +val it = Some 123 : int option > int_of_str "#123";
5.129 +val it = None : int option > int_of_str "-123";
5.130 +val it = Some ~123 : int option *)
5.131 +fun int_of_str' str =
5.132 + case int_of_str str of
5.133 + Some i => i
5.134 + | None => raise TERM ("int_of_string: no int-string",[]);
5.135 +val str2int = int_of_str';
5.136 +
5.137 +fun is_numeral str = case int_of_str str of
5.138 + Some _ => true
5.139 + | None => false;
5.140 +val is_no = is_numeral;
5.141 +fun is_num (Free (s,_)) = if is_numeral s then true else false
5.142 + | is_num _ = false;
5.143 +(*>
5.144 +> is_num ((term_of o the o (parse thy)) "#1");
5.145 +val it = true : bool
5.146 +> is_num ((term_of o the o (parse thy)) "#-1");
5.147 +val it = true : bool
5.148 +> is_num ((term_of o the o (parse thy)) "a123");
5.149 +val it = false : bool
5.150 +*)
5.151 +
5.152 +fun int_of_Free (Free (intstr, _)) =
5.153 + (case BasisLibrary.Int.fromString intstr of
5.154 + SOME i => i
5.155 + | NONE => raise error ("int_of_Free ( "^ intstr ^", _)"))
5.156 + | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");
5.157 +
5.158 +fun vars t =
5.159 + let
5.160 + fun scan vs (Const(s,T)) = vs
5.161 + | scan vs (t as Free(s,T)) = if is_no s then vs else t::vs
5.162 + | scan vs (t as Var((s,i),T)) = t::vs
5.163 + | scan vs (Bound i) = vs
5.164 + | scan vs (Abs(s,T,t)) = scan vs t
5.165 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
5.166 + in (distinct o (scan [])) t end;
5.167 +
5.168 +fun is_Free (Free _) = true
5.169 + | is_Free _ = false;
5.170 +fun is_fun_id (Const _) = true
5.171 + | is_fun_id (Free _) = true
5.172 + | is_fun_id _ = false;
5.173 +fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
5.174 + | is_f_x _ = false;
5.175 +(* is_f_x (str2term "q_0/2 * L * x") (*false*);
5.176 + is_f_x (str2term "M_b x") (*true*);
5.177 + *)
5.178 +fun vars_str t =
5.179 + let
5.180 + fun scan vs (Const(s,T)) = vs
5.181 + | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
5.182 + | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
5.183 + | scan vs (Bound i) = vs
5.184 + | scan vs (Abs(s,T,t)) = scan vs t
5.185 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
5.186 + in (distinct o (scan [])) t end;
5.187 +
5.188 +fun ids2str t =
5.189 + let
5.190 + fun scan vs (Const(s,T)) = if is_no s then vs else s::vs
5.191 + | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
5.192 + | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
5.193 + | scan vs (Bound i) = vs
5.194 + | scan vs (Abs(s,T,t)) = scan (s::vs) t
5.195 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
5.196 + in (distinct o (scan [])) t end;
5.197 +fun is_bdv str =
5.198 + case explode str of
5.199 + "b"::"d"::"v"::_ => true
5.200 + | _ => false;
5.201 +fun is_bdv_ (Free (s,_)) = is_bdv s
5.202 + | is_bdv_ _ = false;
5.203 +
5.204 +fun free2str (Free (s,_)) = s
5.205 + | free2str t = raise error ("free2str not for "^
5.206 + (Sign.string_of_term (sign_of thy) t));
5.207 +fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
5.208 + handle _ => raise error ("free2int: "^term_detail2str t))
5.209 + | free2int t = raise error ("free2int: "^term_detail2str t);
5.210 +
5.211 +(*27.8.01: unused*)
5.212 +fun var2free (t as Const(s,T)) = t
5.213 + | var2free (t as Free(s,T)) = t
5.214 + | var2free (Var((s,i),T)) = Free(s,T)
5.215 + | var2free (t as Bound i) = t
5.216 + | var2free (Abs(s,T,t)) = Abs(s,T,var2free t)
5.217 + | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
5.218 +
5.219 +(*27.8.01: doesn't find some subterm ???!???*)
5.220 +fun free2var (t as Const(s,T)) = t
5.221 + | free2var (t as Free(s,T)) = if is_no s then t else Var((s,0),T)
5.222 + | free2var (t as Var((s,i),T)) = t
5.223 + | free2var (t as Bound i) = t
5.224 + | free2var (Abs(s,T,t)) = Abs(s,T,free2var t)
5.225 + | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
5.226 +
5.227 +
5.228 +fun mk_listT T = Type ("List.list", [T]);
5.229 +fun list_const T =
5.230 + Const("List.list.Cons", [T, mk_listT T] ---> mk_listT T);
5.231 +(*28.8.01: TODO: get type from head of list: 1 arg less!!!*)
5.232 +fun list2isalist T [] = Const("List.list.Nil",mk_listT T)
5.233 + | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts);
5.234 +(*
5.235 +> val tt = (term_of o the o (parse thy)) "R=(R::real)";
5.236 +> val TT = type_of tt;
5.237 +> val ss = list2isalist TT [tt,tt,tt];
5.238 +> cterm_of (sign_of thy) ss;
5.239 +val it = "[R = R, R = R, R = R]" : cterm *)
5.240 +
5.241 +fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);
5.242 +
5.243 +val listType = Type ("List.list",[Type ("bool",[])]);
5.244 +fun isalist2list ls =
5.245 + let
5.246 + fun get es (Const("List.list.Cons",_) $ t $ ls) = get (t::es) ls
5.247 + | get es (Const("List.list.Nil",_)) = es
5.248 + | get _ t =
5.249 + raise error ("isalist2list applied to NON-list '"^term2str t^"'")
5.250 + in (rev o (get [])) ls end;
5.251 +(*
5.252 +> val il = str2term "[a=b,c=d,e=f]";
5.253 +> val l = isalist2list il;
5.254 +> (writeln o terms2str) l;
5.255 +["a = b","c = d","e = f"]
5.256 +
5.257 +> val il = str2term "ss___::bool list";
5.258 +> val l = isalist2list il;
5.259 +[Free ("ss___", "bool List.list")]
5.260 +*)
5.261 +
5.262 +
5.263 +
5.264 +val prop = Type ("prop",[]); (* ~/Diss.99/Integers-Isa/tools.sml*)
5.265 +val bool = Type ("bool",[]); (* Integ.int *)
5.266 +val Trueprop = Const("Trueprop",bool-->prop);
5.267 +fun mk_prop t = Trueprop $ t;
5.268 +val true_as_term = Const("True",bool);
5.269 +val false_as_term = Const("False",bool);
5.270 +val true_as_cterm = cterm_of (sign_of thy) true_as_term;
5.271 +val false_as_cterm = cterm_of (sign_of thy) false_as_term;
5.272 +
5.273 +infixr 5 -->; (* /Pure/term.ML *)
5.274 +infixr --->; (* /Pure/term.ML *)
5.275 +fun S --> T = Type("fun",[S,T]); (* /Pure/term.ML *)
5.276 +val op ---> = foldr (op -->); (* /Pure/term.ML *)
5.277 +fun list_implies ([], B) = B : term
5.278 + | list_implies (A::AS, B) = implies $ A $ list_implies(AS,B);(* /term.ML *)
5.279 +
5.280 +
5.281 +
5.282 +(** substitution **)
5.283 +
5.284 +fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = (* = thm.ML *)
5.285 + match_bvs(s, t, if x="" orelse y="" then al
5.286 + else (x,y)::al)
5.287 + | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
5.288 + | match_bvs(_,_,al) = al;
5.289 +fun ren_inst(insts,prop,pat,obj) = (* = thm.ML *)
5.290 + let val ren = match_bvs(pat,obj,[])
5.291 + fun renAbs(Abs(x,T,b)) =
5.292 + Abs(case assoc_string(ren,x) of None => x
5.293 + | Some(y) => y, T, renAbs(b))
5.294 + | renAbs(f$t) = renAbs(f) $ renAbs(t)
5.295 + | renAbs(t) = t
5.296 + in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
5.297 +
5.298 +
5.299 +
5.300 +
5.301 +
5.302 +
5.303 +fun dest_equals' (Const("op =",_) $ t $ u) = (t,u)(* logic.ML: Const("=="*)
5.304 + | dest_equals' t = raise TERM("dest_equals'", [t]);
5.305 +val lhs_ = (fst o dest_equals');
5.306 +val rhs_ = (snd o dest_equals');
5.307 +
5.308 +fun is_equality (Const("op =",_) $ t $ u) = true (* logic.ML: Const("=="*)
5.309 + | is_equality _ = false;
5.310 +fun mk_equality (t,u) = (Const("op =",[type_of t,type_of u]--->bool) $ t $ u);
5.311 +fun is_expliceq (Const("op =",_) $ (Free _) $ u) = true
5.312 + | is_expliceq _ = false;
5.313 +fun strip_trueprop (Const("Trueprop",_) $ t) = t
5.314 + | strip_trueprop t = t;
5.315 +(* | strip_trueprop t = raise TERM("strip_trueprop", [t]);
5.316 +*)
5.317 +
5.318 +(*.(A1==>...An==>B) goes to (A1==>...An==>).*)
5.319 +fun strip_imp_prems' (Const("==>", T) $ A $ t) =
5.320 + let fun coll_prems As (Const("==>", _) $ A $ t) =
5.321 + coll_prems (As $ (implies $ A)) t
5.322 + | coll_prems As _ = Some As
5.323 + in coll_prems (implies $ A) t end
5.324 + | strip_imp_prems' _ = None; (* logic.ML: term -> term list*)
5.325 +(*
5.326 + val thm = real_mult_div_cancel1;
5.327 + val prop = (#prop o rep_thm) thm;
5.328 + atomt prop;
5.329 +*** -------------
5.330 +*** Const ( ==>)
5.331 +*** . Const ( Trueprop)
5.332 +*** . . Const ( Not)
5.333 +*** . . . Const ( op =)
5.334 +*** . . . . Var ((k, 0), )
5.335 +*** . . . . Const ( 0)
5.336 +*** . Const ( Trueprop)
5.337 +*** . . Const ( op =) *** .............
5.338 + val Some t = strip_imp_prems' ((#prop o rep_thm) thm);
5.339 + atomt t;
5.340 +*** -------------
5.341 +*** Const ( ==>)
5.342 +*** . Const ( Trueprop)
5.343 +*** . . Const ( Not)
5.344 +*** . . . Const ( op =)
5.345 +*** . . . . Var ((k, 0), )
5.346 +*** . . . . Const ( 0)
5.347 +
5.348 + val thm = real_le_anti_sym;
5.349 + val prop = (#prop o rep_thm) thm;
5.350 + atomt prop;
5.351 +*** -------------
5.352 +*** Const ( ==>)
5.353 +*** . Const ( Trueprop)
5.354 +*** . . Const ( op <=)
5.355 +*** . . . Var ((z, 0), )
5.356 +*** . . . Var ((w, 0), )
5.357 +*** . Const ( ==>)
5.358 +*** . . Const ( Trueprop)
5.359 +*** . . . Const ( op <=)
5.360 +*** . . . . Var ((w, 0), )
5.361 +*** . . . . Var ((z, 0), )
5.362 +*** . . Const ( Trueprop)
5.363 +*** . . . Const ( op =)
5.364 +*** .............
5.365 + val Some t = strip_imp_prems' ((#prop o rep_thm) thm);
5.366 + atomt t;
5.367 +*** -------------
5.368 +*** Const ( ==>)
5.369 +*** . Const ( Trueprop)
5.370 +*** . . Const ( op <=)
5.371 +*** . . . Var ((z, 0), )
5.372 +*** . . . Var ((w, 0), )
5.373 +*** . Const ( ==>)
5.374 +*** . . Const ( Trueprop)
5.375 +*** . . . Const ( op <=)
5.376 +*** . . . . Var ((w, 0), )
5.377 +*** . . . . Var ((z, 0), )
5.378 +*)
5.379 +
5.380 +(*. (A1==>...An==>) (B) goes to (A1==>...An==>B), where B is lowest branch.*)
5.381 +fun ins_concl (Const("==>", T) $ A $ t) B = implies $ A $ (ins_concl t B)
5.382 + | ins_concl (Const("==>", T) $ A ) B = implies $ A $ B
5.383 + | ins_concl t B = raise TERM("ins_concl", [t, B]);
5.384 +(*
5.385 + val thm = real_le_anti_sym;
5.386 + val prop = (#prop o rep_thm) thm;
5.387 + val concl = Logic.strip_imp_concl prop;
5.388 + val Some prems = strip_imp_prems' prop;
5.389 + val prop' = ins_concl prems concl;
5.390 + prop = prop';
5.391 + atomt prop;
5.392 + atomt prop';
5.393 +*)
5.394 +
5.395 +
5.396 +fun vperm (Var _, Var _) = true (* Pure/thm.ML *)
5.397 + | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
5.398 + | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
5.399 + | vperm (t, u) = (t = u);
5.400 +
5.401 +fun var_perm (t, u) = (* Pure/thm.ML *)
5.402 + vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
5.403 +
5.404 +(* fun decomp_simp, Pure/thm.ML *)
5.405 +fun perm lhs rhs = var_perm (lhs, rhs) andalso not (lhs aconv rhs)
5.406 + andalso not (is_Var lhs);
5.407 +
5.408 +
5.409 +(*---6.1.00: Isa99
5.410 +fun char2int c = ord c - ord "0";
5.411 +
5.412 +fun rev_strl2int [s] = char2int s
5.413 + | rev_strl2int (s::ss) = char2int s + 10*(rev_strl2int ss)
5.414 + | rev_strl2int _ = raise ERROR;
5.415 +
5.416 + fun int_of_str str = ---6.1.00: Isa99---
5.417 + let
5.418 + fun scan ("(" :: "+" :: is) =
5.419 + (case rev is of
5.420 + ")" :: si => rev_strl2int si
5.421 + | _ => raise error ("no number: "^str))
5.422 + | scan ("(" :: "-" :: is) =
5.423 + (case rev is of
5.424 + ")" :: si => (~1)*(rev_strl2int si)
5.425 + | _ => raise error ("no number: "^str))
5.426 + | scan ("(" :: is) =
5.427 + (case rev is of
5.428 + ")" :: si => rev_strl2int si
5.429 + | _ => raise error ("no number: "^str))
5.430 + | scan ( "+" :: is) = (rev_strl2int o rev) is
5.431 + | scan ( "-" :: is) = (~1)*((rev_strl2int o rev) is)
5.432 + | scan ( is) = (rev_strl2int o rev) is
5.433 + in (scan o skip_blanks o explode o strip_thy) str
5.434 + handle ERROR => raise error ("no number: "^str) end;
5.435 +---*)
5.436 +
5.437 +
5.438 +fun str_of_int n =
5.439 + if n < 0 then "-"^((string_of_int o abs) n)
5.440 + else string_of_int n;
5.441 +(*
5.442 +> str_of_int 1;
5.443 +val it = "1" : string > str_of_int ~1;
5.444 +val it = "-1" : string
5.445 +*)
5.446 +
5.447 +
5.448 +fun power b 0 = 1
5.449 + | power b n =
5.450 + if n>0 then b*(power b (n-1))
5.451 + else raise error ("power "^(str_of_int b)^" "^(str_of_int n));
5.452 +(*
5.453 +> power 2 3;
5.454 +val it = 8 : int
5.455 +> power ~2 3;
5.456 +val it = ~8 : int
5.457 +> power ~3 2;
5.458 +val it = 9 : int
5.459 +> power 3 ~2;
5.460 +*)
5.461 +fun gcd 0 b = b
5.462 + | gcd a b = if a < b then gcd (b mod a) a
5.463 + else gcd (a mod b) b;
5.464 +fun sign n = if n < 0 then ~1
5.465 + else if n = 0 then 0 else 1;
5.466 +fun sign2 n1 n2 = (sign n1) * (sign n2);
5.467 +
5.468 +infix dvd;
5.469 +fun d dvd n = n mod d = 0;
5.470 +
5.471 +fun divisors n =
5.472 + let fun pdiv ds d n =
5.473 + if d=n then d::ds
5.474 + else if d dvd n then pdiv (d::ds) d (n div d)
5.475 + else pdiv ds (d+1) n
5.476 + in pdiv [] 2 n end;
5.477 +
5.478 +divisors 30;
5.479 +divisors 32;
5.480 +divisors 60;
5.481 +divisors 11;
5.482 +
5.483 +fun doubles ds = (* ds is ordered *)
5.484 + let fun dbls ds [] = ds
5.485 + | dbls ds [i] = ds
5.486 + | dbls ds (i::i'::is) = if i=i' then dbls (i::ds) is
5.487 + else dbls ds (i'::is)
5.488 + in dbls [] ds end;
5.489 +(*> doubles [2,3,4];
5.490 +val it = [] : int list
5.491 +> doubles [2,3,3,5,5,7];
5.492 +val it = [5,3] : int list*)
5.493 +
5.494 +fun squfact 0 = 0
5.495 + | squfact 1 = 1
5.496 + | squfact n = foldl op* (1, (doubles o divisors) n);
5.497 +(*> squfact 30;
5.498 +val it = 1 : int
5.499 +> squfact 32;
5.500 +val it = 4 : int
5.501 +> squfact 60;
5.502 +val it = 2 : int
5.503 +> squfact 11;
5.504 +val it = 1 : int*)
5.505 +
5.506 +
5.507 +fun dest_type (Type(T,[])) = T
5.508 + | dest_type T =
5.509 + (atomtyp T;
5.510 + raise error ("... dest_type: not impl. for this type"));
5.511 +
5.512 +fun term_of_num ntyp n = Free (str_of_int n, ntyp);
5.513 +
5.514 +fun pairT T1 T2 = Type ("*", [T1, T2]);
5.515 +(*> val t = str2term "(1,2)";
5.516 +> type_of t = pairT HOLogic.realT HOLogic.realT;
5.517 +val it = true : bool
5.518 +*)
5.519 +fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
5.520 +(*> val t = str2term "(1,2)";
5.521 +> val Const ("Pair",pT) $ _ $ _ = t;
5.522 +> pT = PairT HOLogic.realT HOLogic.realT;
5.523 +val it = true : bool
5.524 +*)
5.525 +fun pairt t1 t2 =
5.526 + Const ("Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
5.527 +(*> val t = str2term "(1,2)";
5.528 +> val (t1, t2) = (str2term "1", str2term "2");
5.529 +> t = pairt t1 t2;
5.530 +val it = true : bool*)
5.531 +
5.532 +
5.533 +fun num_of_term (t as Free (s,_)) =
5.534 + (case int_of_str s of
5.535 + Some s' => s'
5.536 + | None => raise error ("num_of_term not for "^
5.537 + (Sign.string_of_term (sign_of thy) t)))
5.538 + | num_of_term t = raise error ("num_of_term not for "^
5.539 + (Sign.string_of_term (sign_of thy) t));
5.540 +
5.541 +fun mk_factroot op_(*=thy.sqrt*) T fact root =
5.542 + Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
5.543 + (Const (op_, T --> T) $ term_of_num T root);
5.544 +(*
5.545 +val T = (type_of o term_of o the) (parse thy "#12::real");
5.546 +val t = mk_factroot "SqRoot.sqrt" T 2 3;
5.547 +cterm_of (sign_of thy) t;
5.548 +val it = "#2 * sqrt #3 " : cterm
5.549 +*)
5.550 +fun var_op_num v op_ optype ntyp n =
5.551 + Const (op_, optype) $ v $
5.552 + Free (str_of_int n, ntyp);
5.553 +
5.554 +fun num_op_var v op_ optype ntyp n =
5.555 + Const (op_,optype) $
5.556 + Free (str_of_int n, ntyp) $ v;
5.557 +
5.558 +fun num_op_num T1 T2 (op_,Top) n1 n2 =
5.559 + Const (op_,Top) $
5.560 + Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
5.561 +(*
5.562 +> val t = num_op_num "Int" 3 4;
5.563 +> atomty t;
5.564 +> string_of_cterm (cterm_of (sign_of thy) t);
5.565 +*)
5.566 +
5.567 +fun const_in str (Const _) = false
5.568 + | const_in str (Free (s,_)) = if strip_thy s = str then true else false
5.569 + | const_in str (Bound _) = false
5.570 + | const_in str (Var _) = false
5.571 + | const_in str (Abs (_,_,body)) = const_in str body
5.572 + | const_in str (f$u) = const_in str f orelse const_in str u;
5.573 +(*
5.574 +> val t = (term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
5.575 +> const_in "sqrt" t;
5.576 +val it = true : bool
5.577 +> val t = (term_of o the o (parse thy)) "6 + 5 * 4 + 3";
5.578 +> const_in "sqrt" t;
5.579 +val it = false : bool
5.580 +*)
5.581 +
5.582 +(*used for calculating built in binary operations in Isabelle2002->Float.ML
5.583 +fun calc "op +" (n1, n2) = n1+n2
5.584 + | calc "op -" (n1, n2) = n1-n2
5.585 + | calc "op *" (n1, n2) = n1*n2
5.586 + | calc "HOL.divide"(n1, n2) = n1 div n2
5.587 + | calc "Atools.pow"(n1, n2) = power n1 n2
5.588 + | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
5.589 +fun calc_equ "op <" (n1, n2) = n1 < n2
5.590 + | calc_equ "op <=" (n1, n2) = n1 <= n2
5.591 + | calc_equ op_ _ =
5.592 + raise error ("calc_equ: operator = "^op_^" not defined");
5.593 +fun sqrt (n:int) = if n < 0 then 0
5.594 + (*FIXME ~~~*) else (trunc o Math.sqrt o BasisLibrary.Real.fromInt) n;
5.595 +
5.596 +fun mk_thmid thmid op_ n1 n2 =
5.597 + thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
5.598 +
5.599 +fun dest_binop_typ (Type("fun",[range,Type("fun",[arg2,arg1])])) =
5.600 + (arg1,arg2,range)
5.601 + | dest_binop_typ _ = raise error "dest_binop_typ: not binary";
5.602 +(* -----
5.603 +> val t = (term_of o the o (parse thy)) "#3^#4";
5.604 +> val hT = type_of (head_of t);
5.605 +> dest_binop_typ hT;
5.606 +val it = ("'a","nat","'a") : typ * typ * typ
5.607 + ----- *)
5.608 +
5.609 +
5.610 +(** transform binary numerals into
5.611 + Free("#numeral", Type ("polymorph",[])) **)
5.612 +
5.613 +(*5.1.00.: apply_trans in /Pure/Syntax/printer.ML
5.614 + to numeral_tr' in HOL/Tools/numeral_syntax.ML failed:
5.615 +fun pretty ... =
5.616 + val trans = apply_trans "print ast translation";
5.617 + and combT (tup as (c, a, args, p)) =
5.618 + in
5.619 + (case token_trans a args of (*try token translation function*)
5.620 + Some (s, len) => [Pretty.strlen_real s len]
5.621 + | None => (*try print translation functions*)
5.622 + astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
5.623 +
5.624 + Error: unbound type constructor: ast in path Ast.ast
5.625 +*)
5.626 +(*WN.28.8.03: *)
5.627 +fun app_num_tr'1 (Const("0",T)) = Free("0",T)
5.628 + | app_num_tr'1 (Const("1",T)) = Free("1",T)
5.629 +(*| app_num_tr'1 (t as Const("uminus",_) $ Free(s,T)) =
5.630 + (case int_of_str s of Some i =>
5.631 + if i > 0 then Free("-"^s,T) else Free(s,T)
5.632 + | None => t)
5.633 + | app_num_tr'1 (t as Const(s,T)) = t
5.634 +*)| app_num_tr'1 (Const("Numeral.number_of",Type ("fun", [_, T])) $ t) =
5.635 + Free(NumeralSyntax.dest_bin_str t, T)
5.636 +(*| app_num_tr'1 (t as Free(s,T)) = t
5.637 + | app_num_tr'1 (t as Var(n,T)) = t
5.638 + | app_num_tr'1 (t as Bound i) = t*)
5.639 + | app_num_tr'1 (Abs(s,T,body)) = Abs(s,T, app_num_tr'1 body)
5.640 + | app_num_tr'1 (t1 $ t2) = (app_num_tr'1 t1) $ (app_num_tr'1 t2)
5.641 + | app_num_tr'1 t = t;
5.642 +
5.643 +(*.to be used immediately before evaluation of numerals;
5.644 +see Scripts/calculate.sml .*)
5.645 +fun(*app_num_tr'2 (Const("0",T)) = Free("0",T)
5.646 + | app_num_tr'2 (Const("1",T)) = Free("1",T)
5.647 + |*)app_num_tr'2 (t as Const("uminus",_) $ Free(s,T)) =
5.648 + (case int_of_str s of Some i =>
5.649 + if i > 0 then Free("-"^s,T) else Free(s,T)
5.650 + | None => t)
5.651 +(*| app_num_tr'2 (t as Const(s,T)) = t
5.652 + | app_num_tr'2 (Const("Numeral.number_of",Type ("fun", [_, T])) $ t) =
5.653 + Free(NumeralSyntax.dest_bin_str t, T)
5.654 + | app_num_tr'2 (t as Free(s,T)) = t
5.655 + | app_num_tr'2 (t as Var(n,T)) = t
5.656 + | app_num_tr'2 (t as Bound i) = t
5.657 +*)| app_num_tr'2 (Abs(s,T,body)) = Abs(s,T, app_num_tr'2 body)
5.658 + | app_num_tr'2 (t1 $ t2) = (app_num_tr'2 t1) $ (app_num_tr'2 t2)
5.659 + | app_num_tr'2 t = t;
5.660 +
5.661 +fun num_str thm =
5.662 + let
5.663 + val {sign_ref = sign_ref, der = der, maxidx = maxidx,
5.664 + shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} =
5.665 + rep_thm_G thm;
5.666 + val prop' = app_num_tr'1 prop;
5.667 + in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;
5.668 +
5.669 +
5.670 +(** get types of Free and Abs for parse' **)
5.671 +(*11.1.00: not used, fix-typed +,*,-,^ instead *)
5.672 +
5.673 +val dummyT = Type ("dummy",[]);
5.674 +val dummyT = TVar (("DUMMY",0),[]);
5.675 +
5.676 +(* assumes only 1 type for numerals
5.677 + and different identifiers for Const, Free and Abs *)
5.678 +fun get_types t =
5.679 + let
5.680 + fun get ts (Const(s,T)) = (s,T)::ts
5.681 + | get ts (Free(s,T)) = if is_no s
5.682 + then ("#",T)::ts else (s,T)::ts
5.683 + | get ts (Var(n,T)) = ts
5.684 + | get ts (Bound i) = ts
5.685 + | get ts (Abs(s,T,body)) = get ((s,T)::ts) body
5.686 + | get ts (t1 $ t2) = (get ts t1) @ (get ts t2)
5.687 + in distinct (get [] t) end;
5.688 +(*
5.689 +val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
5.690 +get_types t;
5.691 +*)
5.692 +
5.693 +(*11.1.00: not used, fix-typed +,*,-,^ instead *)
5.694 +fun set_types al (Const(s,T)) =
5.695 + (case assoc (al,s) of
5.696 + Some T' => Const(s,T')
5.697 + | None => (warning ("set_types: no type for "^s); Const(s,dummyT)))
5.698 + | set_types al (Free(s,T)) =
5.699 + if is_no s then
5.700 + (case assoc (al,"#") of
5.701 + Some T' => Free(s,T')
5.702 + | None => (warning ("set_types: no type for numerals"); Free(s,T)))
5.703 + else (case assoc (al,s) of
5.704 + Some T' => Free(s,T')
5.705 + | None => (warning ("set_types: no type for "^s); Free(s,T)))
5.706 + | set_types al (Var(n,T)) = Var(n,T)
5.707 + | set_types al (Bound i) = Bound i
5.708 + | set_types al (Abs(s,T,body)) =
5.709 + (case assoc (al,s) of
5.710 + Some T' => Abs(s,T', set_types al body)
5.711 + | None => (warning ("set_types: no type for "^s);
5.712 + Abs(s,T, set_types al body)))
5.713 + | set_types al (t1 $ t2) = (set_types al t1) $ (set_types al t2);
5.714 +(*
5.715 +val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
5.716 +val al = get_types t;
5.717 +
5.718 +val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
5.719 +atomty t; (* 'a *)
5.720 +val t' = set_types al t;
5.721 +atomty t'; (*real*)
5.722 +cterm_of (sign_of thy) t';
5.723 +val it = "x = #0 + #-1 * #-4" : cterm
5.724 +
5.725 +val t = (term_of o the o (parse thy))
5.726 + "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2";
5.727 +atomty t;
5.728 +val t' = set_types al t;
5.729 +atomty t';
5.730 +cterm_of (sign_of thy) t';
5.731 +uncaught exception TYPE (*^^^ is new, NOT in al*)
5.732 +*)
5.733 +
5.734 +
5.735 +(** from Descript.ML **)
5.736 +
5.737 +(** decompose an isa-list to an ML-list
5.738 + i.e. [] belong to the meta-language, too **)
5.739 +
5.740 +fun is_list ((Const("List.list.Cons",_)) $ _ $ _) = true
5.741 + | is_list _ = false;
5.742 +(* val (Some ct) = parse thy "lll::real list";
5.743 +> val ty = (#t o rep_cterm) ct;
5.744 +> is_list ty;
5.745 +val it = false : bool
5.746 +> val (Some ct) = parse thy "[lll]";
5.747 +> val ty = (#t o rep_cterm) ct;
5.748 +> is_list ty;
5.749 +val it = true : bool *)
5.750 +
5.751 +
5.752 +
5.753 +fun mk_Free (s,T) = Free(s,T);
5.754 +fun mk_free T s = Free(s,T);
5.755 +
5.756 +(*instantiate let; necessary for ass_up*)
5.757 +fun inst_abs thy (Const sT) = Const sT
5.758 + | inst_abs thy (Free sT) = Free sT
5.759 + | inst_abs thy (Bound n) = Bound n
5.760 + | inst_abs thy (Var iT) = Var iT
5.761 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
5.762 + let val (v',b') = variant_abs (v,T2,b); (*fun variant_abs: term.ML*)
5.763 + in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end
5.764 + | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
5.765 + | inst_abs thy t =
5.766 + (writeln("inst_abs: unchanged t= "^(Sign.string_of_term (sign_of thy) t));
5.767 + t);
5.768 +(*val scr as (Script sc) = Script ((term_of o the o (parse thy))
5.769 + "Script Testeq (e_::bool) = \
5.770 + \While (contains_root e_) Do \
5.771 + \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \
5.772 + \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
5.773 + \ in Try (Repeat (Rewrite radd_0 False e_))) ");
5.774 +ML> atomt sc;
5.775 +*** Const ( Script.Testeq)
5.776 +*** . Free ( e_, )
5.777 +*** . Const ( Script.While)
5.778 +*** . . Const ( RatArith.contains'_root)
5.779 +*** . . . Free ( e_, )
5.780 +*** . . Const ( Let)
5.781 +*** . . . Const ( Script.Try)
5.782 +*** . . . . Const ( Script.Repeat)
5.783 +*** . . . . . Const ( Script.Rewrite)
5.784 +*** . . . . . . Free ( rroot_square_inv, )
5.785 +*** . . . . . . Const ( False)
5.786 +*** . . . . . . Free ( e_, )
5.787 +*** . . . Abs( e_,..
5.788 +*** . . . . Const ( Let)
5.789 +*** . . . . . Const ( Script.Try)
5.790 +*** . . . . . . Const ( Script.Repeat)
5.791 +*** . . . . . . . Const ( Script.Rewrite)
5.792 +*** . . . . . . . . Free ( square_equation_left, )
5.793 +*** . . . . . . . . Const ( True)
5.794 +*** . . . . . . . . Bound 0 <-- !!!
5.795 +*** . . . . . Abs( e_,..
5.796 +*** . . . . . . Const ( Script.Try)
5.797 +*** . . . . . . . Const ( Script.Repeat)
5.798 +*** . . . . . . . . Const ( Script.Rewrite)
5.799 +*** . . . . . . . . . Free ( radd_0, )
5.800 +*** . . . . . . . . . Const ( False)
5.801 +*** . . . . . . . . . Bound 0 <-- !!!
5.802 +val it = () : unit
5.803 +ML> atomt (inst_abs thy sc);
5.804 +*** Const ( Script.Testeq)
5.805 +*** . Free ( e_, )
5.806 +*** . Const ( Script.While)
5.807 +*** . . Const ( RatArith.contains'_root)
5.808 +*** . . . Free ( e_, )
5.809 +*** . . Const ( Let)
5.810 +*** . . . Const ( Script.Try)
5.811 +*** . . . . Const ( Script.Repeat)
5.812 +*** . . . . . Const ( Script.Rewrite)
5.813 +*** . . . . . . Free ( rroot_square_inv, )
5.814 +*** . . . . . . Const ( False)
5.815 +*** . . . . . . Free ( e_, )
5.816 +*** . . . Abs( e_,..
5.817 +*** . . . . Const ( Let)
5.818 +*** . . . . . Const ( Script.Try)
5.819 +*** . . . . . . Const ( Script.Repeat)
5.820 +*** . . . . . . . Const ( Script.Rewrite)
5.821 +*** . . . . . . . . Free ( square_equation_left, )
5.822 +*** . . . . . . . . Const ( True)
5.823 +*** . . . . . . . . Free ( e_, ) <-- !!!
5.824 +*** . . . . . Abs( e_,..
5.825 +*** . . . . . . Const ( Script.Try)
5.826 +*** . . . . . . . Const ( Script.Repeat)
5.827 +*** . . . . . . . . Const ( Script.Rewrite)
5.828 +*** . . . . . . . . . Free ( radd_0, )
5.829 +*** . . . . . . . . . Const ( False)
5.830 +*** . . . . . . . . . Free ( e_, ) <-- ZUFALL vor 5.03!!!
5.831 +val it = () : unit*)
5.832 +
5.833 +
5.834 +
5.835 +
5.836 +fun inst_abs thy (Const sT) = Const sT
5.837 + | inst_abs thy (Free sT) = Free sT
5.838 + | inst_abs thy (Bound n) = Bound n
5.839 + | inst_abs thy (Var iT) = Var iT
5.840 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
5.841 + let val b' = subst_bound (Free(v,T2),b);
5.842 + (*fun variant_abs: term.ML*)
5.843 + in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end
5.844 + | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
5.845 + | inst_abs thy t =
5.846 + (writeln("inst_abs: unchanged t= "^(Sign.string_of_term (sign_of thy) t));
5.847 + t);
5.848 +(*val scr =
5.849 + "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
5.850 + \ (let h_ = (hd o (filterVar f_)) eqs_; \
5.851 + \ e_1 = hd (dropWhile (ident h_) eqs_); \
5.852 + \ vs_ = dropWhile (ident f_) (Vars h_); \
5.853 + \ v_1 = hd (dropWhile (ident v_) vs_); \
5.854 + \ (s_1::bool list)=(SubProblem(DiffApp_,[univar,equation],[no_met])\
5.855 + \ [bool_ e_1, real_ v_1])\
5.856 + \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
5.857 +> val ttt = (term_of o the o (parse thy)) scr;
5.858 +> writeln(term2str ttt);
5.859 +> atomt ttt;
5.860 +*** -------------
5.861 +*** Const ( DiffApp.Make'_fun'_by'_explicit)
5.862 +*** . Free ( f_, )
5.863 +*** . Free ( v_, )
5.864 +*** . Free ( eqs_, )
5.865 +*** . Const ( Let)
5.866 +*** . . Const ( Fun.op o)
5.867 +*** . . . Const ( List.hd)
5.868 +*** . . . Const ( DiffApp.filterVar)
5.869 +*** . . . . Free ( f_, )
5.870 +*** . . . Free ( eqs_, )
5.871 +*** . . Abs( h_,..
5.872 +*** . . . Const ( Let)
5.873 +*** . . . . Const ( List.hd)
5.874 +*** . . . . . Const ( List.dropWhile)
5.875 +*** . . . . . . Const ( Atools.ident)
5.876 +*** . . . . . . . Bound 0 <---- Free ( h_, )
5.877 +*** . . . . . . Free ( eqs_, )
5.878 +*** . . . . Abs( e_1,..
5.879 +*** . . . . . Const ( Let)
5.880 +*** . . . . . . Const ( List.dropWhile)
5.881 +*** . . . . . . . Const ( Atools.ident)
5.882 +*** . . . . . . . . Free ( f_, )
5.883 +*** . . . . . . . Const ( Tools.Vars)
5.884 +*** . . . . . . . . Bound 1 <---- Free ( h_, )
5.885 +*** . . . . . . Abs( vs_,..
5.886 +*** . . . . . . . Const ( Let)
5.887 +*** . . . . . . . . Const ( List.hd)
5.888 +*** . . . . . . . . . Const ( List.dropWhile)
5.889 +*** . . . . . . . . . . Const ( Atools.ident)
5.890 +*** . . . . . . . . . . . Free ( v_, )
5.891 +*** . . . . . . . . . . Bound 0 <---- Free ( vs_, )
5.892 +*** . . . . . . . . Abs( v_1,..
5.893 +*** . . . . . . . . . Const ( Let)
5.894 +*** . . . . . . . . . . Const ( Script.SubProblem)
5.895 +*** . . . . . . . . . . . Const ( Pair)
5.896 +*** . . . . . . . . . . . . Free ( DiffApp_, )
5.897 +*** . . . . . . . . . . . . Const ( Pair)
5.898 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.899 +*** . . . . . . . . . . . . . . Free ( univar, )
5.900 +*** . . . . . . . . . . . . . . Const ( List.list.Cons)
5.901 +*** . . . . . . . . . . . . . . . Free ( equation, )
5.902 +*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
5.903 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.904 +*** . . . . . . . . . . . . . . Free ( no_met, )
5.905 +*** . . . . . . . . . . . . . . Const ( List.list.Nil)
5.906 +*** . . . . . . . . . . . Const ( List.list.Cons)
5.907 +*** . . . . . . . . . . . . Const ( Script.bool_)
5.908 +*** . . . . . . . . . . . . . Bound 2 <----- Free ( e_1, )
5.909 +*** . . . . . . . . . . . . Const ( List.list.Cons)
5.910 +*** . . . . . . . . . . . . . Const ( Script.real_)
5.911 +*** . . . . . . . . . . . . . . Bound 0 <----- Free ( v_1, )
5.912 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.913 +*** . . . . . . . . . . Abs( s_1,..
5.914 +*** . . . . . . . . . . . Const ( Script.Substitute)
5.915 +*** . . . . . . . . . . . . Const ( List.list.Cons)
5.916 +*** . . . . . . . . . . . . . Const ( Pair)
5.917 +*** . . . . . . . . . . . . . . Bound 1 <----- Free ( v_1, )
5.918 +*** . . . . . . . . . . . . . . Const ( Fun.op o)
5.919 +*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
5.920 +*** . . . . . . . . . . . . . . . Const ( List.hd)
5.921 +*** . . . . . . . . . . . . . . . Bound 0 <----- Free ( s_1, )
5.922 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.923 +*** . . . . . . . . . . . . Bound 4 <----- Free ( h_, )
5.924 +
5.925 +> val ttt' = inst_abs thy ttt;
5.926 +> writeln(term2str ttt');
5.927 +Script Make_fun_by_explicit f_ v_ eqs_ =
5.928 + ... as above ...
5.929 +> atomt ttt';
5.930 +*** -------------
5.931 +*** Const ( DiffApp.Make'_fun'_by'_explicit)
5.932 +*** . Free ( f_, )
5.933 +*** . Free ( v_, )
5.934 +*** . Free ( eqs_, )
5.935 +*** . Const ( Let)
5.936 +*** . . Const ( Fun.op o)
5.937 +*** . . . Const ( List.hd)
5.938 +*** . . . Const ( DiffApp.filterVar)
5.939 +*** . . . . Free ( f_, )
5.940 +*** . . . Free ( eqs_, )
5.941 +*** . . Abs( h_,..
5.942 +*** . . . Const ( Let)
5.943 +*** . . . . Const ( List.hd)
5.944 +*** . . . . . Const ( List.dropWhile)
5.945 +*** . . . . . . Const ( Atools.ident)
5.946 +*** . . . . . . . Free ( h_, ) <---- Bound 0
5.947 +*** . . . . . . Free ( eqs_, )
5.948 +*** . . . . Abs( e_1,..
5.949 +*** . . . . . Const ( Let)
5.950 +*** . . . . . . Const ( List.dropWhile)
5.951 +*** . . . . . . . Const ( Atools.ident)
5.952 +*** . . . . . . . . Free ( f_, )
5.953 +*** . . . . . . . Const ( Tools.Vars)
5.954 +*** . . . . . . . . Free ( h_, ) <---- Bound 1
5.955 +*** . . . . . . Abs( vs_,..
5.956 +*** . . . . . . . Const ( Let)
5.957 +*** . . . . . . . . Const ( List.hd)
5.958 +*** . . . . . . . . . Const ( List.dropWhile)
5.959 +*** . . . . . . . . . . Const ( Atools.ident)
5.960 +*** . . . . . . . . . . . Free ( v_, )
5.961 +*** . . . . . . . . . . Free ( vs_, ) <---- Bound 0
5.962 +*** . . . . . . . . Abs( v_1,..
5.963 +*** . . . . . . . . . Const ( Let)
5.964 +*** . . . . . . . . . . Const ( Script.SubProblem)
5.965 +*** . . . . . . . . . . . Const ( Pair)
5.966 +*** . . . . . . . . . . . . Free ( DiffApp_, )
5.967 +*** . . . . . . . . . . . . Const ( Pair)
5.968 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.969 +*** . . . . . . . . . . . . . . Free ( univar, )
5.970 +*** . . . . . . . . . . . . . . Const ( List.list.Cons)
5.971 +*** . . . . . . . . . . . . . . . Free ( equation, )
5.972 +*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
5.973 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
5.974 +*** . . . . . . . . . . . . . . Free ( no_met, )
5.975 +*** . . . . . . . . . . . . . . Const ( List.list.Nil)
5.976 +*** . . . . . . . . . . . Const ( List.list.Cons)
5.977 +*** . . . . . . . . . . . . Const ( Script.bool_)
5.978 +*** . . . . . . . . . . . . . Free ( e_1, ) <----- Bound 2
5.979 +*** . . . . . . . . . . . . Const ( List.list.Cons)
5.980 +*** . . . . . . . . . . . . . Const ( Script.real_)
5.981 +*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 0
5.982 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.983 +*** . . . . . . . . . . Abs( s_1,..
5.984 +*** . . . . . . . . . . . Const ( Script.Substitute)
5.985 +*** . . . . . . . . . . . . Const ( List.list.Cons)
5.986 +*** . . . . . . . . . . . . . Const ( Pair)
5.987 +*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 1
5.988 +*** . . . . . . . . . . . . . . Const ( Fun.op o)
5.989 +*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
5.990 +*** . . . . . . . . . . . . . . . Const ( List.hd)
5.991 +*** . . . . . . . . . . . . . . . Free ( s_1, ) <----- Bound 0
5.992 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
5.993 +*** . . . . . . . . . . . . Free ( h_, ) <----- Bound 4
5.994 +
5.995 +Note numbering of de Bruijn indexes !
5.996 +
5.997 +Script Make_fun_by_explicit f_ v_ eqs_ =
5.998 + let h_ = (hd o filterVar f_) eqs_;
5.999 + e_1 = hd (dropWhile (ident h_ BOUND_0) eqs_);
5.1000 + vs_ = dropWhile (ident f_) (Vars h_ BOUND_1);
5.1001 + v_1 = hd (dropWhile (ident v_) vs_ BOUND_0);
5.1002 + s_1 =
5.1003 + SubProblem (DiffApp_, [univar, equation], [no_met])
5.1004 + [bool_ e_1 BOUND_2, real_ v_1 BOUND_0]
5.1005 + in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4
5.1006 +*)
5.1007 +
5.1008 +
5.1009 +
5.1010 +
5.1011 +fun T_a2real (Type (s, [])) =
5.1012 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
5.1013 + | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
5.1014 + | T_a2real (TFree (s, srt)) =
5.1015 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
5.1016 + | T_a2real (TVar (("DUMMY",_),srt)) = HOLogic.realT;
5.1017 +
5.1018 +(*FIXME .. fixes the type (+see Typefix.thy*)
5.1019 +fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T))
5.1020 + | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
5.1021 + | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
5.1022 + | typ_a2real (Bound i) = (Bound i)
5.1023 + | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
5.1024 + | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
5.1025 +(*
5.1026 +----------------6.8.02---------------------------------------------------
5.1027 + val str = "1";
5.1028 + val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
5.1029 + atomty (term_of t);
5.1030 +*** -------------
5.1031 +*** Const ( 1, 'a)
5.1032 + val t = (app_num_tr' o term_of) t;
5.1033 + atomty t;
5.1034 +*** -------------
5.1035 +*** Const ( 1, 'a)
5.1036 + val t = typ_a2real t;
5.1037 + atomty t;
5.1038 +*** -------------
5.1039 +*** Const ( 1, real)
5.1040 +
5.1041 + val str = "2";
5.1042 + val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
5.1043 + atomty (term_of t);
5.1044 +*** -------------
5.1045 +*** Const ( Numeral.number_of, bin => 'a)
5.1046 +*** . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.1047 +*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.1048 +*** . . . Const ( Numeral.bin.Pls, bin)
5.1049 +*** . . . Const ( True, bool)
5.1050 +*** . . Const ( False, bool)
5.1051 + val t = (app_num_tr' o term_of) t;
5.1052 + atomty t;
5.1053 +*** -------------
5.1054 +*** Free ( 2, 'a)
5.1055 + val t = typ_a2real t;
5.1056 + atomty t;
5.1057 +*** -------------
5.1058 +*** Free ( 2, real)
5.1059 +----------------6.8.02---------------------------------------------------
5.1060 +
5.1061 +
5.1062 +> val str = "R";
5.1063 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
5.1064 +val t = Free ("R","?DUMMY") : term
5.1065 +> val t' = typ_a2real t;
5.1066 +> cterm_of (sign_of thy) t';
5.1067 +val it = "R::RealDef.real" : cterm
5.1068 +
5.1069 +> val str = "R=R";
5.1070 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
5.1071 +> atomty (typ_a2real t);
5.1072 +*** -------------
5.1073 +*** Const ( op =, [RealDef.real, RealDef.real] => bool)
5.1074 +*** Free ( R, RealDef.real)
5.1075 +*** Free ( R, RealDef.real)
5.1076 +> val t' = typ_a2real t;
5.1077 +> cterm_of (sign_of thy) t';
5.1078 +val it = "(R::RealDef.real) = R" : cterm
5.1079 +
5.1080 +> val str = "fixed_values [R=R]";
5.1081 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
5.1082 +> val t' = typ_a2real t;
5.1083 +> cterm_of (sign_of thy) t';
5.1084 +val it = "fixed_values [(R::RealDef.real) = R]" : cterm
5.1085 +*)
5.1086 +
5.1087 +(*TODO.WN0609: parse should return a term or a string
5.1088 + (or even more comprehensive datastructure for error-messages)
5.1089 + i.e. in wrapping with Some term or None the latter is not sufficient*)
5.1090 +fun parseold thy str =
5.1091 + (let
5.1092 + val sgn = sign_of thy;
5.1093 + val t = ((*typ_a2real o*) app_num_tr'1 o term_of)
5.1094 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
5.1095 + in Some (cterm_of sgn t) end)
5.1096 + handle _ => None;
5.1097 +fun parseN thy str =
5.1098 + (let
5.1099 + val sgn = sign_of thy;
5.1100 + val t = ((*typ_a2real o app_num_tr'1 o*) term_of)
5.1101 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
5.1102 + in Some (cterm_of sgn t) end)
5.1103 + handle _ => None;
5.1104 +
5.1105 +fun parse thy str =
5.1106 + (let
5.1107 + val sgn = sign_of thy;
5.1108 + val t = (typ_a2real o app_num_tr'1 o term_of)
5.1109 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
5.1110 + in Some (cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
5.1111 + handle _ => None;
5.1112 +(* 10.8.02: for this reason we still have ^^^--------------------
5.1113 + val thy = SqRoot.thy;
5.1114 + val str = "(1::real) ^ (2::nat)";
5.1115 + val sgn = sign_of thy;
5.1116 + val ct = (read_cterm sgn (str,(TVar(("DUMMY",0),[])))) handle e =>print_exn e;
5.1117 +(*1*)"(1::real) ^ 2";
5.1118 + atomty (term_of ct);
5.1119 +*** -------------
5.1120 +*** Const ( Nat.power, [real, nat] => real)
5.1121 +*** . Const ( 1, real)
5.1122 +*** . Const ( Numeral.number_of, bin => nat)
5.1123 +*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.1124 +*** . . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.1125 +*** . . . . Const ( Numeral.bin.Pls, bin)
5.1126 +*** . . . . Const ( True, bool)
5.1127 +*** . . . Const ( False, bool)
5.1128 + val t = ((app_num_tr' o term_of)
5.1129 + (read_cterm sgn (str,(TVar(("DUMMY",0),[])))))handle e => print_exn e;
5.1130 + val ct = (cterm_of sgn t) handle e => print_exn e;
5.1131 +(*2*)"(1::real) ^ (2::nat)";
5.1132 + atomty (term_of ct);
5.1133 +*** -------------
5.1134 +*** Const ( Nat.power, [real, nat] => real)
5.1135 +*** . Free ( 1, real)
5.1136 +*** . Free ( 2, nat) (*1*) Const("2",_) (*2*) Free("2",_)
5.1137 +
5.1138 +
5.1139 + val str = "(2::real) ^ (2::nat)";
5.1140 + val t = (read_cterm sgn (str,(TVar(("DUMMY",0),[])))) handle e => print_exn e;
5.1141 +val t = "(2::real) ^ 2" : cterm
5.1142 + val t = ((app_num_tr' o term_of)
5.1143 + (read_cterm sgn (str,(TVar(("DUMMY",0),[])))))handle e => print_exn e;
5.1144 + val ct = (cterm_of sgn t) handle e => print_exn e;
5.1145 +Variable "2" has two distinct types
5.1146 +real
5.1147 +nat
5.1148 +uncaught exception TYPE
5.1149 + raised at: sign.ML:672.26-673.56
5.1150 + goals.ML:1100.61
5.1151 +
5.1152 +
5.1153 + val str = "(3::real) ^ (2::nat)";
5.1154 + val t = (read_cterm sgn (str,(TVar(("DUMMY",0),[])))) handle e => print_exn e;
5.1155 +val t = "(3::real) ^ 2" : cterm
5.1156 + val t = ((app_num_tr' o term_of)
5.1157 + (read_cterm sgn (str,(TVar(("DUMMY",0),[])))))handle e => print_exn e;
5.1158 + val ct = (cterm_of sgn t) handle e => print_exn e;
5.1159 +val ct = "(3::real) ^ (2::nat)" : cterm
5.1160 +
5.1161 +
5.1162 +Conclusion: The type inference allows different types
5.1163 + for one and the same Numeral.number_of
5.1164 + BUT the type inference doesn't allow
5.1165 + Free ( 2, real) and Free ( 2, nat) within one term
5.1166 +--------------- ~~~~ ~~~ *)
5.1167 +(*
5.1168 +> val (Some ct) = parse thy "(-#5)^^^#3";
5.1169 +> atomty (term_of ct);
5.1170 +*** -------------
5.1171 +*** Const ( Nat.op ^, ['a, nat] => 'a)
5.1172 +*** Const ( uminus, 'a => 'a)
5.1173 +*** Free ( #5, 'a)
5.1174 +*** Free ( #3, nat)
5.1175 +> val (Some ct) = parse thy "R=R";
5.1176 +> atomty (term_of ct);
5.1177 +*** -------------
5.1178 +*** Const ( op =, [real, real] => bool)
5.1179 +*** Free ( R, real)
5.1180 +*** Free ( R, real)
5.1181 +
5.1182 +THIS IS THE OUTPUT FOR VERSION (3) above at typ_a2real !!!!!
5.1183 +*** -------------
5.1184 +*** Const ( op =, [RealDef.real, RealDef.real] => bool)
5.1185 +*** Free ( R, RealDef.real)
5.1186 +*** Free ( R, RealDef.real) *)
5.1187 +
5.1188 +(*version for testing local to theories*)
5.1189 +fun str2t thy str = (term_of o the o (parse thy )) str;
5.1190 +
5.1191 +fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str;
5.1192 +fun str2termN str = (term_of o the o (parseN (assoc_thy "Isac.thy"))) str;
5.1193 +fun strs2terms ss = map str2term ss;
5.1194 +
5.1195 +(*+ makes a substitution from the output of Pattern.match +*)
5.1196 +fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);
5.1197 +(*
5.1198 + val t = (term_of o the o (parse thy)) "1/a";
5.1199 + val pat = (term_of o the o (parse thy)) "?u/?v";
5.1200 + val (_,sbst) = (Pattern.match (Sign.tsig_of(sign_of thy)) (pat,t))
5.1201 + handle _ => ([],[]);
5.1202 + ([],
5.1203 + [(("v",0),Free ("a","RealDef.real")),(("u",0),Free ("1","RealDef.real"))])
5.1204 + : (indexname * typ) list * (indexname * term) list
5.1205 + val subst = map mk_subs sbst;
5.1206 + [(Free ("v","RealDef.real"),Free ("a","RealDef.real")),
5.1207 + (Free ("u","RealDef.real"),Free ("1","RealDef.real"))] : (term * term) list
5.1208 +*)
5.1209 +
5.1210 +
5.1211 +val atomthm = atomt o #prop o rep_thm;
5.1212 +
5.1213 +(*.instantiate #prop thm with bound variables (as Free).*)
5.1214 +fun inst_bdv [] t = t : term
5.1215 + | inst_bdv (instl: (term*term) list) t =
5.1216 + let fun subst (v as Var((s,_),T)) =
5.1217 + (case explode s of
5.1218 + "b"::"d"::"v"::_ =>
5.1219 + if_none (assoc(instl,Free(s,T))) (Free(s,T))
5.1220 + | _ => v)
5.1221 + | subst (Abs(a,T,body)) = Abs(a, T, subst body)
5.1222 + | subst (f$t') = subst f $ subst t'
5.1223 + | subst t = if_none (assoc(instl,t)) t
5.1224 + in subst t end;
5.1225 +
5.1226 +
5.1227 +(*WN050829 caution: is_atom (str2term"q_0/2 * L * x") = true !!!
5.1228 + use length (vars term) = 1 instead*)
5.1229 +fun is_atom (Const ("Float.Float",_) $ _) = true
5.1230 + | is_atom (Const ("ComplexI.I'_'_",_)) = true
5.1231 + | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
5.1232 + | is_atom (Const ("op +",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
5.1233 + | is_atom (Const ("op +",_) $ t1 $
5.1234 + (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
5.1235 + is_atom t1 andalso is_atom t2
5.1236 + | is_atom (Const _) = true
5.1237 + | is_atom (Free _) = true
5.1238 + | is_atom (Var _) = true
5.1239 + | is_atom _ = false;
5.1240 +(* val t = str2term "q_0/2 * L * x";
5.1241 +
5.1242 +
5.1243 +*)
5.1244 +(*val t = str2term "Float ((1,2),(0,0))";
5.1245 +> is_atom t;
5.1246 +val it = true : bool
5.1247 +> val t = str2term "Float ((1,2),(0,0)) * I__";
5.1248 +> is_atom t;
5.1249 +val it = true : bool
5.1250 +> val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
5.1251 +> is_atom t;
5.1252 +val it = true : bool
5.1253 +> val t = str2term "1 + 2*I__";
5.1254 +> val Const ("op +",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
5.1255 +*)
5.1256 +
5.1257 +(*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
5.1258 + have found a substitution (required for evaluating the preconditions
5.1259 + of _incomplete_ models).*)
5.1260 +fun subst_atomic_all [] t = (false, (*TODO may be 'true' for some terms ?*)
5.1261 + t : term)
5.1262 + | subst_atomic_all (instl: (term*term) list) t =
5.1263 + let fun subst (Abs(a,T,body)) =
5.1264 + let val (all, body') = subst body
5.1265 + in (all, Abs(a, T, body')) end
5.1266 + | subst (f$tt) =
5.1267 + let val (all1, f') = subst f
5.1268 + val (all2, tt') = subst tt
5.1269 + in (all1 andalso all2, f' $ tt') end
5.1270 + | subst (t as Free _) =
5.1271 + if is_num t then (true, t) (*numerals cannot be subst*)
5.1272 + else (case assoc(instl,t) of
5.1273 + Some t' => (true, t')
5.1274 + | None => (false, t))
5.1275 + | subst t = (true, if_none (assoc(instl,t)) t)
5.1276 + in subst t end;
6.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Thu Dec 27 12:25:27 2007 +0100
6.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Thu Dec 27 15:20:44 2007 +0100
6.3 @@ -44,7 +44,7 @@
6.4 if term2str t = "a + (b + (c + d))" then ()
6.5 else raise error "polyminus.sml 2 watch order_add_mult";
6.6
6.7 -"----- if parentheses are right, left_commute is (alsmost) sufficient...";
6.8 +"----- if parentheses are right, left_commute is (almost) sufficient...";
6.9 val t = str2term "a + (d + (c + b))";
6.10 "a + (d + (c + b))";
6.11 val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
6.12 @@ -58,60 +58,92 @@
6.13 "WN0712707 complicated monomials do not yet work ...";
6.14 val t = str2term "((5*a + 4*d) + 3*c) + 2*b";
6.15 val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
6.16 -"2 * b + (3 * c + (4 * d + 5 * a))"
6.17 +if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
6.18 +else raise error "polyminus.sml: order_add_mult changed";
6.19
6.20 +"----- here we see rew_sub going into subterm with ord.rew....";
6.21 +val od = ord_make_polynomial false Poly.thy;
6.22 +val t = str2term "b + a + c + d";
6.23 +val Some (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t;
6.24 +val Some (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t;
6.25 +(*@@@ rew_sub gosub: t = d + (b + a + c)
6.26 + @@@ rew_sub begin: t = b + a + c*)
6.27 +
6.28 +(*#####################################################################
6.29
6.30 "----------- build predicate for +- ordering ---------------------";
6.31 "----------- build predicate for +- ordering ---------------------";
6.32 "----------- build predicate for +- ordering ---------------------";
6.33 "a" < "b";
6.34 "ba" < "ab";
6.35 -"123" < "a";
6.36 +"123" < "a"; (*unused due to ---vvv*)
6.37 +"12" < "3"; (*true !!!*)
6.38
6.39 -" b kleiner a ==> (b + a) = (a + b)";
6.40 +" a kleiner b ==> (b + a) = (a + b)";
6.41 str2term "aaa";
6.42 str2term "222 * aaa";
6.43
6.44 +case eval_kleiner 0 0 (str2term "12 kleiner 9") 0 of
6.45 + Some ("12 kleiner 9 = False", _) => ()
6.46 + | _ => raise error "polyminus.sml: 12 kleiner 9 = False";
6.47 +
6.48 +case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
6.49 + Some ("a kleiner b = True", _) => ()
6.50 + | _ => raise error "polyminus.sml: a kleiner b = True";
6.51 +
6.52 +"----- test rewrite_, rewrite_set_";
6.53 +val od = dummy_ord;
6.54 +val erls = erls_ordne_alphabetisch;
6.55 +val t = str2term "b + a";
6.56 +"############################################";
6.57 +val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
6.58 +if term2str t = "a + b" then ()
6.59 +else raise error "polyminus.sml: ordne_alphabetisch1 b + a";
6.60 +
6.61 trace_rewrite:=true;
6.62 val t = str2term "b + a";
6.63 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
6.64 -"a + b";
6.65 +if term2str t = "a + b" then ()
6.66 +else raise error "polyminus.sml: ordne_alphabetisch a + b";
6.67
6.68 val t = str2term "2*b + a";
6.69 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
6.70 -"a + 2 * b";
6.71 +if term2str t = "a + 2 * b" then ()
6.72 +else raise error "polyminus.sml: ordne_alphabetisch a + 2 * b";
6.73
6.74 val t = str2term "a + c + b";
6.75 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
6.76 -"a + b + c";
6.77 +if term2str t = "a + b + c" then ()
6.78 +else raise error "polyminus.sml: ordne_alphabetisch a + b + c";
6.79 +
6.80 +"----- rewrite goes into subterms";
6.81 +val t = str2term "a + c + b + d";
6.82 +val Some (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t;
6.83 +if term2str t = "a + b + c + d" then ()
6.84 +else raise error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
6.85
6.86 val t = str2term "a + c + d + b";
6.87 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
6.88 -"a + c + b + d";(*?!?...*)
6.89 -
6.90 -"----- rewrite seems not to go into subterms";
6.91 -val od = ord_make_polynomial true Poly.thy;(*/////////not necessary*)
6.92 -val erls = erls_ordne_alphabetisch;
6.93 -val t = str2term "a + c + b + d";
6.94 -val Some (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t;
6.95 +if term2str t = "a + b + c + d" then ()
6.96 +else raise error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
6.97
6.98 "----- here we see rew_sub going into subterm with cond.rew....";
6.99 val t = str2term "b + a + c + d";
6.100 val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
6.101 +if term2str t = "a + b + c + d" then ()
6.102 +else raise error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
6.103
6.104 -"----- here we see rew_sub going into subterm with ord.rew....";
6.105 -val od = ord_make_polynomial false Poly.thy;
6.106 -val t = str2term "b + a + c + d";
6.107 -val Some (t,_) = rewrite_ thy od erls false real_add_commute t; term2str t;
6.108 -val Some (t,_) = rewrite_ thy od erls false real_add_commute t; term2str t;
6.109 -(*@@@ rew_sub gosub: t = d + (b + a + c)
6.110 - @@@ rew_sub begin: t = b + a + c*)
6.111 -
6.112 -
6.113 -
6.114 -
6.115 -(*WN071207 postponed: cannot identify what goes on...*)
6.116 +"----- compile rls for the most complicated terms";
6.117 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
6.118 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
6.119 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
6.120 -"5 * e - 8 * g + 6 * f - 9 - 7 * e + 10 * g - 4 * f + 12"'
6.121 \ No newline at end of file
6.122 +"5 * e - 8 * g + 6 * f - 9 - 7 * e + 10 * g - 4 * f + 12";
6.123 +
6.124 +
6.125 +trace_rewrite:=false;
6.126 +(*
6.127 +use"../smltest/IsacKnowledge/polyminus.sml";
6.128 +use"polyminus.sml";
6.129 + *)
6.130 +
6.131 +#####################################################################*)