1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Sep 27 13:35:06 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Sep 28 07:28:10 2010 +0200
1.3 @@ -24,7 +24,7 @@
1.4 use "calcelems.sml"
1.5 ML {* check_guhs_unique := true *}
1.6
1.7 -use "ProgLang/term.sml"
1.8 +use "ProgLang/termC.sml"
1.9 use "ProgLang/calculate.sml"
1.10 use "ProgLang/rewrite.sml"
1.11 use_thy"ProgLang/Script" (*ListC, Tools, Script*)
2.1 --- a/src/Tools/isac/Build_Test_Isac.thy Mon Sep 27 13:35:06 2010 +0200
2.2 +++ b/src/Tools/isac/Build_Test_Isac.thy Tue Sep 28 07:28:10 2010 +0200
2.3 @@ -24,7 +24,7 @@
2.4 use "calcelems.sml"
2.5 ML {* check_guhs_unique := true *}
2.6
2.7 -use "ProgLang/term.sml"
2.8 +use "ProgLang/termC.sml"
2.9 use "ProgLang/calculate.sml"
2.10 use "ProgLang/rewrite.sml"
2.11 use_thy"ProgLang/Script" (*ListC, Tools, Script*)
3.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Mon Sep 27 13:35:06 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 07:28:10 2010 +0200
3.3 @@ -20,7 +20,7 @@
3.4 ---------------------------------------------------------------------*)
3.5
3.6
3.7 -(*diese vvv funktionen kommen nach src/Isa99/term.sml -------------*)
3.8 +(*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*)
3.9 fun term2str t =
3.10 let fun ato (Const(a,T)) n =
3.11 "\n"^indent n^"Const ( "^a^")"
3.12 @@ -37,7 +37,7 @@
3.13 fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
3.14 handle _ => raise error ("free2int: "^term2str t))
3.15 | free2int t = raise error ("free2int: "^term2str t);
3.16 -(*diese ^^^ funktionen kommen nach src/Isa99/term.sml -------------*)
3.17 +(*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*)
3.18
3.19
3.20 (* remark on exceptions: 'error' is implemented by Isabelle
4.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Sep 27 13:35:06 2010 +0200
4.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Sep 28 07:28:10 2010 +0200
4.3 @@ -5,12 +5,12 @@
4.4
4.5 theory ListC imports Complex_Main
4.6 uses ("library.sml")("calcelems.sml")
4.7 -("ProgLang/term.sml")("ProgLang/calculate.sml")
4.8 +("ProgLang/termC.sml")("ProgLang/calculate.sml")
4.9 ("ProgLang/rewrite.sml")
4.10 begin
4.11 use "library.sml" (*indent,...*)
4.12 use "calcelems.sml" (*str_of_type, Thm,...*)
4.13 -use "ProgLang/term.sml" (*num_str,...*)
4.14 +use "ProgLang/termC.sml" (*num_str,...*)
4.15 use "ProgLang/calculate.sml" (*???*)
4.16 use "ProgLang/rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*)
4.17
5.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 27 13:35:06 2010 +0200
5.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 07:28:10 2010 +0200
5.3 @@ -272,30 +272,30 @@
5.4 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
5.5 (*end*);
5.6
5.7 -(* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t);
5.8 - *)
5.9 -(*.rewrite using a list of terms.*)
5.10 -fun rewrite_terms_ thy ord erls subte t =
5.11 - let (*val _=tracing("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
5.12 - term_detail2str (hd subte)^
5.13 +(* given a list of equalities (lhs = rhs) and a term,
5.14 + replace all occurrences of lhs in the term with rhs;
5.15 + thus the order or equalities matters: put variables in lhs first. *)
5.16 +fun rewrite_terms_ thy ord erls equs t =
5.17 + let (*val _=tracing("### rewrite_terms_ equs= '"^terms2str equs^"' ..."^
5.18 + term_detail2str (hd equs)^
5.19 "### rewrite_terms_ t= '"^term2str t^"' ..."^
5.20 term_detail2str t);*)
5.21 fun rew_ (t', asm') [] _ = (t', asm')
5.22 - (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t);
5.23 + (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], equs, t);
5.24 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
5.25 rew_ (t', asm') (r::rs) t;
5.26 *)
5.27 | rew_ (t', asm') (rules as r::rs) t =
5.28 let val _ = tracing("rew_ "^term2str t);
5.29 val (t'', asm'', lrd, rew) =
5.30 - rew_sub thy 1 [] ord erls false [] r t
5.31 + rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
5.32 in if rew
5.33 - then (tracing("true rew_ "^term2str t'');
5.34 + then (tracing ("true rew_ " ^ term2str t'');
5.35 rew_ (t'', asm' @ asm'') rules t'')
5.36 - else (tracing("false rew_ "^term2str t'');
5.37 + else (tracing ("false rew_ " ^ term2str t'');
5.38 rew_ (t', asm') rs t')
5.39 end
5.40 - val (t'', asm'') = rew_ (e_term, []) subte t
5.41 + val (t'', asm'') = rew_ (e_term, []) equs t
5.42 in if t'' = e_term
5.43 then NONE else SOME (t'', asm'')
5.44 end;
6.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Mon Sep 27 13:35:06 2010 +0200
6.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Tue Sep 28 07:28:10 2010 +0200
6.3 @@ -1,4 +1,4 @@
6.4 -(* tools which depend on Script.thy and thus are not in term.sml
6.5 +(* tools which depend on Script.thy and thus are not in termC.sml
6.6 (c) Walther Neuper 2000
6.7
6.8 use"ProgLang/scrtools.sml";
7.1 --- a/src/Tools/isac/ProgLang/term.sml Mon Sep 27 13:35:06 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,1219 +0,0 @@
7.4 -(* extends Isabelle/src/Pure/term.ML
7.5 - (c) Walther Neuper 1999
7.6 -
7.7 -use"ProgLang/term.sml";
7.8 -use"term.sml";
7.9 -*)
7.10 -
7.11 -(*
7.12 -> (cterm_of thy) a_term;
7.13 -val it = "empty" : cterm *)
7.14 -
7.15 -(*2003 fun match thy t pat =
7.16 - (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
7.17 - handle _ => [];
7.18 -fn : theory ->
7.19 - Term.term -> Term.term -> (Term.indexname * Term.term) list*)
7.20 -(*see src/Tools/eqsubst.ML fun clean_match*)
7.21 -(*2003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
7.22 -fun matches thy tm pa =
7.23 - (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
7.24 - handle _ => false
7.25 -
7.26 -fun atomtyp t = (*WN10 see raw_pp_typ*)
7.27 - let
7.28 - fun ato n (Type (s,[])) =
7.29 - ("\n*** "^indent n^"Type ("^s^",[])")
7.30 - | ato n (Type (s,Ts)) =
7.31 - ("\n*** "^indent n^"Type ("^s^",["^ atol (n+1) Ts)
7.32 -
7.33 - | ato n (TFree (s,sort)) =
7.34 - ("\n*** "^indent n^"TFree ("^s^",["^ strs2str' sort)
7.35 -
7.36 - | ato n (TVar ((s,i),sort)) =
7.37 - ("\n*** "^indent n^"TVar (("^s^","^
7.38 - string_of_int i ^ strs2str' sort)
7.39 - and atol n [] =
7.40 - ("\n*** "^indent n^"]")
7.41 - | atol n (T::Ts) = (ato n T ^ atol n Ts)
7.42 -(*in print (ato 0 t ^ "\n") end; TODO TUM10*)
7.43 -in tracing (ato 0 t) end;
7.44 -(*
7.45 -> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
7.46 -> atomtyp T;
7.47 -*** Type (fun,[
7.48 -*** Type (RealDef.real,[])
7.49 -*** Type (fun,[
7.50 -*** Type (IntDef.int,[])
7.51 -*** Type (nat,[])
7.52 -*** ]
7.53 -*** ]
7.54 -*)
7.55 -
7.56 -(*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*)
7.57 -local
7.58 - fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
7.59 - fun pp_list xs = Pretty.list "[" "]" xs
7.60 - fun pp_str s = Pretty.str s
7.61 - fun pp_qstr s = Pretty.quote (pp_str s)
7.62 - fun pp_int i = pp_str (string_of_int i)
7.63 - fun pp_sort S = pp_list (map pp_qstr S)
7.64 - fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
7.65 -in
7.66 -fun raw_pp_typ (TVar ((a, i), S)) =
7.67 - pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
7.68 - | raw_pp_typ (TFree (a, S)) =
7.69 - pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
7.70 - | raw_pp_typ (Type (a, tys)) =
7.71 - pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
7.72 -end
7.73 -(* install
7.74 -PolyML.addPrettyPrinter
7.75 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
7.76 -de-install
7.77 -PolyML.addPrettyPrinter
7.78 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
7.79 -*)
7.80 -
7.81 -fun atomt t =
7.82 - let fun ato (Const (a, _)) n =
7.83 - "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
7.84 - | ato (Free (a, _)) n =
7.85 - "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
7.86 - | ato (Var ((a, i), _)) n =
7.87 - "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^
7.88 - string_of_int i ^ "), _)"
7.89 - | ato (Bound i) n =
7.90 - "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
7.91 - | ato (Abs (a, _, body)) n =
7.92 - "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
7.93 - | ato (f $ t) n = (ato f n ^ ato t (n + 1))
7.94 - in tracing ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
7.95 -
7.96 -fun term_detail2str t =
7.97 - let fun ato (Const (a, T)) n =
7.98 - "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")"
7.99 - | ato (Free (a, T)) n =
7.100 - "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")"
7.101 - | ato (Var ((a, i), T)) n =
7.102 - "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^
7.103 - string_of_typ T ^ ")"
7.104 - | ato (Bound i) n =
7.105 - "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
7.106 - | ato (Abs(a, T, body)) n =
7.107 - "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.."
7.108 - ^ ato body (n + 1)
7.109 - | ato (f $ t) n = ato f n ^ ato t (n + 1)
7.110 - in "\n*** " ^ ato t 0 ^ "\n***" end;
7.111 -fun atomty t = (tracing o term_detail2str) t; (*WN100907 broken*)
7.112 -
7.113 -fun term_str thy (Const(s,_)) = s
7.114 - | term_str thy (Free(s,_)) = s
7.115 - | term_str thy (Var((s,i),_)) = s^(string_of_int i)
7.116 - | term_str thy (Bound i) = "B."^(string_of_int i)
7.117 - | term_str thy (Abs(s,_,_)) = s
7.118 - | term_str thy t = raise error("term_str not for "^term2str t);
7.119 -
7.120 -(*.contains the fst argument the second argument (a leave! of term).*)
7.121 -fun contains_term (Abs(_,_,body)) t = contains_term body t
7.122 - | contains_term (f $ f') t =
7.123 - contains_term f t orelse contains_term f' t
7.124 - | contains_term s t = t = s;
7.125 -(*.contains the term a VAR(("*",_),_) ?.*)
7.126 -fun contains_Var (Abs(_,_,body)) = contains_Var body
7.127 - | contains_Var (f $ f') = contains_Var f orelse contains_Var f'
7.128 - | contains_Var (Var _) = true
7.129 - | contains_Var _ = false;
7.130 -(* contains_Var (str2term "?z = 3") (*true*);
7.131 - contains_Var (str2term "z = 3") (*false*);
7.132 - *)
7.133 -
7.134 -(*fun int_of_str str =
7.135 - let val ss = explode str
7.136 - val str' = case ss of
7.137 - "("::s => drop_last s | _ => ss
7.138 - in case BasisLibrary.Int.fromString (implode str') of
7.139 - SOME i => SOME i
7.140 - | NONE => NONE end;*)
7.141 -fun int_of_str str =
7.142 - let val ss = explode str
7.143 - val str' = case ss of
7.144 - "("::s => drop_last s | _ => ss
7.145 - in (SOME (Thy_Output.integer (implode str'))) handle _ => NONE end;
7.146 -(*
7.147 -> int_of_str "123";
7.148 -val it = SOME 123 : int option
7.149 -> int_of_str "(-123)";
7.150 -val it = SOME 123 : int option
7.151 -> int_of_str "#123";
7.152 -val it = NONE : int option
7.153 -> int_of_str "-123";
7.154 -val it = SOME ~123 : int option
7.155 -*)
7.156 -fun int_of_str' str =
7.157 - case int_of_str str of
7.158 - SOME i => i
7.159 - | NONE => raise TERM ("int_of_string: no int-string",[]);
7.160 -val str2int = int_of_str';
7.161 -
7.162 -fun is_numeral str = case int_of_str str of
7.163 - SOME _ => true
7.164 - | NONE => false;
7.165 -val is_no = is_numeral;
7.166 -fun is_num (Free (s,_)) = if is_numeral s then true else false
7.167 - | is_num _ = false;
7.168 -(*>
7.169 -> is_num ((term_of o the o (parse thy)) "#1");
7.170 -val it = true : bool
7.171 -> is_num ((term_of o the o (parse thy)) "#-1");
7.172 -val it = true : bool
7.173 -> is_num ((term_of o the o (parse thy)) "a123");
7.174 -val it = false : bool
7.175 -*)
7.176 -
7.177 -(*fun int_of_Free (Free (intstr, _)) =
7.178 - (case BasisLibrary.Int.fromString intstr of
7.179 - SOME i => i
7.180 - | NONE => raise error ("int_of_Free ( "^ intstr ^", _)"))
7.181 - | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");*)
7.182 -fun int_of_Free (Free (intstr, _)) = (Thy_Output.integer intstr
7.183 - handle _ => raise error ("int_of_Free ( "^ intstr ^", _)"))
7.184 - | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");
7.185 -
7.186 -fun vars t =
7.187 - let
7.188 - fun scan vs (Const(s,T)) = vs
7.189 - | scan vs (t as Free(s,T)) = if is_no s then vs else t::vs
7.190 - | scan vs (t as Var((s,i),T)) = t::vs
7.191 - | scan vs (Bound i) = vs
7.192 - | scan vs (Abs(s,T,t)) = scan vs t
7.193 - | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
7.194 - in (distinct o (scan [])) t end;
7.195 -
7.196 -fun is_Free (Free _) = true
7.197 - | is_Free _ = false;
7.198 -fun is_fun_id (Const _) = true
7.199 - | is_fun_id (Free _) = true
7.200 - | is_fun_id _ = false;
7.201 -fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
7.202 - | is_f_x _ = false;
7.203 -(* is_f_x (str2term "q_0/2 * L * x") (*false*);
7.204 - is_f_x (str2term "M_b x") (*true*);
7.205 - *)
7.206 -fun vars_str t =
7.207 - let
7.208 - fun scan vs (Const(s,T)) = vs
7.209 - | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
7.210 - | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
7.211 - | scan vs (Bound i) = vs
7.212 - | scan vs (Abs(s,T,t)) = scan vs t
7.213 - | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
7.214 - in (distinct o (scan [])) t end;
7.215 -
7.216 -fun ids2str t =
7.217 - let
7.218 - fun scan vs (Const(s,T)) = if is_no s then vs else s::vs
7.219 - | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
7.220 - | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
7.221 - | scan vs (Bound i) = vs
7.222 - | scan vs (Abs(s,T,t)) = scan (s::vs) t
7.223 - | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
7.224 - in (distinct o (scan [])) t end;
7.225 -fun is_bdv str =
7.226 - case explode str of
7.227 - "b"::"d"::"v"::_ => true
7.228 - | _ => false;
7.229 -fun is_bdv_ (Free (s,_)) = is_bdv s
7.230 - | is_bdv_ _ = false;
7.231 -
7.232 -fun free2str (Free (s,_)) = s
7.233 - | free2str t = raise error ("free2str not for "^ term2str t);
7.234 -fun free2int (t as Free (s, _)) = ((str2int s)
7.235 - handle _ => raise error ("free2int: "^term_detail2str t))
7.236 - | free2int t = raise error ("free2int: "^term_detail2str t);
7.237 -
7.238 -(*27.8.01: unused*)
7.239 -fun var2free (t as Const(s,T)) = t
7.240 - | var2free (t as Free(s,T)) = t
7.241 - | var2free (Var((s,i),T)) = Free(s,T)
7.242 - | var2free (t as Bound i) = t
7.243 - | var2free (Abs(s,T,t)) = Abs(s,T,var2free t)
7.244 - | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
7.245 -
7.246 -(*27.8.01: doesn't find some subterm ???!???*)
7.247 -(*2010 Logic.varify !!!*)
7.248 -fun free2var (t as Const(s,T)) = t
7.249 - | free2var (t as Free(s,T)) = if is_no s then t else Var((s,0),T)
7.250 - | free2var (t as Var((s,i),T)) = t
7.251 - | free2var (t as Bound i) = t
7.252 - | free2var (Abs(s,T,t)) = Abs(s,T,free2var t)
7.253 - | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
7.254 -
7.255 -
7.256 -fun mk_listT T = Type ("List.list", [T]);
7.257 -fun list_const T =
7.258 - Const("List.list.Cons", [T, mk_listT T] ---> mk_listT T);
7.259 -(*28.8.01: TODO: get type from head of list: 1 arg less!!!*)
7.260 -fun list2isalist T [] = Const("List.list.Nil",mk_listT T)
7.261 - | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts);
7.262 -(*
7.263 -> val tt = (term_of o the o (parse thy)) "R=(R::real)";
7.264 -> val TT = type_of tt;
7.265 -> val ss = list2isalist TT [tt,tt,tt];
7.266 -> (cterm_of thy) ss;
7.267 -val it = "[R = R, R = R, R = R]" : cterm *)
7.268 -
7.269 -fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
7.270 - | isapair2pair t =
7.271 - raise error ("isapair2pair called with "^term2str t);
7.272 -
7.273 -val listType = Type ("List.list",[Type ("bool",[])]);
7.274 -fun isalist2list ls =
7.275 - let
7.276 - fun get es (Const("List.list.Cons",_) $ t $ ls) = get (t::es) ls
7.277 - | get es (Const("List.list.Nil",_)) = es
7.278 - | get _ t =
7.279 - raise error ("isalist2list applied to NON-list '"^term2str t^"'")
7.280 - in (rev o (get [])) ls end;
7.281 -(*
7.282 -> val il = str2term "[a=b,c=d,e=f]";
7.283 -> val l = isalist2list il;
7.284 -> (tracing o terms2str) l;
7.285 -["a = b","c = d","e = f"]
7.286 -
7.287 -> val il = str2term "ss___::bool list";
7.288 -> val l = isalist2list il;
7.289 -[Free ("ss___", "bool List.list")]
7.290 -*)
7.291 -
7.292 -
7.293 -(*review Isabelle2009/src/HOL/Tools/hologic.ML*)
7.294 -val prop = Type ("prop",[]); (* ~/Diss.99/Integers-Isa/tools.sml*)
7.295 -val bool = Type ("bool",[]); (* 2002 Integ.int *)
7.296 -val Trueprop = Const("Trueprop",bool-->prop);
7.297 -fun mk_prop t = Trueprop $ t;
7.298 -val true_as_term = Const("True",bool);
7.299 -val false_as_term = Const("False",bool);
7.300 -val true_as_cterm = cterm_of (theory "HOL") true_as_term;
7.301 -val false_as_cterm = cterm_of (theory "HOL") false_as_term;
7.302 -
7.303 -infixr 5 -->; (*2002 /Pure/term.ML *)
7.304 -infixr --->; (*2002 /Pure/term.ML *)
7.305 -fun S --> T = Type("fun",[S,T]); (*2002 /Pure/term.ML *)
7.306 -val op ---> = foldr (op -->); (*2002 /Pure/term.ML *)
7.307 -fun list_implies ([], B) = B : term (*2002 /term.ML *)
7.308 - | list_implies (A::AS, B) = Logic.implies $ A $ list_implies(AS,B);
7.309 -
7.310 -
7.311 -
7.312 -(** substitution **)
7.313 -
7.314 -fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = (* = thm.ML *)
7.315 - match_bvs(s, t, if x="" orelse y="" then al
7.316 - else (x,y)::al)
7.317 - | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
7.318 - | match_bvs(_,_,al) = al;
7.319 -fun ren_inst(insts,prop,pat,obj) = (* = thm.ML *)
7.320 - let val ren = match_bvs(pat,obj,[])
7.321 - fun renAbs(Abs(x,T,b)) =
7.322 - Abs(case assoc_string(ren,x) of NONE => x
7.323 - | SOME(y) => y, T, renAbs(b))
7.324 - | renAbs(f$t) = renAbs(f) $ renAbs(t)
7.325 - | renAbs(t) = t
7.326 - in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
7.327 -
7.328 -
7.329 -
7.330 -
7.331 -
7.332 -
7.333 -fun dest_equals' (Const("op =",_) $ t $ u) = (t,u)(* logic.ML: Const("=="*)
7.334 - | dest_equals' t = raise TERM("dest_equals'", [t]);
7.335 -val lhs_ = (fst o dest_equals');
7.336 -val rhs_ = (snd o dest_equals');
7.337 -
7.338 -fun is_equality (Const("op =",_) $ t $ u) = true (* logic.ML: Const("=="*)
7.339 - | is_equality _ = false;
7.340 -fun mk_equality (t,u) = (Const("op =",[type_of t,type_of u]--->bool) $ t $ u);
7.341 -fun is_expliceq (Const("op =",_) $ (Free _) $ u) = true
7.342 - | is_expliceq _ = false;
7.343 -fun strip_trueprop (Const("Trueprop",_) $ t) = t
7.344 - | strip_trueprop t = t;
7.345 -(* | strip_trueprop t = raise TERM("strip_trueprop", [t]);
7.346 -*)
7.347 -
7.348 -(*.(A1==>...An==>B) goes to (A1==>...An==>).*)
7.349 -fun strip_imp_prems' (Const("==>", T) $ A $ t) =
7.350 - let fun coll_prems As (Const("==>", _) $ A $ t) =
7.351 - coll_prems (As $ (Logic.implies $ A)) t
7.352 - | coll_prems As _ = SOME As
7.353 - in coll_prems (Logic.implies $ A) t end
7.354 - | strip_imp_prems' _ = NONE; (* logic.ML: term -> term list*)
7.355 -(*
7.356 - val thm = real_mult_div_cancel1;
7.357 - val prop = (#prop o rep_thm) thm;
7.358 - atomt prop;
7.359 -*** -------------
7.360 -*** Const ( ==>)
7.361 -*** . Const ( Trueprop)
7.362 -*** . . Const ( Not)
7.363 -*** . . . Const ( op =)
7.364 -*** . . . . Var ((k, 0), )
7.365 -*** . . . . Const ( 0)
7.366 -*** . Const ( Trueprop)
7.367 -*** . . Const ( op =) *** .............
7.368 - val SOME t = strip_imp_prems' ((#prop o rep_thm) thm);
7.369 - atomt t;
7.370 -*** -------------
7.371 -*** Const ( ==>)
7.372 -*** . Const ( Trueprop)
7.373 -*** . . Const ( Not)
7.374 -*** . . . Const ( op =)
7.375 -*** . . . . Var ((k, 0), )
7.376 -*** . . . . Const ( 0)
7.377 -
7.378 - val thm = real_le_anti_sym;
7.379 - val prop = (#prop o rep_thm) thm;
7.380 - atomt prop;
7.381 -*** -------------
7.382 -*** Const ( ==>)
7.383 -*** . Const ( Trueprop)
7.384 -*** . . Const ( op <=)
7.385 -*** . . . Var ((z, 0), )
7.386 -*** . . . Var ((w, 0), )
7.387 -*** . Const ( ==>)
7.388 -*** . . Const ( Trueprop)
7.389 -*** . . . Const ( op <=)
7.390 -*** . . . . Var ((w, 0), )
7.391 -*** . . . . Var ((z, 0), )
7.392 -*** . . Const ( Trueprop)
7.393 -*** . . . Const ( op =)
7.394 -*** .............
7.395 - val SOME t = strip_imp_prems' ((#prop o rep_thm) thm);
7.396 - atomt t;
7.397 -*** -------------
7.398 -*** Const ( ==>)
7.399 -*** . Const ( Trueprop)
7.400 -*** . . Const ( op <=)
7.401 -*** . . . Var ((z, 0), )
7.402 -*** . . . Var ((w, 0), )
7.403 -*** . Const ( ==>)
7.404 -*** . . Const ( Trueprop)
7.405 -*** . . . Const ( op <=)
7.406 -*** . . . . Var ((w, 0), )
7.407 -*** . . . . Var ((z, 0), )
7.408 -*)
7.409 -
7.410 -(*. (A1==>...An==>) (B) goes to (A1==>...An==>B), where B is lowest branch.*)
7.411 -fun ins_concl (Const("==>", T) $ A $ t) B = Logic.implies $ A $ (ins_concl t B)
7.412 - | ins_concl (Const("==>", T) $ A ) B = Logic.implies $ A $ B
7.413 - | ins_concl t B = raise TERM("ins_concl", [t, B]);
7.414 -(*
7.415 - val thm = real_le_anti_sym;
7.416 - val prop = (#prop o rep_thm) thm;
7.417 - val concl = Logic.strip_imp_concl prop;
7.418 - val SOME prems = strip_imp_prems' prop;
7.419 - val prop' = ins_concl prems concl;
7.420 - prop = prop';
7.421 - atomt prop;
7.422 - atomt prop';
7.423 -*)
7.424 -
7.425 -
7.426 -fun vperm (Var _, Var _) = true (*2002 Pure/thm.ML *)
7.427 - | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
7.428 - | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
7.429 - | vperm (t, u) = (t = u);
7.430 -
7.431 -(*2002 cp from Pure/term.ML --- since 2009 in Pure/old_term.ML*)
7.432 -fun mem_term (_, []) = false
7.433 - | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
7.434 -fun subset_term ([], ys) = true
7.435 - | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
7.436 -fun eq_set_term (xs, ys) =
7.437 - xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
7.438 -(*a total, irreflexive ordering on index names*)
7.439 -fun xless ((a,i), (b,j): indexname) = i<j orelse (i=j andalso a<b);
7.440 -(*a partial ordering (not reflexive) for atomic terms*)
7.441 -fun atless (Const (a,_), Const (b,_)) = a<b
7.442 - | atless (Free (a,_), Free (b,_)) = a<b
7.443 - | atless (Var(v,_), Var(w,_)) = xless(v,w)
7.444 - | atless (Bound i, Bound j) = i<j
7.445 - | atless _ = false;
7.446 -(*insert atomic term into partially sorted list, suppressing duplicates (?)*)
7.447 -fun insert_aterm (t,us) =
7.448 - let fun inserta [] = [t]
7.449 - | inserta (us as u::us') =
7.450 - if atless(t,u) then t::us
7.451 - else if t=u then us (*duplicate*)
7.452 - else u :: inserta(us')
7.453 - in inserta us end;
7.454 -
7.455 -(*Accumulates the Vars in the term, suppressing duplicates*)
7.456 -fun add_term_vars (t, vars: term list) = case t of
7.457 - Var _ => insert_aterm(t,vars)
7.458 - | Abs (_,_,body) => add_term_vars(body,vars)
7.459 - | f$t => add_term_vars (f, add_term_vars(t, vars))
7.460 - | _ => vars;
7.461 -fun term_vars t = add_term_vars(t,[]);
7.462 -
7.463 -
7.464 -fun var_perm (t, u) = (*2002 Pure/thm.ML *)
7.465 - vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
7.466 -
7.467 -(*2002 fun decomp_simp, Pure/thm.ML *)
7.468 -fun perm lhs rhs = var_perm (lhs, rhs) andalso not (lhs aconv rhs)
7.469 - andalso not (is_Var lhs);
7.470 -
7.471 -
7.472 -fun str_of_int n =
7.473 - if n < 0 then "-"^((string_of_int o abs) n)
7.474 - else string_of_int n;
7.475 -(*
7.476 -> str_of_int 1;
7.477 -val it = "1" : string > str_of_int ~1;
7.478 -val it = "-1" : string
7.479 -*)
7.480 -
7.481 -
7.482 -fun power b 0 = 1
7.483 - | power b n =
7.484 - if n>0 then b*(power b (n-1))
7.485 - else raise error ("power "^(str_of_int b)^" "^(str_of_int n));
7.486 -(*
7.487 -> power 2 3;
7.488 -val it = 8 : int
7.489 -> power ~2 3;
7.490 -val it = ~8 : int
7.491 -> power ~3 2;
7.492 -val it = 9 : int
7.493 -> power 3 ~2;
7.494 -*)
7.495 -fun gcd 0 b = b
7.496 - | gcd a b = if a < b then gcd (b mod a) a
7.497 - else gcd (a mod b) b;
7.498 -fun sign n = if n < 0 then ~1
7.499 - else if n = 0 then 0 else 1;
7.500 -fun sign2 n1 n2 = (sign n1) * (sign n2);
7.501 -
7.502 -infix dvd;
7.503 -fun d dvd n = n mod d = 0;
7.504 -
7.505 -fun divisors n =
7.506 - let fun pdiv ds d n =
7.507 - if d=n then d::ds
7.508 - else if d dvd n then pdiv (d::ds) d (n div d)
7.509 - else pdiv ds (d+1) n
7.510 - in pdiv [] 2 n end;
7.511 -
7.512 -divisors 30;
7.513 -divisors 32;
7.514 -divisors 60;
7.515 -divisors 11;
7.516 -
7.517 -fun doubles ds = (* ds is ordered *)
7.518 - let fun dbls ds [] = ds
7.519 - | dbls ds [i] = ds
7.520 - | dbls ds (i::i'::is) = if i=i' then dbls (i::ds) is
7.521 - else dbls ds (i'::is)
7.522 - in dbls [] ds end;
7.523 -(*> doubles [2,3,4];
7.524 -val it = [] : int list
7.525 -> doubles [2,3,3,5,5,7];
7.526 -val it = [5,3] : int list*)
7.527 -
7.528 -fun squfact 0 = 0
7.529 - | squfact 1 = 1
7.530 - | squfact n = foldl op* (1, (doubles o divisors) n);
7.531 -(*> squfact 30;
7.532 -val it = 1 : int
7.533 -> squfact 32;
7.534 -val it = 4 : int
7.535 -> squfact 60;
7.536 -val it = 2 : int
7.537 -> squfact 11;
7.538 -val it = 1 : int*)
7.539 -
7.540 -
7.541 -fun dest_type (Type(T,[])) = T
7.542 - | dest_type T =
7.543 - (atomtyp T;
7.544 - raise error ("... dest_type: not impl. for this type"));
7.545 -
7.546 -fun term_of_num ntyp n = Free (str_of_int n, ntyp);
7.547 -
7.548 -fun pairT T1 T2 = Type ("*", [T1, T2]);
7.549 -(*> val t = str2term "(1,2)";
7.550 -> type_of t = pairT HOLogic.realT HOLogic.realT;
7.551 -val it = true : bool
7.552 -*)
7.553 -fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
7.554 -(*> val t = str2term "(1,2)";
7.555 -> val Const ("Pair",pT) $ _ $ _ = t;
7.556 -> pT = PairT HOLogic.realT HOLogic.realT;
7.557 -val it = true : bool
7.558 -*)
7.559 -fun pairt t1 t2 =
7.560 - Const ("Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
7.561 -(*> val t = str2term "(1,2)";
7.562 -> val (t1, t2) = (str2term "1", str2term "2");
7.563 -> t = pairt t1 t2;
7.564 -val it = true : bool*)
7.565 -
7.566 -
7.567 -fun num_of_term (t as Free (s,_)) =
7.568 - (case int_of_str s of
7.569 - SOME s' => s'
7.570 - | NONE => raise error ("num_of_term not for "^ term2str t))
7.571 - | num_of_term t = raise error ("num_of_term not for "^term2str t);
7.572 -
7.573 -fun mk_factroot op_(*=thy.sqrt*) T fact root =
7.574 - Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
7.575 - (Const (op_, T --> T) $ term_of_num T root);
7.576 -(*
7.577 -val T = (type_of o term_of o the) (parse thy "#12::real");
7.578 -val t = mk_factroot "SqRoot.sqrt" T 2 3;
7.579 -(cterm_of thy) t;
7.580 -val it = "#2 * sqrt #3 " : cterm
7.581 -*)
7.582 -fun var_op_num v op_ optype ntyp n =
7.583 - Const (op_, optype) $ v $
7.584 - Free (str_of_int n, ntyp);
7.585 -
7.586 -fun num_op_var v op_ optype ntyp n =
7.587 - Const (op_,optype) $
7.588 - Free (str_of_int n, ntyp) $ v;
7.589 -
7.590 -fun num_op_num T1 T2 (op_,Top) n1 n2 =
7.591 - Const (op_,Top) $
7.592 - Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
7.593 -(*
7.594 -> val t = num_op_num "Int" 3 4;
7.595 -> atomty t;
7.596 -> string_of_cterm ((cterm_of thy) t);
7.597 -*)
7.598 -
7.599 -fun const_in str (Const _) = false
7.600 - | const_in str (Free (s,_)) = if strip_thy s = str then true else false
7.601 - | const_in str (Bound _) = false
7.602 - | const_in str (Var _) = false
7.603 - | const_in str (Abs (_,_,body)) = const_in str body
7.604 - | const_in str (f$u) = const_in str f orelse const_in str u;
7.605 -(*
7.606 -> val t = (term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
7.607 -> const_in "sqrt" t;
7.608 -val it = true : bool
7.609 -> val t = (term_of o the o (parse thy)) "6 + 5 * 4 + 3";
7.610 -> const_in "sqrt" t;
7.611 -val it = false : bool
7.612 -*)
7.613 -
7.614 -(*used for calculating built in binary operations in Isabelle2002->Float.ML*)
7.615 -(*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2
7.616 - | calc "Groups.minus_class.minus" (n1, n2) = n1-n2
7.617 - | calc "op *" (n1, n2) = n1*n2
7.618 - | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
7.619 - | calc "Atools.pow"(n1, n2) = power n1 n2
7.620 - | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
7.621 -fun calc_equ "op <" (n1, n2) = n1 < n2
7.622 - | calc_equ "op <=" (n1, n2) = n1 <= n2
7.623 - | calc_equ op_ _ =
7.624 - raise error ("calc_equ: operator = "^op_^" not defined");
7.625 -fun sqrt (n:int) = if n < 0 then 0
7.626 - (*FIXME ~~~*) else (trunc o Math.sqrt o Real.fromInt) n;
7.627 -
7.628 -fun mk_thmid thmid op_ n1 n2 =
7.629 - thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
7.630 -
7.631 -fun dest_binop_typ (Type("fun",[range,Type("fun",[arg2,arg1])])) =
7.632 - (arg1,arg2,range)
7.633 - | dest_binop_typ _ = raise error "dest_binop_typ: not binary";
7.634 -(* -----
7.635 -> val t = (term_of o the o (parse thy)) "#3^#4";
7.636 -> val hT = type_of (head_of t);
7.637 -> dest_binop_typ hT;
7.638 -val it = ("'a","nat","'a") : typ * typ * typ
7.639 - ----- *)
7.640 -
7.641 -
7.642 -(** transform binary numeralsstrings **)
7.643 -(*Makarius 100308, hacked by WN*)
7.644 -val numbers_to_string =
7.645 - let
7.646 - fun dest_num t =
7.647 - (case try HOLogic.dest_number t of
7.648 - SOME (T, i) =>
7.649 - (*if T = @{typ int} orelse T = @{typ real} then WN*)
7.650 - SOME (Free (signed_string_of_int i, T))
7.651 - (*else NONE WN*)
7.652 - | NONE => NONE);
7.653 -
7.654 - fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
7.655 - | to_str (t as (u1 $ u2)) =
7.656 - (case dest_num t of
7.657 - SOME t' => t'
7.658 - | NONE => to_str u1 $ to_str u2)
7.659 - | to_str t = perhaps dest_num t;
7.660 - in to_str end
7.661 -
7.662 -(*.make uminus uniform:
7.663 - Const ("uminus", _) $ Free ("2", "RealDef.real") --> Free ("-2", _)
7.664 -to be used immediately before evaluation of numerals;
7.665 -see Scripts/calculate.sml .*)
7.666 -(*2002 fun(*app_num_tr'2 (Const("0",T)) = Free("0",T)
7.667 - | app_num_tr'2 (Const("1",T)) = Free("1",T)
7.668 - |*)app_num_tr'2 (t as Const("uminus",_) $ Free(s,T)) =
7.669 - (case int_of_str s of SOME i =>
7.670 - if i > 0 then Free("-"^s,T) else Free(s,T)
7.671 - | NONE => t)
7.672 -(*| app_num_tr'2 (t as Const(s,T)) = t
7.673 - | app_num_tr'2 (Const("Numeral.number_of",Type ("fun", [_, T])) $ t) =
7.674 - Free(NumeralSyntax.dest_bin_str t, T)
7.675 - | app_num_tr'2 (t as Free(s,T)) = t
7.676 - | app_num_tr'2 (t as Var(n,T)) = t
7.677 - | app_num_tr'2 (t as Bound i) = t
7.678 -*)| app_num_tr'2 (Abs(s,T,body)) = Abs(s,T, app_num_tr'2 body)
7.679 - | app_num_tr'2 (t1 $ t2) = (app_num_tr'2 t1) $ (app_num_tr'2 t2)
7.680 - | app_num_tr'2 t = t;
7.681 -*)
7.682 -val uminus_to_string =
7.683 - let
7.684 - fun dest_num t =
7.685 - (case t of
7.686 - (Const ("HOL.uminus_class.uminus", _) $ Free (s, T)) =>
7.687 - (case int_of_str s of
7.688 - SOME i =>
7.689 - SOME (Free (signed_string_of_int (~1 * i), T))
7.690 - | NONE => NONE)
7.691 - | _ => NONE);
7.692 -
7.693 - fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
7.694 - | to_str (t as (u1 $ u2)) =
7.695 - (case dest_num t of
7.696 - SOME t' => t'
7.697 - | NONE => to_str u1 $ to_str u2)
7.698 - | to_str t = perhaps dest_num t;
7.699 - in to_str end;
7.700 -
7.701 -
7.702 -(*2002 fun num_str thm =
7.703 - let
7.704 - val {sign_ref = sign_ref, der = der, maxidx = maxidx,
7.705 - shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} =
7.706 - rep_thm_G thm;
7.707 - val prop' = app_num_tr'1 prop;
7.708 - in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;*)
7.709 -fun num_str thm =
7.710 - let val (deriv,
7.711 - {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps,
7.712 - hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
7.713 - val prop' = numbers_to_string prop;
7.714 - in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
7.715 -
7.716 -fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
7.717 -val it = fn : theory -> xstring -> Thm.thm*)
7.718 - Thm (xstring,
7.719 - num_str (ProofContext.get_thm (thy2ctxt' "Isac") xstring));
7.720 -
7.721 -(** get types of Free and Abs for parse' **)
7.722 -(*11.1.00: not used, fix-typed +,*,-,^ instead *)
7.723 -
7.724 -val dummyT = Type ("dummy",[]);
7.725 -val dummyT = TVar (("DUMMY",0),[]);
7.726 -
7.727 -(* assumes only 1 type for numerals
7.728 - and different identifiers for Const, Free and Abs *)
7.729 -fun get_types t =
7.730 - let
7.731 - fun get ts (Const(s,T)) = (s,T)::ts
7.732 - | get ts (Free(s,T)) = if is_no s
7.733 - then ("#",T)::ts else (s,T)::ts
7.734 - | get ts (Var(n,T)) = ts
7.735 - | get ts (Bound i) = ts
7.736 - | get ts (Abs(s,T,body)) = get ((s,T)::ts) body
7.737 - | get ts (t1 $ t2) = (get ts t1) @ (get ts t2)
7.738 - in distinct (get [] t) end;
7.739 -(*
7.740 -val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
7.741 -get_types t;
7.742 -*)
7.743 -
7.744 -(*11.1.00: not used, fix-typed +,*,-,^ instead *)
7.745 -fun set_types al (Const(s,T)) =
7.746 - (case assoc (al,s) of
7.747 - SOME T' => Const(s,T')
7.748 - | NONE => (warning ("set_types: no type for "^s); Const(s,dummyT)))
7.749 - | set_types al (Free(s,T)) =
7.750 - if is_no s then
7.751 - (case assoc (al,"#") of
7.752 - SOME T' => Free(s,T')
7.753 - | NONE => (warning ("set_types: no type for numerals"); Free(s,T)))
7.754 - else (case assoc (al,s) of
7.755 - SOME T' => Free(s,T')
7.756 - | NONE => (warning ("set_types: no type for "^s); Free(s,T)))
7.757 - | set_types al (Var(n,T)) = Var(n,T)
7.758 - | set_types al (Bound i) = Bound i
7.759 - | set_types al (Abs(s,T,body)) =
7.760 - (case assoc (al,s) of
7.761 - SOME T' => Abs(s,T', set_types al body)
7.762 - | NONE => (warning ("set_types: no type for "^s);
7.763 - Abs(s,T, set_types al body)))
7.764 - | set_types al (t1 $ t2) = (set_types al t1) $ (set_types al t2);
7.765 -(*
7.766 -val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
7.767 -val al = get_types t;
7.768 -
7.769 -val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
7.770 -atomty t; (* 'a *)
7.771 -val t' = set_types al t;
7.772 -atomty t'; (*real*)
7.773 -(cterm_of thy) t';
7.774 -val it = "x = #0 + #-1 * #-4" : cterm
7.775 -
7.776 -val t = (term_of o the o (parse thy))
7.777 - "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2";
7.778 -atomty t;
7.779 -val t' = set_types al t;
7.780 -atomty t';
7.781 -(cterm_of thy) t';
7.782 -uncaught exception TYPE (*^^^ is new, NOT in al*)
7.783 -*)
7.784 -
7.785 -
7.786 -(** from Descript.ML **)
7.787 -
7.788 -(** decompose an isa-list to an ML-list
7.789 - i.e. [] belong to the meta-language, too **)
7.790 -
7.791 -fun is_list ((Const("List.list.Cons",_)) $ _ $ _) = true
7.792 - | is_list _ = false;
7.793 -(* val (SOME ct) = parse thy "lll::real list";
7.794 -> val ty = (#t o rep_cterm) ct;
7.795 -> is_list ty;
7.796 -val it = false : bool
7.797 -> val (SOME ct) = parse thy "[lll]";
7.798 -> val ty = (#t o rep_cterm) ct;
7.799 -> is_list ty;
7.800 -val it = true : bool *)
7.801 -
7.802 -
7.803 -
7.804 -fun mk_Free (s,T) = Free(s,T);
7.805 -fun mk_free T s = Free(s,T);
7.806 -
7.807 -(*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*)
7.808 -fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*)
7.809 - let fun subst (t as Bound i, lev) =
7.810 - if i<lev then t (*var is locally bound*)
7.811 - else if i=lev then incr_boundvars lev arg
7.812 - else Bound(i-1) (*loose: change it*)
7.813 - | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
7.814 - | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
7.815 - | subst (t,lev) = t
7.816 - in subst (t,0) end;
7.817 -
7.818 -(*instantiate let; necessary for ass_up*)
7.819 -fun inst_abs thy (Const sT) = Const sT (*TODO.WN100907 drop thy*)
7.820 - | inst_abs thy (Free sT) = Free sT
7.821 - | inst_abs thy (Bound n) = Bound n
7.822 - | inst_abs thy (Var iT) = Var iT
7.823 - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) =
7.824 - let val b' = subst_bound (Free (v, T2), b);
7.825 - (*fun variant_abs: term.ML*)
7.826 - in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
7.827 - | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
7.828 - | inst_abs thy t = t;
7.829 -(*val scr =
7.830 - "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
7.831 - \ (let h_ = (hd o (filterVar f_)) eqs_; \
7.832 - \ e_1 = hd (dropWhile (ident h_) eqs_); \
7.833 - \ vs_ = dropWhile (ident f_) (Vars h_); \
7.834 - \ v_1 = hd (dropWhile (ident v_) vs_); \
7.835 - \ (s_1::bool list)=(SubProblem(DiffApp_,[univar,equation],[no_met])\
7.836 - \ [BOOL e_1, REAL v_1])\
7.837 - \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
7.838 -> val ttt = (term_of o the o (parse thy)) scr;
7.839 -> tracing(term2str ttt);
7.840 -> atomt ttt;
7.841 -*** -------------
7.842 -*** Const ( DiffApp.Make'_fun'_by'_explicit)
7.843 -*** . Free ( f_, )
7.844 -*** . Free ( v_, )
7.845 -*** . Free ( eqs_, )
7.846 -*** . Const ( Let)
7.847 -*** . . Const ( Fun.op o)
7.848 -*** . . . Const ( List.hd)
7.849 -*** . . . Const ( DiffApp.filterVar)
7.850 -*** . . . . Free ( f_, )
7.851 -*** . . . Free ( eqs_, )
7.852 -*** . . Abs( h_,..
7.853 -*** . . . Const ( Let)
7.854 -*** . . . . Const ( List.hd)
7.855 -*** . . . . . Const ( List.dropWhile)
7.856 -*** . . . . . . Const ( Atools.ident)
7.857 -*** . . . . . . . Bound 0 <---- Free ( h_, )
7.858 -*** . . . . . . Free ( eqs_, )
7.859 -*** . . . . Abs( e_1,..
7.860 -*** . . . . . Const ( Let)
7.861 -*** . . . . . . Const ( List.dropWhile)
7.862 -*** . . . . . . . Const ( Atools.ident)
7.863 -*** . . . . . . . . Free ( f_, )
7.864 -*** . . . . . . . Const ( Tools.Vars)
7.865 -*** . . . . . . . . Bound 1 <---- Free ( h_, )
7.866 -*** . . . . . . Abs( vs_,..
7.867 -*** . . . . . . . Const ( Let)
7.868 -*** . . . . . . . . Const ( List.hd)
7.869 -*** . . . . . . . . . Const ( List.dropWhile)
7.870 -*** . . . . . . . . . . Const ( Atools.ident)
7.871 -*** . . . . . . . . . . . Free ( v_, )
7.872 -*** . . . . . . . . . . Bound 0 <---- Free ( vs_, )
7.873 -*** . . . . . . . . Abs( v_1,..
7.874 -*** . . . . . . . . . Const ( Let)
7.875 -*** . . . . . . . . . . Const ( Script.SubProblem)
7.876 -*** . . . . . . . . . . . Const ( Pair)
7.877 -*** . . . . . . . . . . . . Free ( DiffApp_, )
7.878 -*** . . . . . . . . . . . . Const ( Pair)
7.879 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
7.880 -*** . . . . . . . . . . . . . . Free ( univar, )
7.881 -*** . . . . . . . . . . . . . . Const ( List.list.Cons)
7.882 -*** . . . . . . . . . . . . . . . Free ( equation, )
7.883 -*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
7.884 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
7.885 -*** . . . . . . . . . . . . . . Free ( no_met, )
7.886 -*** . . . . . . . . . . . . . . Const ( List.list.Nil)
7.887 -*** . . . . . . . . . . . Const ( List.list.Cons)
7.888 -*** . . . . . . . . . . . . Const ( Script.BOOL)
7.889 -*** . . . . . . . . . . . . . Bound 2 <----- Free ( e_1, )
7.890 -*** . . . . . . . . . . . . Const ( List.list.Cons)
7.891 -*** . . . . . . . . . . . . . Const ( Script.real_)
7.892 -*** . . . . . . . . . . . . . . Bound 0 <----- Free ( v_1, )
7.893 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
7.894 -*** . . . . . . . . . . Abs( s_1,..
7.895 -*** . . . . . . . . . . . Const ( Script.Substitute)
7.896 -*** . . . . . . . . . . . . Const ( List.list.Cons)
7.897 -*** . . . . . . . . . . . . . Const ( Pair)
7.898 -*** . . . . . . . . . . . . . . Bound 1 <----- Free ( v_1, )
7.899 -*** . . . . . . . . . . . . . . Const ( Fun.op o)
7.900 -*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
7.901 -*** . . . . . . . . . . . . . . . Const ( List.hd)
7.902 -*** . . . . . . . . . . . . . . . Bound 0 <----- Free ( s_1, )
7.903 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
7.904 -*** . . . . . . . . . . . . Bound 4 <----- Free ( h_, )
7.905 -
7.906 -> val ttt' = inst_abs thy ttt;
7.907 -> tracing(term2str ttt');
7.908 -Script Make_fun_by_explicit f_ v_ eqs_ =
7.909 - ... as above ...
7.910 -> atomt ttt';
7.911 -*** -------------
7.912 -*** Const ( DiffApp.Make'_fun'_by'_explicit)
7.913 -*** . Free ( f_, )
7.914 -*** . Free ( v_, )
7.915 -*** . Free ( eqs_, )
7.916 -*** . Const ( Let)
7.917 -*** . . Const ( Fun.op o)
7.918 -*** . . . Const ( List.hd)
7.919 -*** . . . Const ( DiffApp.filterVar)
7.920 -*** . . . . Free ( f_, )
7.921 -*** . . . Free ( eqs_, )
7.922 -*** . . Abs( h_,..
7.923 -*** . . . Const ( Let)
7.924 -*** . . . . Const ( List.hd)
7.925 -*** . . . . . Const ( List.dropWhile)
7.926 -*** . . . . . . Const ( Atools.ident)
7.927 -*** . . . . . . . Free ( h_, ) <---- Bound 0
7.928 -*** . . . . . . Free ( eqs_, )
7.929 -*** . . . . Abs( e_1,..
7.930 -*** . . . . . Const ( Let)
7.931 -*** . . . . . . Const ( List.dropWhile)
7.932 -*** . . . . . . . Const ( Atools.ident)
7.933 -*** . . . . . . . . Free ( f_, )
7.934 -*** . . . . . . . Const ( Tools.Vars)
7.935 -*** . . . . . . . . Free ( h_, ) <---- Bound 1
7.936 -*** . . . . . . Abs( vs_,..
7.937 -*** . . . . . . . Const ( Let)
7.938 -*** . . . . . . . . Const ( List.hd)
7.939 -*** . . . . . . . . . Const ( List.dropWhile)
7.940 -*** . . . . . . . . . . Const ( Atools.ident)
7.941 -*** . . . . . . . . . . . Free ( v_, )
7.942 -*** . . . . . . . . . . Free ( vs_, ) <---- Bound 0
7.943 -*** . . . . . . . . Abs( v_1,..
7.944 -*** . . . . . . . . . Const ( Let)
7.945 -*** . . . . . . . . . . Const ( Script.SubProblem)
7.946 -*** . . . . . . . . . . . Const ( Pair)
7.947 -*** . . . . . . . . . . . . Free ( DiffApp_, )
7.948 -*** . . . . . . . . . . . . Const ( Pair)
7.949 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
7.950 -*** . . . . . . . . . . . . . . Free ( univar, )
7.951 -*** . . . . . . . . . . . . . . Const ( List.list.Cons)
7.952 -*** . . . . . . . . . . . . . . . Free ( equation, )
7.953 -*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
7.954 -*** . . . . . . . . . . . . . Const ( List.list.Cons)
7.955 -*** . . . . . . . . . . . . . . Free ( no_met, )
7.956 -*** . . . . . . . . . . . . . . Const ( List.list.Nil)
7.957 -*** . . . . . . . . . . . Const ( List.list.Cons)
7.958 -*** . . . . . . . . . . . . Const ( Script.BOOL)
7.959 -*** . . . . . . . . . . . . . Free ( e_1, ) <----- Bound 2
7.960 -*** . . . . . . . . . . . . Const ( List.list.Cons)
7.961 -*** . . . . . . . . . . . . . Const ( Script.real_)
7.962 -*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 0
7.963 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
7.964 -*** . . . . . . . . . . Abs( s_1,..
7.965 -*** . . . . . . . . . . . Const ( Script.Substitute)
7.966 -*** . . . . . . . . . . . . Const ( List.list.Cons)
7.967 -*** . . . . . . . . . . . . . Const ( Pair)
7.968 -*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 1
7.969 -*** . . . . . . . . . . . . . . Const ( Fun.op o)
7.970 -*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
7.971 -*** . . . . . . . . . . . . . . . Const ( List.hd)
7.972 -*** . . . . . . . . . . . . . . . Free ( s_1, ) <----- Bound 0
7.973 -*** . . . . . . . . . . . . . Const ( List.list.Nil)
7.974 -*** . . . . . . . . . . . . Free ( h_, ) <----- Bound 4
7.975 -
7.976 -Note numbering of de Bruijn indexes !
7.977 -
7.978 -Script Make_fun_by_explicit f_ v_ eqs_ =
7.979 - let h_ = (hd o filterVar f_) eqs_;
7.980 - e_1 = hd (dropWhile (ident h_ BOUND_0) eqs_);
7.981 - vs_ = dropWhile (ident f_) (Vars h_ BOUND_1);
7.982 - v_1 = hd (dropWhile (ident v_) vs_ BOUND_0);
7.983 - s_1 =
7.984 - SubProblem (DiffApp_, [univar, equation], [no_met])
7.985 - [BOOL e_1 BOUND_2, REAL v_1 BOUND_0]
7.986 - in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4
7.987 -*)
7.988 -
7.989 -
7.990 -fun T_a2real (Type (s, [])) =
7.991 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
7.992 - | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
7.993 - | T_a2real (TFree (s, srt)) =
7.994 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
7.995 - | T_a2real (TVar (("DUMMY",_),srt)) = HOLogic.realT;
7.996 -
7.997 -(*FIXME .. fixes the type (+see Typefix.thy*)
7.998 -fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T))
7.999 - | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
7.1000 - | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
7.1001 - | typ_a2real (Bound i) = (Bound i)
7.1002 - | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
7.1003 - | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
7.1004 -(*
7.1005 -----------------6.8.02---------------------------------------------------
7.1006 - val str = "1";
7.1007 - val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
7.1008 - atomty (term_of t);
7.1009 -*** -------------
7.1010 -*** Const ( 1, 'a)
7.1011 - val t = (app_num_tr' o term_of) t;
7.1012 - atomty t;
7.1013 -*** -------------
7.1014 -*** Const ( 1, 'a)
7.1015 - val t = typ_a2real t;
7.1016 - atomty t;
7.1017 -*** -------------
7.1018 -*** Const ( 1, real)
7.1019 -
7.1020 - val str = "2";
7.1021 - val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
7.1022 - atomty (term_of t);
7.1023 -*** -------------
7.1024 -*** Const ( Numeral.number_of, bin => 'a)
7.1025 -*** . Const ( Numeral.bin.Bit, [bin, bool] => bin)
7.1026 -*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
7.1027 -*** . . . Const ( Numeral.bin.Pls, bin)
7.1028 -*** . . . Const ( True, bool)
7.1029 -*** . . Const ( False, bool)
7.1030 - val t = (app_num_tr' o term_of) t;
7.1031 - atomty t;
7.1032 -*** -------------
7.1033 -*** Free ( 2, 'a)
7.1034 - val t = typ_a2real t;
7.1035 - atomty t;
7.1036 -*** -------------
7.1037 -*** Free ( 2, real)
7.1038 -----------------6.8.02---------------------------------------------------
7.1039 -
7.1040 -
7.1041 -> val str = "R";
7.1042 -> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
7.1043 -val t = Free ("R","?DUMMY") : term
7.1044 -> val t' = typ_a2real t;
7.1045 -> (cterm_of thy) t';
7.1046 -val it = "R::RealDef.real" : cterm
7.1047 -
7.1048 -> val str = "R=R";
7.1049 -> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
7.1050 -> atomty (typ_a2real t);
7.1051 -*** -------------
7.1052 -*** Const ( op =, [RealDef.real, RealDef.real] => bool)
7.1053 -*** Free ( R, RealDef.real)
7.1054 -*** Free ( R, RealDef.real)
7.1055 -> val t' = typ_a2real t;
7.1056 -> (cterm_of thy) t';
7.1057 -val it = "(R::RealDef.real) = R" : cterm
7.1058 -
7.1059 -> val str = "fixed_values [R=R]";
7.1060 -> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
7.1061 -> val t' = typ_a2real t;
7.1062 -> (cterm_of thy) t';
7.1063 -val it = "fixed_values [(R::RealDef.real) = R]" : cterm
7.1064 -*)
7.1065 -
7.1066 -(*TODO.WN0609: parse should return a term or a string
7.1067 - (or even more comprehensive datastructure for error-messages)
7.1068 - i.e. in wrapping with SOME term or NONE the latter is not sufficient*)
7.1069 -(*2002 fun parseold thy str =
7.1070 - (let
7.1071 - val sgn = sign_of thy;
7.1072 - val t = ((*typ_a2real o*) app_num_tr'1 o term_of)
7.1073 - (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
7.1074 - in SOME (cterm_of sgn t) end)
7.1075 - handle _ => NONE;*)
7.1076 -
7.1077 -
7.1078 -
7.1079 -fun parseold thy str =
7.1080 - (let val t = ((*typ_a2real o*) numbers_to_string)
7.1081 - (Syntax.read_term_global thy str)
7.1082 - in SOME (cterm_of thy t) end)
7.1083 - handle _ => NONE;
7.1084 -(*2002 fun parseN thy str =
7.1085 - (let
7.1086 - val sgn = sign_of thy;
7.1087 - val t = ((*typ_a2real o app_num_tr'1 o*) term_of)
7.1088 - (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
7.1089 - in SOME (cterm_of sgn t) end)
7.1090 - handle _ => NONE;*)
7.1091 -fun parseN thy str =
7.1092 - (let val t = (*(typ_a2real o numbers_to_string)*)
7.1093 - (Syntax.read_term_global thy str)
7.1094 - in SOME (cterm_of thy t) end)
7.1095 - handle _ => NONE;
7.1096 -(*2002 fun parse thy str =
7.1097 - (let
7.1098 - val sgn = sign_of thy;
7.1099 - val t = (typ_a2real o app_num_tr'1 o term_of)
7.1100 - (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
7.1101 - in SOME (cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
7.1102 - handle _ => NONE;*)
7.1103 -(*2010 fun parse thy str =
7.1104 - (let val t = (typ_a2real o app_num_tr'1) (Syntax.read_term_global thy str)
7.1105 - in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
7.1106 - handle _ => NONE;*)
7.1107 -fun parse thy str =
7.1108 - (let val t = (typ_a2real o numbers_to_string)
7.1109 - (Syntax.read_term_global thy str)
7.1110 - in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
7.1111 - handle _ => NONE;
7.1112 -(*
7.1113 -> val (SOME ct) = parse thy "(-#5)^^^#3";
7.1114 -> atomty (term_of ct);
7.1115 -*** -------------
7.1116 -*** Const ( Nat.op ^, ['a, nat] => 'a)
7.1117 -*** Const ( uminus, 'a => 'a)
7.1118 -*** Free ( #5, 'a)
7.1119 -*** Free ( #3, nat)
7.1120 -> val (SOME ct) = parse thy "R=R";
7.1121 -> atomty (term_of ct);
7.1122 -*** -------------
7.1123 -*** Const ( op =, [real, real] => bool)
7.1124 -*** Free ( R, real)
7.1125 -*** Free ( R, real)
7.1126 -
7.1127 -THIS IS THE OUTPUT FOR VERSION (3) above at typ_a2real !!!!!
7.1128 -*** -------------
7.1129 -*** Const ( op =, [RealDef.real, RealDef.real] => bool)
7.1130 -*** Free ( R, RealDef.real)
7.1131 -*** Free ( R, RealDef.real) *)
7.1132 -
7.1133 -fun parse_patt thy str =
7.1134 - ProofContext.read_term_pattern (thy2ctxt thy) str;
7.1135 -
7.1136 -(*version for testing local to theories*)
7.1137 -fun str2term_ thy str = (term_of o the o (parse thy)) str;
7.1138 -fun str2term str = (term_of o the o (parse (theory "Isac"))) str;
7.1139 -fun strs2terms ss = map str2term ss;
7.1140 -fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str;
7.1141 -
7.1142 -(*+ makes a substitution from the output of Pattern.match +*)
7.1143 -(*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)
7.1144 -fun mk_subs (subs: ((string * int) * (Term.typ * Term.term)) list) =
7.1145 -let fun mk_sub ((id, _), (ty, tm)) = (Free (id, ty), tm) in
7.1146 -map mk_sub subs end;
7.1147 -
7.1148 -val atomthm = atomt o #prop o rep_thm;
7.1149 -
7.1150 -(*.instantiate #prop thm with bound variables (as Free).*)
7.1151 -fun inst_bdv [] t = t : term
7.1152 - | inst_bdv (instl: (term*term) list) t =
7.1153 - let fun subst (v as Var((s,_),T)) =
7.1154 - (case explode s of
7.1155 - "b"::"d"::"v"::_ =>
7.1156 - if_none (assoc(instl,Free(s,T))) (Free(s,T))
7.1157 - | _ => v)
7.1158 - | subst (Abs(a,T,body)) = Abs(a, T, subst body)
7.1159 - | subst (f$t') = subst f $ subst t'
7.1160 - | subst t = if_none (assoc(instl,t)) t
7.1161 - in subst t end;
7.1162 -
7.1163 -
7.1164 -(*WN050829 caution: is_atom (str2term"q_0/2 * L * x") = true !!!
7.1165 - use length (vars term) = 1 instead*)
7.1166 -fun is_atom (Const ("Float.Float",_) $ _) = true
7.1167 - | is_atom (Const ("ComplexI.I'_'_",_)) = true
7.1168 - | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
7.1169 - | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
7.1170 - | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $
7.1171 - (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
7.1172 - is_atom t1 andalso is_atom t2
7.1173 - | is_atom (Const _) = true
7.1174 - | is_atom (Free _) = true
7.1175 - | is_atom (Var _) = true
7.1176 - | is_atom _ = false;
7.1177 -(* val t = str2term "q_0/2 * L * x";
7.1178 -
7.1179 -
7.1180 -*)
7.1181 -(*val t = str2term "Float ((1,2),(0,0))";
7.1182 -> is_atom t;
7.1183 -val it = true : bool
7.1184 -> val t = str2term "Float ((1,2),(0,0)) * I__";
7.1185 -> is_atom t;
7.1186 -val it = true : bool
7.1187 -> val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
7.1188 -> is_atom t;
7.1189 -val it = true : bool
7.1190 -> val t = str2term "1 + 2*I__";
7.1191 -> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
7.1192 -*)
7.1193 -
7.1194 -(*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
7.1195 - have found a substitution (required for evaluating the preconditions
7.1196 - of _incomplete_ models).*)
7.1197 -fun subst_atomic_all [] t = (false, (*TODO may be 'true' for some terms ?*)
7.1198 - t : term)
7.1199 - | subst_atomic_all (instl: (term*term) list) t =
7.1200 - let fun subst (Abs(a,T,body)) =
7.1201 - let val (all, body') = subst body
7.1202 - in (all, Abs(a, T, body')) end
7.1203 - | subst (f$tt) =
7.1204 - let val (all1, f') = subst f
7.1205 - val (all2, tt') = subst tt
7.1206 - in (all1 andalso all2, f' $ tt') end
7.1207 - | subst (t as Free _) =
7.1208 - if is_num t then (true, t) (*numerals cannot be subst*)
7.1209 - else (case assoc(instl,t) of
7.1210 - SOME t' => (true, t')
7.1211 - | NONE => (false, t))
7.1212 - | subst t = (true, if_none (assoc(instl,t)) t)
7.1213 - in subst t end;
7.1214 -
7.1215 -(*.add two terms with a type given.*)
7.1216 -fun mk_add t1 t2 =
7.1217 - let val T1 = type_of t1
7.1218 - val T2 = type_of t2
7.1219 - in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2])
7.1220 - else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
7.1221 - end;
7.1222 -
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 07:28:10 2010 +0200
8.3 @@ -0,0 +1,1217 @@
8.4 +(* Title: extends Isabelle/src/Pure/term.ML
8.5 + Author: Walther Neuper 1999
8.6 + (c) due to copyright terms
8.7 +*)
8.8 +
8.9 +(*
8.10 +> (cterm_of thy) a_term;
8.11 +val it = "empty" : cterm *)
8.12 +
8.13 +(*2003 fun match thy t pat =
8.14 + (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
8.15 + handle _ => [];
8.16 +fn : theory ->
8.17 + Term.term -> Term.term -> (Term.indexname * Term.term) list*)
8.18 +(*see src/Tools/eqsubst.ML fun clean_match*)
8.19 +(*2003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
8.20 +fun matches thy tm pa =
8.21 + (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
8.22 + handle _ => false
8.23 +
8.24 +fun atomtyp t = (*WN10 see raw_pp_typ*)
8.25 + let
8.26 + fun ato n (Type (s,[])) =
8.27 + ("\n*** "^indent n^"Type ("^s^",[])")
8.28 + | ato n (Type (s,Ts)) =
8.29 + ("\n*** "^indent n^"Type ("^s^",["^ atol (n+1) Ts)
8.30 +
8.31 + | ato n (TFree (s,sort)) =
8.32 + ("\n*** "^indent n^"TFree ("^s^",["^ strs2str' sort)
8.33 +
8.34 + | ato n (TVar ((s,i),sort)) =
8.35 + ("\n*** "^indent n^"TVar (("^s^","^
8.36 + string_of_int i ^ strs2str' sort)
8.37 + and atol n [] =
8.38 + ("\n*** "^indent n^"]")
8.39 + | atol n (T::Ts) = (ato n T ^ atol n Ts)
8.40 +(*in print (ato 0 t ^ "\n") end; TODO TUM10*)
8.41 +in tracing (ato 0 t) end;
8.42 +(*
8.43 +> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
8.44 +> atomtyp T;
8.45 +*** Type (fun,[
8.46 +*** Type (RealDef.real,[])
8.47 +*** Type (fun,[
8.48 +*** Type (IntDef.int,[])
8.49 +*** Type (nat,[])
8.50 +*** ]
8.51 +*** ]
8.52 +*)
8.53 +
8.54 +(*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*)
8.55 +local
8.56 + fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
8.57 + fun pp_list xs = Pretty.list "[" "]" xs
8.58 + fun pp_str s = Pretty.str s
8.59 + fun pp_qstr s = Pretty.quote (pp_str s)
8.60 + fun pp_int i = pp_str (string_of_int i)
8.61 + fun pp_sort S = pp_list (map pp_qstr S)
8.62 + fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
8.63 +in
8.64 +fun raw_pp_typ (TVar ((a, i), S)) =
8.65 + pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
8.66 + | raw_pp_typ (TFree (a, S)) =
8.67 + pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
8.68 + | raw_pp_typ (Type (a, tys)) =
8.69 + pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
8.70 +end
8.71 +(* install
8.72 +PolyML.addPrettyPrinter
8.73 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
8.74 +de-install
8.75 +PolyML.addPrettyPrinter
8.76 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
8.77 +*)
8.78 +
8.79 +fun atomt t =
8.80 + let fun ato (Const (a, _)) n =
8.81 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
8.82 + | ato (Free (a, _)) n =
8.83 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
8.84 + | ato (Var ((a, i), _)) n =
8.85 + "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^
8.86 + string_of_int i ^ "), _)"
8.87 + | ato (Bound i) n =
8.88 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
8.89 + | ato (Abs (a, _, body)) n =
8.90 + "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
8.91 + | ato (f $ t) n = (ato f n ^ ato t (n + 1))
8.92 + in tracing ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
8.93 +
8.94 +fun term_detail2str t =
8.95 + let fun ato (Const (a, T)) n =
8.96 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")"
8.97 + | ato (Free (a, T)) n =
8.98 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")"
8.99 + | ato (Var ((a, i), T)) n =
8.100 + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^
8.101 + string_of_typ T ^ ")"
8.102 + | ato (Bound i) n =
8.103 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
8.104 + | ato (Abs(a, T, body)) n =
8.105 + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.."
8.106 + ^ ato body (n + 1)
8.107 + | ato (f $ t) n = ato f n ^ ato t (n + 1)
8.108 + in "\n*** " ^ ato t 0 ^ "\n***" end;
8.109 +fun atomty t = (tracing o term_detail2str) t; (*WN100907 broken*)
8.110 +
8.111 +fun term_str thy (Const(s,_)) = s
8.112 + | term_str thy (Free(s,_)) = s
8.113 + | term_str thy (Var((s,i),_)) = s^(string_of_int i)
8.114 + | term_str thy (Bound i) = "B."^(string_of_int i)
8.115 + | term_str thy (Abs(s,_,_)) = s
8.116 + | term_str thy t = raise error("term_str not for "^term2str t);
8.117 +
8.118 +(*.contains the fst argument the second argument (a leave! of term).*)
8.119 +fun contains_term (Abs(_,_,body)) t = contains_term body t
8.120 + | contains_term (f $ f') t =
8.121 + contains_term f t orelse contains_term f' t
8.122 + | contains_term s t = t = s;
8.123 +(*.contains the term a VAR(("*",_),_) ?.*)
8.124 +fun contains_Var (Abs(_,_,body)) = contains_Var body
8.125 + | contains_Var (f $ f') = contains_Var f orelse contains_Var f'
8.126 + | contains_Var (Var _) = true
8.127 + | contains_Var _ = false;
8.128 +(* contains_Var (str2term "?z = 3") (*true*);
8.129 + contains_Var (str2term "z = 3") (*false*);
8.130 + *)
8.131 +
8.132 +(*fun int_of_str str =
8.133 + let val ss = explode str
8.134 + val str' = case ss of
8.135 + "("::s => drop_last s | _ => ss
8.136 + in case BasisLibrary.Int.fromString (implode str') of
8.137 + SOME i => SOME i
8.138 + | NONE => NONE end;*)
8.139 +fun int_of_str str =
8.140 + let val ss = explode str
8.141 + val str' = case ss of
8.142 + "("::s => drop_last s | _ => ss
8.143 + in (SOME (Thy_Output.integer (implode str'))) handle _ => NONE end;
8.144 +(*
8.145 +> int_of_str "123";
8.146 +val it = SOME 123 : int option
8.147 +> int_of_str "(-123)";
8.148 +val it = SOME 123 : int option
8.149 +> int_of_str "#123";
8.150 +val it = NONE : int option
8.151 +> int_of_str "-123";
8.152 +val it = SOME ~123 : int option
8.153 +*)
8.154 +fun int_of_str' str =
8.155 + case int_of_str str of
8.156 + SOME i => i
8.157 + | NONE => raise TERM ("int_of_string: no int-string",[]);
8.158 +val str2int = int_of_str';
8.159 +
8.160 +fun is_numeral str = case int_of_str str of
8.161 + SOME _ => true
8.162 + | NONE => false;
8.163 +val is_no = is_numeral;
8.164 +fun is_num (Free (s,_)) = if is_numeral s then true else false
8.165 + | is_num _ = false;
8.166 +(*>
8.167 +> is_num ((term_of o the o (parse thy)) "#1");
8.168 +val it = true : bool
8.169 +> is_num ((term_of o the o (parse thy)) "#-1");
8.170 +val it = true : bool
8.171 +> is_num ((term_of o the o (parse thy)) "a123");
8.172 +val it = false : bool
8.173 +*)
8.174 +
8.175 +(*fun int_of_Free (Free (intstr, _)) =
8.176 + (case BasisLibrary.Int.fromString intstr of
8.177 + SOME i => i
8.178 + | NONE => raise error ("int_of_Free ( "^ intstr ^", _)"))
8.179 + | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");*)
8.180 +fun int_of_Free (Free (intstr, _)) = (Thy_Output.integer intstr
8.181 + handle _ => raise error ("int_of_Free ( "^ intstr ^", _)"))
8.182 + | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");
8.183 +
8.184 +fun vars t =
8.185 + let
8.186 + fun scan vs (Const(s,T)) = vs
8.187 + | scan vs (t as Free(s,T)) = if is_no s then vs else t::vs
8.188 + | scan vs (t as Var((s,i),T)) = t::vs
8.189 + | scan vs (Bound i) = vs
8.190 + | scan vs (Abs(s,T,t)) = scan vs t
8.191 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
8.192 + in (distinct o (scan [])) t end;
8.193 +
8.194 +fun is_Free (Free _) = true
8.195 + | is_Free _ = false;
8.196 +fun is_fun_id (Const _) = true
8.197 + | is_fun_id (Free _) = true
8.198 + | is_fun_id _ = false;
8.199 +fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
8.200 + | is_f_x _ = false;
8.201 +(* is_f_x (str2term "q_0/2 * L * x") (*false*);
8.202 + is_f_x (str2term "M_b x") (*true*);
8.203 + *)
8.204 +fun vars_str t =
8.205 + let
8.206 + fun scan vs (Const(s,T)) = vs
8.207 + | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
8.208 + | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
8.209 + | scan vs (Bound i) = vs
8.210 + | scan vs (Abs(s,T,t)) = scan vs t
8.211 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
8.212 + in (distinct o (scan [])) t end;
8.213 +
8.214 +fun ids2str t =
8.215 + let
8.216 + fun scan vs (Const(s,T)) = if is_no s then vs else s::vs
8.217 + | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
8.218 + | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
8.219 + | scan vs (Bound i) = vs
8.220 + | scan vs (Abs(s,T,t)) = scan (s::vs) t
8.221 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
8.222 + in (distinct o (scan [])) t end;
8.223 +fun is_bdv str =
8.224 + case explode str of
8.225 + "b"::"d"::"v"::_ => true
8.226 + | _ => false;
8.227 +fun is_bdv_ (Free (s,_)) = is_bdv s
8.228 + | is_bdv_ _ = false;
8.229 +
8.230 +fun free2str (Free (s,_)) = s
8.231 + | free2str t = raise error ("free2str not for "^ term2str t);
8.232 +fun free2int (t as Free (s, _)) = ((str2int s)
8.233 + handle _ => raise error ("free2int: "^term_detail2str t))
8.234 + | free2int t = raise error ("free2int: "^term_detail2str t);
8.235 +
8.236 +(*27.8.01: unused*)
8.237 +fun var2free (t as Const(s,T)) = t
8.238 + | var2free (t as Free(s,T)) = t
8.239 + | var2free (Var((s,i),T)) = Free(s,T)
8.240 + | var2free (t as Bound i) = t
8.241 + | var2free (Abs(s,T,t)) = Abs(s,T,var2free t)
8.242 + | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
8.243 +
8.244 +(*27.8.01: doesn't find some subterm ???!???*)
8.245 +(*2010 free2var -> Logic.varify, but take care of 'Free ("1",_)'*)
8.246 +fun free2var (t as Const (s, T)) = t
8.247 + | free2var (t as Free (s, T)) = if is_no s then t else Var ((s, 0), T)
8.248 + | free2var (t as Var ((s, i), T)) = t
8.249 + | free2var (t as Bound i) = t
8.250 + | free2var (Abs (s, T, t)) = Abs (s, T, free2var t)
8.251 + | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
8.252 +
8.253 +
8.254 +fun mk_listT T = Type ("List.list", [T]);
8.255 +fun list_const T =
8.256 + Const("List.list.Cons", [T, mk_listT T] ---> mk_listT T);
8.257 +(*28.8.01: TODO: get type from head of list: 1 arg less!!!*)
8.258 +fun list2isalist T [] = Const("List.list.Nil",mk_listT T)
8.259 + | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts);
8.260 +(*
8.261 +> val tt = (term_of o the o (parse thy)) "R=(R::real)";
8.262 +> val TT = type_of tt;
8.263 +> val ss = list2isalist TT [tt,tt,tt];
8.264 +> (cterm_of thy) ss;
8.265 +val it = "[R = R, R = R, R = R]" : cterm *)
8.266 +
8.267 +fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
8.268 + | isapair2pair t =
8.269 + raise error ("isapair2pair called with "^term2str t);
8.270 +
8.271 +val listType = Type ("List.list",[Type ("bool",[])]);
8.272 +fun isalist2list ls =
8.273 + let
8.274 + fun get es (Const("List.list.Cons",_) $ t $ ls) = get (t::es) ls
8.275 + | get es (Const("List.list.Nil",_)) = es
8.276 + | get _ t =
8.277 + raise error ("isalist2list applied to NON-list '"^term2str t^"'")
8.278 + in (rev o (get [])) ls end;
8.279 +(*
8.280 +> val il = str2term "[a=b,c=d,e=f]";
8.281 +> val l = isalist2list il;
8.282 +> (tracing o terms2str) l;
8.283 +["a = b","c = d","e = f"]
8.284 +
8.285 +> val il = str2term "ss___::bool list";
8.286 +> val l = isalist2list il;
8.287 +[Free ("ss___", "bool List.list")]
8.288 +*)
8.289 +
8.290 +
8.291 +(*review Isabelle2009/src/HOL/Tools/hologic.ML*)
8.292 +val prop = Type ("prop",[]); (* ~/Diss.99/Integers-Isa/tools.sml*)
8.293 +val bool = Type ("bool",[]); (* 2002 Integ.int *)
8.294 +val Trueprop = Const("Trueprop",bool-->prop);
8.295 +fun mk_prop t = Trueprop $ t;
8.296 +val true_as_term = Const("True",bool);
8.297 +val false_as_term = Const("False",bool);
8.298 +val true_as_cterm = cterm_of (theory "HOL") true_as_term;
8.299 +val false_as_cterm = cterm_of (theory "HOL") false_as_term;
8.300 +
8.301 +infixr 5 -->; (*2002 /Pure/term.ML *)
8.302 +infixr --->; (*2002 /Pure/term.ML *)
8.303 +fun S --> T = Type("fun",[S,T]); (*2002 /Pure/term.ML *)
8.304 +val op ---> = foldr (op -->); (*2002 /Pure/term.ML *)
8.305 +fun list_implies ([], B) = B : term (*2002 /term.ML *)
8.306 + | list_implies (A::AS, B) = Logic.implies $ A $ list_implies(AS,B);
8.307 +
8.308 +
8.309 +
8.310 +(** substitution **)
8.311 +
8.312 +fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = (* = thm.ML *)
8.313 + match_bvs(s, t, if x="" orelse y="" then al
8.314 + else (x,y)::al)
8.315 + | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
8.316 + | match_bvs(_,_,al) = al;
8.317 +fun ren_inst(insts,prop,pat,obj) = (* = thm.ML *)
8.318 + let val ren = match_bvs(pat,obj,[])
8.319 + fun renAbs(Abs(x,T,b)) =
8.320 + Abs(case assoc_string(ren,x) of NONE => x
8.321 + | SOME(y) => y, T, renAbs(b))
8.322 + | renAbs(f$t) = renAbs(f) $ renAbs(t)
8.323 + | renAbs(t) = t
8.324 + in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
8.325 +
8.326 +
8.327 +
8.328 +
8.329 +
8.330 +
8.331 +fun dest_equals' (Const("op =",_) $ t $ u) = (t,u)(* logic.ML: Const("=="*)
8.332 + | dest_equals' t = raise TERM("dest_equals'", [t]);
8.333 +val lhs_ = (fst o dest_equals');
8.334 +val rhs_ = (snd o dest_equals');
8.335 +
8.336 +fun is_equality (Const("op =",_) $ t $ u) = true (* logic.ML: Const("=="*)
8.337 + | is_equality _ = false;
8.338 +fun mk_equality (t,u) = (Const("op =",[type_of t,type_of u]--->bool) $ t $ u);
8.339 +fun is_expliceq (Const("op =",_) $ (Free _) $ u) = true
8.340 + | is_expliceq _ = false;
8.341 +fun strip_trueprop (Const("Trueprop",_) $ t) = t
8.342 + | strip_trueprop t = t;
8.343 +(* | strip_trueprop t = raise TERM("strip_trueprop", [t]);
8.344 +*)
8.345 +
8.346 +(*.(A1==>...An==>B) goes to (A1==>...An==>).*)
8.347 +fun strip_imp_prems' (Const("==>", T) $ A $ t) =
8.348 + let fun coll_prems As (Const("==>", _) $ A $ t) =
8.349 + coll_prems (As $ (Logic.implies $ A)) t
8.350 + | coll_prems As _ = SOME As
8.351 + in coll_prems (Logic.implies $ A) t end
8.352 + | strip_imp_prems' _ = NONE; (* logic.ML: term -> term list*)
8.353 +(*
8.354 + val thm = real_mult_div_cancel1;
8.355 + val prop = (#prop o rep_thm) thm;
8.356 + atomt prop;
8.357 +*** -------------
8.358 +*** Const ( ==>)
8.359 +*** . Const ( Trueprop)
8.360 +*** . . Const ( Not)
8.361 +*** . . . Const ( op =)
8.362 +*** . . . . Var ((k, 0), )
8.363 +*** . . . . Const ( 0)
8.364 +*** . Const ( Trueprop)
8.365 +*** . . Const ( op =) *** .............
8.366 + val SOME t = strip_imp_prems' ((#prop o rep_thm) thm);
8.367 + atomt t;
8.368 +*** -------------
8.369 +*** Const ( ==>)
8.370 +*** . Const ( Trueprop)
8.371 +*** . . Const ( Not)
8.372 +*** . . . Const ( op =)
8.373 +*** . . . . Var ((k, 0), )
8.374 +*** . . . . Const ( 0)
8.375 +
8.376 + val thm = real_le_anti_sym;
8.377 + val prop = (#prop o rep_thm) thm;
8.378 + atomt prop;
8.379 +*** -------------
8.380 +*** Const ( ==>)
8.381 +*** . Const ( Trueprop)
8.382 +*** . . Const ( op <=)
8.383 +*** . . . Var ((z, 0), )
8.384 +*** . . . Var ((w, 0), )
8.385 +*** . Const ( ==>)
8.386 +*** . . Const ( Trueprop)
8.387 +*** . . . Const ( op <=)
8.388 +*** . . . . Var ((w, 0), )
8.389 +*** . . . . Var ((z, 0), )
8.390 +*** . . Const ( Trueprop)
8.391 +*** . . . Const ( op =)
8.392 +*** .............
8.393 + val SOME t = strip_imp_prems' ((#prop o rep_thm) thm);
8.394 + atomt t;
8.395 +*** -------------
8.396 +*** Const ( ==>)
8.397 +*** . Const ( Trueprop)
8.398 +*** . . Const ( op <=)
8.399 +*** . . . Var ((z, 0), )
8.400 +*** . . . Var ((w, 0), )
8.401 +*** . Const ( ==>)
8.402 +*** . . Const ( Trueprop)
8.403 +*** . . . Const ( op <=)
8.404 +*** . . . . Var ((w, 0), )
8.405 +*** . . . . Var ((z, 0), )
8.406 +*)
8.407 +
8.408 +(*. (A1==>...An==>) (B) goes to (A1==>...An==>B), where B is lowest branch.*)
8.409 +fun ins_concl (Const("==>", T) $ A $ t) B = Logic.implies $ A $ (ins_concl t B)
8.410 + | ins_concl (Const("==>", T) $ A ) B = Logic.implies $ A $ B
8.411 + | ins_concl t B = raise TERM("ins_concl", [t, B]);
8.412 +(*
8.413 + val thm = real_le_anti_sym;
8.414 + val prop = (#prop o rep_thm) thm;
8.415 + val concl = Logic.strip_imp_concl prop;
8.416 + val SOME prems = strip_imp_prems' prop;
8.417 + val prop' = ins_concl prems concl;
8.418 + prop = prop';
8.419 + atomt prop;
8.420 + atomt prop';
8.421 +*)
8.422 +
8.423 +
8.424 +fun vperm (Var _, Var _) = true (*2002 Pure/thm.ML *)
8.425 + | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
8.426 + | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
8.427 + | vperm (t, u) = (t = u);
8.428 +
8.429 +(*2002 cp from Pure/term.ML --- since 2009 in Pure/old_term.ML*)
8.430 +fun mem_term (_, []) = false
8.431 + | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
8.432 +fun subset_term ([], ys) = true
8.433 + | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
8.434 +fun eq_set_term (xs, ys) =
8.435 + xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
8.436 +(*a total, irreflexive ordering on index names*)
8.437 +fun xless ((a,i), (b,j): indexname) = i<j orelse (i=j andalso a<b);
8.438 +(*a partial ordering (not reflexive) for atomic terms*)
8.439 +fun atless (Const (a,_), Const (b,_)) = a<b
8.440 + | atless (Free (a,_), Free (b,_)) = a<b
8.441 + | atless (Var(v,_), Var(w,_)) = xless(v,w)
8.442 + | atless (Bound i, Bound j) = i<j
8.443 + | atless _ = false;
8.444 +(*insert atomic term into partially sorted list, suppressing duplicates (?)*)
8.445 +fun insert_aterm (t,us) =
8.446 + let fun inserta [] = [t]
8.447 + | inserta (us as u::us') =
8.448 + if atless(t,u) then t::us
8.449 + else if t=u then us (*duplicate*)
8.450 + else u :: inserta(us')
8.451 + in inserta us end;
8.452 +
8.453 +(*Accumulates the Vars in the term, suppressing duplicates*)
8.454 +fun add_term_vars (t, vars: term list) = case t of
8.455 + Var _ => insert_aterm(t,vars)
8.456 + | Abs (_,_,body) => add_term_vars(body,vars)
8.457 + | f$t => add_term_vars (f, add_term_vars(t, vars))
8.458 + | _ => vars;
8.459 +fun term_vars t = add_term_vars(t,[]);
8.460 +
8.461 +
8.462 +fun var_perm (t, u) = (*2002 Pure/thm.ML *)
8.463 + vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
8.464 +
8.465 +(*2002 fun decomp_simp, Pure/thm.ML *)
8.466 +fun perm lhs rhs = var_perm (lhs, rhs) andalso not (lhs aconv rhs)
8.467 + andalso not (is_Var lhs);
8.468 +
8.469 +
8.470 +fun str_of_int n =
8.471 + if n < 0 then "-"^((string_of_int o abs) n)
8.472 + else string_of_int n;
8.473 +(*
8.474 +> str_of_int 1;
8.475 +val it = "1" : string > str_of_int ~1;
8.476 +val it = "-1" : string
8.477 +*)
8.478 +
8.479 +
8.480 +fun power b 0 = 1
8.481 + | power b n =
8.482 + if n>0 then b*(power b (n-1))
8.483 + else raise error ("power "^(str_of_int b)^" "^(str_of_int n));
8.484 +(*
8.485 +> power 2 3;
8.486 +val it = 8 : int
8.487 +> power ~2 3;
8.488 +val it = ~8 : int
8.489 +> power ~3 2;
8.490 +val it = 9 : int
8.491 +> power 3 ~2;
8.492 +*)
8.493 +fun gcd 0 b = b
8.494 + | gcd a b = if a < b then gcd (b mod a) a
8.495 + else gcd (a mod b) b;
8.496 +fun sign n = if n < 0 then ~1
8.497 + else if n = 0 then 0 else 1;
8.498 +fun sign2 n1 n2 = (sign n1) * (sign n2);
8.499 +
8.500 +infix dvd;
8.501 +fun d dvd n = n mod d = 0;
8.502 +
8.503 +fun divisors n =
8.504 + let fun pdiv ds d n =
8.505 + if d=n then d::ds
8.506 + else if d dvd n then pdiv (d::ds) d (n div d)
8.507 + else pdiv ds (d+1) n
8.508 + in pdiv [] 2 n end;
8.509 +
8.510 +divisors 30;
8.511 +divisors 32;
8.512 +divisors 60;
8.513 +divisors 11;
8.514 +
8.515 +fun doubles ds = (* ds is ordered *)
8.516 + let fun dbls ds [] = ds
8.517 + | dbls ds [i] = ds
8.518 + | dbls ds (i::i'::is) = if i=i' then dbls (i::ds) is
8.519 + else dbls ds (i'::is)
8.520 + in dbls [] ds end;
8.521 +(*> doubles [2,3,4];
8.522 +val it = [] : int list
8.523 +> doubles [2,3,3,5,5,7];
8.524 +val it = [5,3] : int list*)
8.525 +
8.526 +fun squfact 0 = 0
8.527 + | squfact 1 = 1
8.528 + | squfact n = foldl op* (1, (doubles o divisors) n);
8.529 +(*> squfact 30;
8.530 +val it = 1 : int
8.531 +> squfact 32;
8.532 +val it = 4 : int
8.533 +> squfact 60;
8.534 +val it = 2 : int
8.535 +> squfact 11;
8.536 +val it = 1 : int*)
8.537 +
8.538 +
8.539 +fun dest_type (Type(T,[])) = T
8.540 + | dest_type T =
8.541 + (atomtyp T;
8.542 + raise error ("... dest_type: not impl. for this type"));
8.543 +
8.544 +fun term_of_num ntyp n = Free (str_of_int n, ntyp);
8.545 +
8.546 +fun pairT T1 T2 = Type ("*", [T1, T2]);
8.547 +(*> val t = str2term "(1,2)";
8.548 +> type_of t = pairT HOLogic.realT HOLogic.realT;
8.549 +val it = true : bool
8.550 +*)
8.551 +fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
8.552 +(*> val t = str2term "(1,2)";
8.553 +> val Const ("Pair",pT) $ _ $ _ = t;
8.554 +> pT = PairT HOLogic.realT HOLogic.realT;
8.555 +val it = true : bool
8.556 +*)
8.557 +fun pairt t1 t2 =
8.558 + Const ("Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
8.559 +(*> val t = str2term "(1,2)";
8.560 +> val (t1, t2) = (str2term "1", str2term "2");
8.561 +> t = pairt t1 t2;
8.562 +val it = true : bool*)
8.563 +
8.564 +
8.565 +fun num_of_term (t as Free (s,_)) =
8.566 + (case int_of_str s of
8.567 + SOME s' => s'
8.568 + | NONE => raise error ("num_of_term not for "^ term2str t))
8.569 + | num_of_term t = raise error ("num_of_term not for "^term2str t);
8.570 +
8.571 +fun mk_factroot op_(*=thy.sqrt*) T fact root =
8.572 + Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
8.573 + (Const (op_, T --> T) $ term_of_num T root);
8.574 +(*
8.575 +val T = (type_of o term_of o the) (parse thy "#12::real");
8.576 +val t = mk_factroot "SqRoot.sqrt" T 2 3;
8.577 +(cterm_of thy) t;
8.578 +val it = "#2 * sqrt #3 " : cterm
8.579 +*)
8.580 +fun var_op_num v op_ optype ntyp n =
8.581 + Const (op_, optype) $ v $
8.582 + Free (str_of_int n, ntyp);
8.583 +
8.584 +fun num_op_var v op_ optype ntyp n =
8.585 + Const (op_,optype) $
8.586 + Free (str_of_int n, ntyp) $ v;
8.587 +
8.588 +fun num_op_num T1 T2 (op_,Top) n1 n2 =
8.589 + Const (op_,Top) $
8.590 + Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
8.591 +(*
8.592 +> val t = num_op_num "Int" 3 4;
8.593 +> atomty t;
8.594 +> string_of_cterm ((cterm_of thy) t);
8.595 +*)
8.596 +
8.597 +fun const_in str (Const _) = false
8.598 + | const_in str (Free (s,_)) = if strip_thy s = str then true else false
8.599 + | const_in str (Bound _) = false
8.600 + | const_in str (Var _) = false
8.601 + | const_in str (Abs (_,_,body)) = const_in str body
8.602 + | const_in str (f$u) = const_in str f orelse const_in str u;
8.603 +(*
8.604 +> val t = (term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
8.605 +> const_in "sqrt" t;
8.606 +val it = true : bool
8.607 +> val t = (term_of o the o (parse thy)) "6 + 5 * 4 + 3";
8.608 +> const_in "sqrt" t;
8.609 +val it = false : bool
8.610 +*)
8.611 +
8.612 +(*used for calculating built in binary operations in Isabelle2002->Float.ML*)
8.613 +(*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2
8.614 + | calc "Groups.minus_class.minus" (n1, n2) = n1-n2
8.615 + | calc "op *" (n1, n2) = n1*n2
8.616 + | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
8.617 + | calc "Atools.pow"(n1, n2) = power n1 n2
8.618 + | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
8.619 +fun calc_equ "op <" (n1, n2) = n1 < n2
8.620 + | calc_equ "op <=" (n1, n2) = n1 <= n2
8.621 + | calc_equ op_ _ =
8.622 + raise error ("calc_equ: operator = "^op_^" not defined");
8.623 +fun sqrt (n:int) = if n < 0 then 0
8.624 + (*FIXME ~~~*) else (trunc o Math.sqrt o Real.fromInt) n;
8.625 +
8.626 +fun mk_thmid thmid op_ n1 n2 =
8.627 + thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
8.628 +
8.629 +fun dest_binop_typ (Type("fun",[range,Type("fun",[arg2,arg1])])) =
8.630 + (arg1,arg2,range)
8.631 + | dest_binop_typ _ = raise error "dest_binop_typ: not binary";
8.632 +(* -----
8.633 +> val t = (term_of o the o (parse thy)) "#3^#4";
8.634 +> val hT = type_of (head_of t);
8.635 +> dest_binop_typ hT;
8.636 +val it = ("'a","nat","'a") : typ * typ * typ
8.637 + ----- *)
8.638 +
8.639 +
8.640 +(** transform binary numeralsstrings **)
8.641 +(*Makarius 100308, hacked by WN*)
8.642 +val numbers_to_string =
8.643 + let
8.644 + fun dest_num t =
8.645 + (case try HOLogic.dest_number t of
8.646 + SOME (T, i) =>
8.647 + (*if T = @{typ int} orelse T = @{typ real} then WN*)
8.648 + SOME (Free (signed_string_of_int i, T))
8.649 + (*else NONE WN*)
8.650 + | NONE => NONE);
8.651 +
8.652 + fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
8.653 + | to_str (t as (u1 $ u2)) =
8.654 + (case dest_num t of
8.655 + SOME t' => t'
8.656 + | NONE => to_str u1 $ to_str u2)
8.657 + | to_str t = perhaps dest_num t;
8.658 + in to_str end
8.659 +
8.660 +(*.make uminus uniform:
8.661 + Const ("uminus", _) $ Free ("2", "RealDef.real") --> Free ("-2", _)
8.662 +to be used immediately before evaluation of numerals;
8.663 +see Scripts/calculate.sml .*)
8.664 +(*2002 fun(*app_num_tr'2 (Const("0",T)) = Free("0",T)
8.665 + | app_num_tr'2 (Const("1",T)) = Free("1",T)
8.666 + |*)app_num_tr'2 (t as Const("uminus",_) $ Free(s,T)) =
8.667 + (case int_of_str s of SOME i =>
8.668 + if i > 0 then Free("-"^s,T) else Free(s,T)
8.669 + | NONE => t)
8.670 +(*| app_num_tr'2 (t as Const(s,T)) = t
8.671 + | app_num_tr'2 (Const("Numeral.number_of",Type ("fun", [_, T])) $ t) =
8.672 + Free(NumeralSyntax.dest_bin_str t, T)
8.673 + | app_num_tr'2 (t as Free(s,T)) = t
8.674 + | app_num_tr'2 (t as Var(n,T)) = t
8.675 + | app_num_tr'2 (t as Bound i) = t
8.676 +*)| app_num_tr'2 (Abs(s,T,body)) = Abs(s,T, app_num_tr'2 body)
8.677 + | app_num_tr'2 (t1 $ t2) = (app_num_tr'2 t1) $ (app_num_tr'2 t2)
8.678 + | app_num_tr'2 t = t;
8.679 +*)
8.680 +val uminus_to_string =
8.681 + let
8.682 + fun dest_num t =
8.683 + (case t of
8.684 + (Const ("Groups.uminus_class.uminus", _) $ Free (s, T)) =>
8.685 + (case int_of_str s of
8.686 + SOME i =>
8.687 + SOME (Free (signed_string_of_int (~1 * i), T))
8.688 + | NONE => NONE)
8.689 + | _ => NONE);
8.690 +
8.691 + fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
8.692 + | to_str (t as (u1 $ u2)) =
8.693 + (case dest_num t of
8.694 + SOME t' => t'
8.695 + | NONE => to_str u1 $ to_str u2)
8.696 + | to_str t = perhaps dest_num t;
8.697 + in to_str end;
8.698 +
8.699 +
8.700 +(*2002 fun num_str thm =
8.701 + let
8.702 + val {sign_ref = sign_ref, der = der, maxidx = maxidx,
8.703 + shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} =
8.704 + rep_thm_G thm;
8.705 + val prop' = app_num_tr'1 prop;
8.706 + in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;*)
8.707 +fun num_str thm =
8.708 + let val (deriv,
8.709 + {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps,
8.710 + hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
8.711 + val prop' = numbers_to_string prop;
8.712 + in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
8.713 +
8.714 +fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
8.715 +val it = fn : theory -> xstring -> Thm.thm*)
8.716 + Thm (xstring,
8.717 + num_str (ProofContext.get_thm (thy2ctxt' "Isac") xstring));
8.718 +
8.719 +(** get types of Free and Abs for parse' **)
8.720 +(*11.1.00: not used, fix-typed +,*,-,^ instead *)
8.721 +
8.722 +val dummyT = Type ("dummy",[]);
8.723 +val dummyT = TVar (("DUMMY",0),[]);
8.724 +
8.725 +(* assumes only 1 type for numerals
8.726 + and different identifiers for Const, Free and Abs *)
8.727 +fun get_types t =
8.728 + let
8.729 + fun get ts (Const(s,T)) = (s,T)::ts
8.730 + | get ts (Free(s,T)) = if is_no s
8.731 + then ("#",T)::ts else (s,T)::ts
8.732 + | get ts (Var(n,T)) = ts
8.733 + | get ts (Bound i) = ts
8.734 + | get ts (Abs(s,T,body)) = get ((s,T)::ts) body
8.735 + | get ts (t1 $ t2) = (get ts t1) @ (get ts t2)
8.736 + in distinct (get [] t) end;
8.737 +(*
8.738 +val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
8.739 +get_types t;
8.740 +*)
8.741 +
8.742 +(*11.1.00: not used, fix-typed +,*,-,^ instead *)
8.743 +fun set_types al (Const(s,T)) =
8.744 + (case assoc (al,s) of
8.745 + SOME T' => Const(s,T')
8.746 + | NONE => (warning ("set_types: no type for "^s); Const(s,dummyT)))
8.747 + | set_types al (Free(s,T)) =
8.748 + if is_no s then
8.749 + (case assoc (al,"#") of
8.750 + SOME T' => Free(s,T')
8.751 + | NONE => (warning ("set_types: no type for numerals"); Free(s,T)))
8.752 + else (case assoc (al,s) of
8.753 + SOME T' => Free(s,T')
8.754 + | NONE => (warning ("set_types: no type for "^s); Free(s,T)))
8.755 + | set_types al (Var(n,T)) = Var(n,T)
8.756 + | set_types al (Bound i) = Bound i
8.757 + | set_types al (Abs(s,T,body)) =
8.758 + (case assoc (al,s) of
8.759 + SOME T' => Abs(s,T', set_types al body)
8.760 + | NONE => (warning ("set_types: no type for "^s);
8.761 + Abs(s,T, set_types al body)))
8.762 + | set_types al (t1 $ t2) = (set_types al t1) $ (set_types al t2);
8.763 +(*
8.764 +val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
8.765 +val al = get_types t;
8.766 +
8.767 +val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
8.768 +atomty t; (* 'a *)
8.769 +val t' = set_types al t;
8.770 +atomty t'; (*real*)
8.771 +(cterm_of thy) t';
8.772 +val it = "x = #0 + #-1 * #-4" : cterm
8.773 +
8.774 +val t = (term_of o the o (parse thy))
8.775 + "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2";
8.776 +atomty t;
8.777 +val t' = set_types al t;
8.778 +atomty t';
8.779 +(cterm_of thy) t';
8.780 +uncaught exception TYPE (*^^^ is new, NOT in al*)
8.781 +*)
8.782 +
8.783 +
8.784 +(** from Descript.ML **)
8.785 +
8.786 +(** decompose an isa-list to an ML-list
8.787 + i.e. [] belong to the meta-language, too **)
8.788 +
8.789 +fun is_list ((Const("List.list.Cons",_)) $ _ $ _) = true
8.790 + | is_list _ = false;
8.791 +(* val (SOME ct) = parse thy "lll::real list";
8.792 +> val ty = (#t o rep_cterm) ct;
8.793 +> is_list ty;
8.794 +val it = false : bool
8.795 +> val (SOME ct) = parse thy "[lll]";
8.796 +> val ty = (#t o rep_cterm) ct;
8.797 +> is_list ty;
8.798 +val it = true : bool *)
8.799 +
8.800 +
8.801 +
8.802 +fun mk_Free (s,T) = Free(s,T);
8.803 +fun mk_free T s = Free(s,T);
8.804 +
8.805 +(*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*)
8.806 +fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*)
8.807 + let fun subst (t as Bound i, lev) =
8.808 + if i<lev then t (*var is locally bound*)
8.809 + else if i=lev then incr_boundvars lev arg
8.810 + else Bound(i-1) (*loose: change it*)
8.811 + | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
8.812 + | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
8.813 + | subst (t,lev) = t
8.814 + in subst (t,0) end;
8.815 +
8.816 +(*instantiate let; necessary for ass_up*)
8.817 +fun inst_abs thy (Const sT) = Const sT (*TODO.WN100907 drop thy*)
8.818 + | inst_abs thy (Free sT) = Free sT
8.819 + | inst_abs thy (Bound n) = Bound n
8.820 + | inst_abs thy (Var iT) = Var iT
8.821 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) =
8.822 + let val b' = subst_bound (Free (v, T2), b);
8.823 + (*fun variant_abs: term.ML*)
8.824 + in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
8.825 + | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
8.826 + | inst_abs thy t = t;
8.827 +(*val scr =
8.828 + "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
8.829 + \ (let h_ = (hd o (filterVar f_)) eqs_; \
8.830 + \ e_1 = hd (dropWhile (ident h_) eqs_); \
8.831 + \ vs_ = dropWhile (ident f_) (Vars h_); \
8.832 + \ v_1 = hd (dropWhile (ident v_) vs_); \
8.833 + \ (s_1::bool list)=(SubProblem(DiffApp_,[univar,equation],[no_met])\
8.834 + \ [BOOL e_1, REAL v_1])\
8.835 + \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
8.836 +> val ttt = (term_of o the o (parse thy)) scr;
8.837 +> tracing(term2str ttt);
8.838 +> atomt ttt;
8.839 +*** -------------
8.840 +*** Const ( DiffApp.Make'_fun'_by'_explicit)
8.841 +*** . Free ( f_, )
8.842 +*** . Free ( v_, )
8.843 +*** . Free ( eqs_, )
8.844 +*** . Const ( Let)
8.845 +*** . . Const ( Fun.op o)
8.846 +*** . . . Const ( List.hd)
8.847 +*** . . . Const ( DiffApp.filterVar)
8.848 +*** . . . . Free ( f_, )
8.849 +*** . . . Free ( eqs_, )
8.850 +*** . . Abs( h_,..
8.851 +*** . . . Const ( Let)
8.852 +*** . . . . Const ( List.hd)
8.853 +*** . . . . . Const ( List.dropWhile)
8.854 +*** . . . . . . Const ( Atools.ident)
8.855 +*** . . . . . . . Bound 0 <---- Free ( h_, )
8.856 +*** . . . . . . Free ( eqs_, )
8.857 +*** . . . . Abs( e_1,..
8.858 +*** . . . . . Const ( Let)
8.859 +*** . . . . . . Const ( List.dropWhile)
8.860 +*** . . . . . . . Const ( Atools.ident)
8.861 +*** . . . . . . . . Free ( f_, )
8.862 +*** . . . . . . . Const ( Tools.Vars)
8.863 +*** . . . . . . . . Bound 1 <---- Free ( h_, )
8.864 +*** . . . . . . Abs( vs_,..
8.865 +*** . . . . . . . Const ( Let)
8.866 +*** . . . . . . . . Const ( List.hd)
8.867 +*** . . . . . . . . . Const ( List.dropWhile)
8.868 +*** . . . . . . . . . . Const ( Atools.ident)
8.869 +*** . . . . . . . . . . . Free ( v_, )
8.870 +*** . . . . . . . . . . Bound 0 <---- Free ( vs_, )
8.871 +*** . . . . . . . . Abs( v_1,..
8.872 +*** . . . . . . . . . Const ( Let)
8.873 +*** . . . . . . . . . . Const ( Script.SubProblem)
8.874 +*** . . . . . . . . . . . Const ( Pair)
8.875 +*** . . . . . . . . . . . . Free ( DiffApp_, )
8.876 +*** . . . . . . . . . . . . Const ( Pair)
8.877 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
8.878 +*** . . . . . . . . . . . . . . Free ( univar, )
8.879 +*** . . . . . . . . . . . . . . Const ( List.list.Cons)
8.880 +*** . . . . . . . . . . . . . . . Free ( equation, )
8.881 +*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
8.882 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
8.883 +*** . . . . . . . . . . . . . . Free ( no_met, )
8.884 +*** . . . . . . . . . . . . . . Const ( List.list.Nil)
8.885 +*** . . . . . . . . . . . Const ( List.list.Cons)
8.886 +*** . . . . . . . . . . . . Const ( Script.BOOL)
8.887 +*** . . . . . . . . . . . . . Bound 2 <----- Free ( e_1, )
8.888 +*** . . . . . . . . . . . . Const ( List.list.Cons)
8.889 +*** . . . . . . . . . . . . . Const ( Script.real_)
8.890 +*** . . . . . . . . . . . . . . Bound 0 <----- Free ( v_1, )
8.891 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
8.892 +*** . . . . . . . . . . Abs( s_1,..
8.893 +*** . . . . . . . . . . . Const ( Script.Substitute)
8.894 +*** . . . . . . . . . . . . Const ( List.list.Cons)
8.895 +*** . . . . . . . . . . . . . Const ( Pair)
8.896 +*** . . . . . . . . . . . . . . Bound 1 <----- Free ( v_1, )
8.897 +*** . . . . . . . . . . . . . . Const ( Fun.op o)
8.898 +*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
8.899 +*** . . . . . . . . . . . . . . . Const ( List.hd)
8.900 +*** . . . . . . . . . . . . . . . Bound 0 <----- Free ( s_1, )
8.901 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
8.902 +*** . . . . . . . . . . . . Bound 4 <----- Free ( h_, )
8.903 +
8.904 +> val ttt' = inst_abs thy ttt;
8.905 +> tracing(term2str ttt');
8.906 +Script Make_fun_by_explicit f_ v_ eqs_ =
8.907 + ... as above ...
8.908 +> atomt ttt';
8.909 +*** -------------
8.910 +*** Const ( DiffApp.Make'_fun'_by'_explicit)
8.911 +*** . Free ( f_, )
8.912 +*** . Free ( v_, )
8.913 +*** . Free ( eqs_, )
8.914 +*** . Const ( Let)
8.915 +*** . . Const ( Fun.op o)
8.916 +*** . . . Const ( List.hd)
8.917 +*** . . . Const ( DiffApp.filterVar)
8.918 +*** . . . . Free ( f_, )
8.919 +*** . . . Free ( eqs_, )
8.920 +*** . . Abs( h_,..
8.921 +*** . . . Const ( Let)
8.922 +*** . . . . Const ( List.hd)
8.923 +*** . . . . . Const ( List.dropWhile)
8.924 +*** . . . . . . Const ( Atools.ident)
8.925 +*** . . . . . . . Free ( h_, ) <---- Bound 0
8.926 +*** . . . . . . Free ( eqs_, )
8.927 +*** . . . . Abs( e_1,..
8.928 +*** . . . . . Const ( Let)
8.929 +*** . . . . . . Const ( List.dropWhile)
8.930 +*** . . . . . . . Const ( Atools.ident)
8.931 +*** . . . . . . . . Free ( f_, )
8.932 +*** . . . . . . . Const ( Tools.Vars)
8.933 +*** . . . . . . . . Free ( h_, ) <---- Bound 1
8.934 +*** . . . . . . Abs( vs_,..
8.935 +*** . . . . . . . Const ( Let)
8.936 +*** . . . . . . . . Const ( List.hd)
8.937 +*** . . . . . . . . . Const ( List.dropWhile)
8.938 +*** . . . . . . . . . . Const ( Atools.ident)
8.939 +*** . . . . . . . . . . . Free ( v_, )
8.940 +*** . . . . . . . . . . Free ( vs_, ) <---- Bound 0
8.941 +*** . . . . . . . . Abs( v_1,..
8.942 +*** . . . . . . . . . Const ( Let)
8.943 +*** . . . . . . . . . . Const ( Script.SubProblem)
8.944 +*** . . . . . . . . . . . Const ( Pair)
8.945 +*** . . . . . . . . . . . . Free ( DiffApp_, )
8.946 +*** . . . . . . . . . . . . Const ( Pair)
8.947 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
8.948 +*** . . . . . . . . . . . . . . Free ( univar, )
8.949 +*** . . . . . . . . . . . . . . Const ( List.list.Cons)
8.950 +*** . . . . . . . . . . . . . . . Free ( equation, )
8.951 +*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
8.952 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
8.953 +*** . . . . . . . . . . . . . . Free ( no_met, )
8.954 +*** . . . . . . . . . . . . . . Const ( List.list.Nil)
8.955 +*** . . . . . . . . . . . Const ( List.list.Cons)
8.956 +*** . . . . . . . . . . . . Const ( Script.BOOL)
8.957 +*** . . . . . . . . . . . . . Free ( e_1, ) <----- Bound 2
8.958 +*** . . . . . . . . . . . . Const ( List.list.Cons)
8.959 +*** . . . . . . . . . . . . . Const ( Script.real_)
8.960 +*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 0
8.961 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
8.962 +*** . . . . . . . . . . Abs( s_1,..
8.963 +*** . . . . . . . . . . . Const ( Script.Substitute)
8.964 +*** . . . . . . . . . . . . Const ( List.list.Cons)
8.965 +*** . . . . . . . . . . . . . Const ( Pair)
8.966 +*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 1
8.967 +*** . . . . . . . . . . . . . . Const ( Fun.op o)
8.968 +*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
8.969 +*** . . . . . . . . . . . . . . . Const ( List.hd)
8.970 +*** . . . . . . . . . . . . . . . Free ( s_1, ) <----- Bound 0
8.971 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
8.972 +*** . . . . . . . . . . . . Free ( h_, ) <----- Bound 4
8.973 +
8.974 +Note numbering of de Bruijn indexes !
8.975 +
8.976 +Script Make_fun_by_explicit f_ v_ eqs_ =
8.977 + let h_ = (hd o filterVar f_) eqs_;
8.978 + e_1 = hd (dropWhile (ident h_ BOUND_0) eqs_);
8.979 + vs_ = dropWhile (ident f_) (Vars h_ BOUND_1);
8.980 + v_1 = hd (dropWhile (ident v_) vs_ BOUND_0);
8.981 + s_1 =
8.982 + SubProblem (DiffApp_, [univar, equation], [no_met])
8.983 + [BOOL e_1 BOUND_2, REAL v_1 BOUND_0]
8.984 + in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4
8.985 +*)
8.986 +
8.987 +
8.988 +fun T_a2real (Type (s, [])) =
8.989 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
8.990 + | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
8.991 + | T_a2real (TFree (s, srt)) =
8.992 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
8.993 + | T_a2real (TVar (("DUMMY",_),srt)) = HOLogic.realT;
8.994 +
8.995 +(*FIXME .. fixes the type (+see Typefix.thy*)
8.996 +fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T))
8.997 + | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
8.998 + | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
8.999 + | typ_a2real (Bound i) = (Bound i)
8.1000 + | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
8.1001 + | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
8.1002 +(*
8.1003 +----------------6.8.02---------------------------------------------------
8.1004 + val str = "1";
8.1005 + val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
8.1006 + atomty (term_of t);
8.1007 +*** -------------
8.1008 +*** Const ( 1, 'a)
8.1009 + val t = (app_num_tr' o term_of) t;
8.1010 + atomty t;
8.1011 +*** -------------
8.1012 +*** Const ( 1, 'a)
8.1013 + val t = typ_a2real t;
8.1014 + atomty t;
8.1015 +*** -------------
8.1016 +*** Const ( 1, real)
8.1017 +
8.1018 + val str = "2";
8.1019 + val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
8.1020 + atomty (term_of t);
8.1021 +*** -------------
8.1022 +*** Const ( Numeral.number_of, bin => 'a)
8.1023 +*** . Const ( Numeral.bin.Bit, [bin, bool] => bin)
8.1024 +*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
8.1025 +*** . . . Const ( Numeral.bin.Pls, bin)
8.1026 +*** . . . Const ( True, bool)
8.1027 +*** . . Const ( False, bool)
8.1028 + val t = (app_num_tr' o term_of) t;
8.1029 + atomty t;
8.1030 +*** -------------
8.1031 +*** Free ( 2, 'a)
8.1032 + val t = typ_a2real t;
8.1033 + atomty t;
8.1034 +*** -------------
8.1035 +*** Free ( 2, real)
8.1036 +----------------6.8.02---------------------------------------------------
8.1037 +
8.1038 +
8.1039 +> val str = "R";
8.1040 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
8.1041 +val t = Free ("R","?DUMMY") : term
8.1042 +> val t' = typ_a2real t;
8.1043 +> (cterm_of thy) t';
8.1044 +val it = "R::RealDef.real" : cterm
8.1045 +
8.1046 +> val str = "R=R";
8.1047 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
8.1048 +> atomty (typ_a2real t);
8.1049 +*** -------------
8.1050 +*** Const ( op =, [RealDef.real, RealDef.real] => bool)
8.1051 +*** Free ( R, RealDef.real)
8.1052 +*** Free ( R, RealDef.real)
8.1053 +> val t' = typ_a2real t;
8.1054 +> (cterm_of thy) t';
8.1055 +val it = "(R::RealDef.real) = R" : cterm
8.1056 +
8.1057 +> val str = "fixed_values [R=R]";
8.1058 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
8.1059 +> val t' = typ_a2real t;
8.1060 +> (cterm_of thy) t';
8.1061 +val it = "fixed_values [(R::RealDef.real) = R]" : cterm
8.1062 +*)
8.1063 +
8.1064 +(*TODO.WN0609: parse should return a term or a string
8.1065 + (or even more comprehensive datastructure for error-messages)
8.1066 + i.e. in wrapping with SOME term or NONE the latter is not sufficient*)
8.1067 +(*2002 fun parseold thy str =
8.1068 + (let
8.1069 + val sgn = sign_of thy;
8.1070 + val t = ((*typ_a2real o*) app_num_tr'1 o term_of)
8.1071 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
8.1072 + in SOME (cterm_of sgn t) end)
8.1073 + handle _ => NONE;*)
8.1074 +
8.1075 +
8.1076 +
8.1077 +fun parseold thy str =
8.1078 + (let val t = ((*typ_a2real o*) numbers_to_string)
8.1079 + (Syntax.read_term_global thy str)
8.1080 + in SOME (cterm_of thy t) end)
8.1081 + handle _ => NONE;
8.1082 +(*2002 fun parseN thy str =
8.1083 + (let
8.1084 + val sgn = sign_of thy;
8.1085 + val t = ((*typ_a2real o app_num_tr'1 o*) term_of)
8.1086 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
8.1087 + in SOME (cterm_of sgn t) end)
8.1088 + handle _ => NONE;*)
8.1089 +fun parseN thy str =
8.1090 + (let val t = (*(typ_a2real o numbers_to_string)*)
8.1091 + (Syntax.read_term_global thy str)
8.1092 + in SOME (cterm_of thy t) end)
8.1093 + handle _ => NONE;
8.1094 +(*2002 fun parse thy str =
8.1095 + (let
8.1096 + val sgn = sign_of thy;
8.1097 + val t = (typ_a2real o app_num_tr'1 o term_of)
8.1098 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
8.1099 + in SOME (cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
8.1100 + handle _ => NONE;*)
8.1101 +(*2010 fun parse thy str =
8.1102 + (let val t = (typ_a2real o app_num_tr'1) (Syntax.read_term_global thy str)
8.1103 + in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
8.1104 + handle _ => NONE;*)
8.1105 +fun parse thy str =
8.1106 + (let val t = (typ_a2real o numbers_to_string)
8.1107 + (Syntax.read_term_global thy str)
8.1108 + in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
8.1109 + handle _ => NONE;
8.1110 +(*
8.1111 +> val (SOME ct) = parse thy "(-#5)^^^#3";
8.1112 +> atomty (term_of ct);
8.1113 +*** -------------
8.1114 +*** Const ( Nat.op ^, ['a, nat] => 'a)
8.1115 +*** Const ( uminus, 'a => 'a)
8.1116 +*** Free ( #5, 'a)
8.1117 +*** Free ( #3, nat)
8.1118 +> val (SOME ct) = parse thy "R=R";
8.1119 +> atomty (term_of ct);
8.1120 +*** -------------
8.1121 +*** Const ( op =, [real, real] => bool)
8.1122 +*** Free ( R, real)
8.1123 +*** Free ( R, real)
8.1124 +
8.1125 +THIS IS THE OUTPUT FOR VERSION (3) above at typ_a2real !!!!!
8.1126 +*** -------------
8.1127 +*** Const ( op =, [RealDef.real, RealDef.real] => bool)
8.1128 +*** Free ( R, RealDef.real)
8.1129 +*** Free ( R, RealDef.real) *)
8.1130 +
8.1131 +fun parse_patt thy str =
8.1132 + ProofContext.read_term_pattern (thy2ctxt thy) str;
8.1133 +
8.1134 +(*version for testing local to theories*)
8.1135 +fun str2term_ thy str = (term_of o the o (parse thy)) str;
8.1136 +fun str2term str = (term_of o the o (parse (theory "Isac"))) str;
8.1137 +fun strs2terms ss = map str2term ss;
8.1138 +fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str;
8.1139 +
8.1140 +(*+ makes a substitution from the output of Pattern.match +*)
8.1141 +(*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)
8.1142 +fun mk_subs (subs: ((string * int) * (Term.typ * Term.term)) list) =
8.1143 +let fun mk_sub ((id, _), (ty, tm)) = (Free (id, ty), tm) in
8.1144 +map mk_sub subs end;
8.1145 +
8.1146 +val atomthm = atomt o #prop o rep_thm;
8.1147 +
8.1148 +(*.instantiate #prop thm with bound variables (as Free).*)
8.1149 +fun inst_bdv [] t = t : term
8.1150 + | inst_bdv (instl: (term*term) list) t =
8.1151 + let fun subst (v as Var((s,_),T)) =
8.1152 + (case explode s of
8.1153 + "b"::"d"::"v"::_ =>
8.1154 + if_none (assoc(instl,Free(s,T))) (Free(s,T))
8.1155 + | _ => v)
8.1156 + | subst (Abs(a,T,body)) = Abs(a, T, subst body)
8.1157 + | subst (f$t') = subst f $ subst t'
8.1158 + | subst t = if_none (assoc(instl,t)) t
8.1159 + in subst t end;
8.1160 +
8.1161 +
8.1162 +(*WN050829 caution: is_atom (str2term"q_0/2 * L * x") = true !!!
8.1163 + use length (vars term) = 1 instead*)
8.1164 +fun is_atom (Const ("Float.Float",_) $ _) = true
8.1165 + | is_atom (Const ("ComplexI.I'_'_",_)) = true
8.1166 + | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
8.1167 + | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
8.1168 + | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $
8.1169 + (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
8.1170 + is_atom t1 andalso is_atom t2
8.1171 + | is_atom (Const _) = true
8.1172 + | is_atom (Free _) = true
8.1173 + | is_atom (Var _) = true
8.1174 + | is_atom _ = false;
8.1175 +(* val t = str2term "q_0/2 * L * x";
8.1176 +
8.1177 +
8.1178 +*)
8.1179 +(*val t = str2term "Float ((1,2),(0,0))";
8.1180 +> is_atom t;
8.1181 +val it = true : bool
8.1182 +> val t = str2term "Float ((1,2),(0,0)) * I__";
8.1183 +> is_atom t;
8.1184 +val it = true : bool
8.1185 +> val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
8.1186 +> is_atom t;
8.1187 +val it = true : bool
8.1188 +> val t = str2term "1 + 2*I__";
8.1189 +> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
8.1190 +*)
8.1191 +
8.1192 +(*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
8.1193 + have found a substitution (required for evaluating the preconditions
8.1194 + of _incomplete_ models).*)
8.1195 +fun subst_atomic_all [] t = (false, (*TODO may be 'true' for some terms ?*)
8.1196 + t : term)
8.1197 + | subst_atomic_all (instl: (term*term) list) t =
8.1198 + let fun subst (Abs(a,T,body)) =
8.1199 + let val (all, body') = subst body
8.1200 + in (all, Abs(a, T, body')) end
8.1201 + | subst (f$tt) =
8.1202 + let val (all1, f') = subst f
8.1203 + val (all2, tt') = subst tt
8.1204 + in (all1 andalso all2, f' $ tt') end
8.1205 + | subst (t as Free _) =
8.1206 + if is_num t then (true, t) (*numerals cannot be subst*)
8.1207 + else (case assoc(instl,t) of
8.1208 + SOME t' => (true, t')
8.1209 + | NONE => (false, t))
8.1210 + | subst t = (true, if_none (assoc(instl,t)) t)
8.1211 + in subst t end;
8.1212 +
8.1213 +(*.add two terms with a type given.*)
8.1214 +fun mk_add t1 t2 =
8.1215 + let val T1 = type_of t1
8.1216 + val T2 = type_of t2
8.1217 + in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2])
8.1218 + else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
8.1219 + end;
8.1220 +
9.1 --- a/src/Tools/isac/Test_Isac.thy Mon Sep 27 13:35:06 2010 +0200
9.2 +++ b/src/Tools/isac/Test_Isac.thy Tue Sep 28 07:28:10 2010 +0200
9.3 @@ -27,37 +27,21 @@
9.4 cd "../..";
9.5 *)
9.6 ML{* writeln "**** run systests complete ******************************" *};
9.7 -
9.8 -ML {*
9.9 -val t1 = @{term "1+2::real"};
9.10 -val t2 = @{term "abc"};
9.11 -term2str t2 = "abc";
9.12 -fun terms2str ts = (strs2str o (map term2str )) ts;
9.13 -terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";
9.14 -fun terms2str' ts = (strs2str' o (map term2str )) ts;
9.15 -terms2str' [t1,t2] = "[1 + 2,abc]";
9.16 -fun terms2strs ts = (map term2str) ts;
9.17 -terms2strs [t1,t2] = ["1 + 2", "abc"];
9.18 -*}
9.19 -
9.20 (*
9.21 cd"smltest/Scripts";
9.22 - use"calculate-float.sml";
9.23 *)
9.24 -use"ProgLang/calculate.sml"; (*part.*)
9.25 +use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
9.26 +use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
9.27 +use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*part.*)
9.28 (*
9.29 use"listg.sml";
9.30 -*)
9.31 -use"ProgLang/rewrite.sml"; (*part.*)
9.32 -(*
9.33 use"scrtools.sml";
9.34 - use"term.sml";
9.35 use"tools.sml";
9.36 cd "../..";
9.37 cd"smltest/ME";
9.38 use"ctree.sml";
9.39 *)
9.40 -use "Interpret/calchead.sml" (*part.*)
9.41 +use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
9.42 (*
9.43 use"calchead.sml";
9.44 use"rewtools.sml";
9.45 @@ -89,7 +73,7 @@
9.46 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
9.47 use"logexp.sml";
9.48 *)
9.49 -use"Knowledge/poly.sml"; (*part.*)
9.50 +use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
9.51 (*
9.52 use"polyminus.sml";
9.53 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
9.54 @@ -119,12 +103,12 @@
9.55
9.56 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
9.57 *)
9.58 -use_thy "../../Pure/Isar/Test_Parse_Term"
9.59 -use_thy "../../Pure/Isar/Test_Parsers"
9.60 +use_thy "../../../test/Pure/Isar/Test_Parse_Term"
9.61 +use_thy "../../../test/Pure/Isar/Test_Parsers"
9.62
9.63 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
9.64 (*
9.65 -val path = "/home/neuper/proto2/testsml2xml/";
9.66 +val path = "/home/neuper/proto3/testsml2xml/";
9.67 pbl_hierarchy2file (path ^ "pbl/");
9.68 pbls2file (path ^ "pbl/");
9.69 met_hierarchy2file (path ^ "met/");
10.1 --- a/test/Tools/isac/ProgLang/calculate-float.sml Mon Sep 27 13:35:06 2010 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,147 +0,0 @@
10.4 -(* (c) Stefan Rath 2005
10.5 - tests for sml/Scripts/calculate.sml
10.6 -
10.7 - use"~/proto2/isac/src/smltest/Scripts/calculate-float.sml";
10.8 - use"calculate-float.sml";
10.9 - *)
10.10 -
10.11 -
10.12 -(*WN.28.3.03 fuer Matthias*)
10.13 -(*Floatingpointnumbers, direkte Darstellung der abstrakten Syntax:*)
10.14 - val thy = Float.thy;
10.15 - val t = str2term "Float ((1,2),(0,0))";
10.16 - atomt t;
10.17 - val t = (term_of o the o (parse thy))
10.18 - "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * \
10.19 - \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
10.20 - atomt t;
10.21 -(*die konkrete Syntax wird noch verschoenert*)
10.22 -
10.23 - val thy = "Test.thy";
10.24 - val op_ = "divide_";
10.25 - val ct = "-6 / 3";
10.26 - val SOME (ct,_) = calculate thy (the (assoc (calclist, op_))) ct;
10.27 -
10.28 -(*-----WN050315------------------------------------------------------*)
10.29 -(*..*)
10.30 -val t = str2term "Float ((1,2),(0,0))";
10.31 -atomty t;
10.32 -val Const ("Float.Float",_) $
10.33 - (Const ("Pair",_) $
10.34 - (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;
10.35 -
10.36 -val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
10.37 -atomty t;
10.38 -(*-----WN050315------------------------------------------------------*)
10.39 -
10.40 -
10.41 -val thy = Float.thy;
10.42 -
10.43 -(*.calculate the value of a pair of floats.*)
10.44 -val ((a,b),(c,d)) = calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
10.45 -
10.46 -
10.47 -(*.build the term.*)
10.48 -term_of_float HOLogic.realT ((~1,0),(0,0));
10.49 -term_of_float HOLogic.realT ((~1,11),(0,0));
10.50 -
10.51 -(*--18.3.05-------------------------*)
10.52 -val t = Free ("sdfsdfsdf", HOLogic.realT);
10.53 -val t = Free ("-123,456", HOLogic.realT);
10.54 -val t = Free ("0,123456", HOLogic.realT);
10.55 -term2str t;
10.56 -(*----(1)------------------------------*)
10.57 -val t = str2term "IFloat (1, 2, 3)";
10.58 -val t = str2term "CFloat (1, 2)";
10.59 -atomt t;
10.60 -atomty t;
10.61 -val SOME ct = parse Float.thy "IFloat (1, 2, 3)";
10.62 -val SOME ct = parse Float.thy "CFloat (1, 2)";
10.63 -atomt (term_of ct);
10.64 -atomty (term_of ct);
10.65 -(*----(2)------------------------------*)
10.66 -val SOME ct = parse Float.thy "IFloat (-1, 2, 3)";
10.67 -val t = (term_of ct);
10.68 -atomty t;
10.69 -(*#######################################################################3
10.70 -val Const
10.71 - ("Float.IFloat", _) $
10.72 - (Const
10.73 - ("Pair", _) $
10.74 - Free (no, _) $
10.75 - (Const
10.76 - ("Pair", _) $
10.77 - Free (commas, _) $ Free (exp, _))) = t;
10.78 -
10.79 -fun IFloat2CFloat
10.80 - (Const
10.81 - ("Float.IFloat", _) $
10.82 - (Const
10.83 - ("Pair", _) $
10.84 - Free (no, _) $
10.85 - (Const
10.86 - ("Pair", _) $
10.87 - Free (commas, _) $ Free (exp, _)))) =
10.88 - Const ("Float.CFloat", HOLogic.realT(*wrong type*)) $
10.89 - (Const
10.90 - ("Pair", HOLogic.realT(*wrong type*)) $
10.91 - Free (no^"."^commas, HOLogic.realT)
10.92 - $ Free ("accuracy", HOLogic.realT))
10.93 -
10.94 - | IFloat2CFloat t =
10.95 - raise error ("IFloat2CFloat: invalid argument "^term2str t);
10.96 -
10.97 -val cf = IFloat2CFloat t;
10.98 -term2str cf;
10.99 -
10.100 -(*in IsacKnowledge/Float.ML: fun pairt -> Pair-term*)
10.101 -
10.102 -fun CFloat2Free (Const ("Float.CFloat", _) $
10.103 - (Const ("Pair", _) $ Free (no_commas, _) $ _)) =
10.104 - Free (no_commas, HOLogic.realT);
10.105 -
10.106 -val t' = CFloat2Free cf;
10.107 -term2str t';
10.108 -
10.109 -fun CFloat2sml (Const ("Float.CFloat", _) $
10.110 - (Const ("Pair", _) $ Free (float, _) $ _(**))) =
10.111 - float;
10.112 -CFloat2sml cf;
10.113 -
10.114 -(*--18.3.05-------------------------*)
10.115 -
10.116 -
10.117 -(*.the function evaluating a binary operator.*)
10.118 -val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
10.119 -val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" t thy;
10.120 -term2str t;
10.121 -
10.122 -
10.123 -(*.scan a term for a pair of floats.*)
10.124 - val SOME (thmid,t') = get_pair thy op_ eval_fn t;
10.125 -
10.126 -
10.127 -(*.use 'calculate' explicitly.*)
10.128 - val thy = Test.thy;
10.129 - val op_ = "divide_";
10.130 - val t = str2term "sqrt (x ^^^ 2 + -3 * x) =\
10.131 - \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
10.132 - val SOME (t',_) = calculate_ thy (the (assoc (calclist, op_))) t;
10.133 - term2str t';
10.134 -
10.135 -
10.136 -(*.rewrite with ruleset TEST...simplify (calling calculate internally.*)
10.137 -val t = str2term "a + Float ((1,2),(0,0)) + a + Float ((3,4),(0,0)) * \
10.138 - \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
10.139 -val SOME (t',_) = rewrite_set_ thy false norm_Rational(*///*) t; term2str t';
10.140 -(*Float ((...,...) + 2*a*)
10.141 -
10.142 -
10.143 -(*. parse a float as seen by the user .*)
10.144 -val SOME t = parse Float.thy "123.456";
10.145 -val SOME t = parse Float.thy "-123.456";
10.146 -val SOME t = parse Float.thy "123.456 E6789";
10.147 -val SOME t = parse Float.thy "123.456 E-6789";
10.148 -val SOME t = parse Float.thy "-123.456 E-6789";
10.149 -
10.150 -################################################################*)
11.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Sep 27 13:35:06 2010 +0200
11.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 07:28:10 2010 +0200
11.3 @@ -14,7 +14,7 @@
11.4 "----------- test rewriting without Isac's thys ---------";
11.5 "----------- conditional rewriting without Isac's thys --";
11.6 "----------- step through 'and rew_sub': ----------------";
11.7 -"----------- rewrite_terms_ ----------------------------";
11.8 +"----------- step through 'fun rewrite_terms_' ---------";
11.9 "----------- rewrite_inst_ bdvs -------------------------";
11.10 "----------- check diff 2002--2009-3 --------------------";
11.11 "--------------------------------------------------------";
11.12 @@ -155,6 +155,7 @@
11.13 "----------- step through 'and rew_sub': ----------------";
11.14 "----------- step through 'and rew_sub': ----------------";
11.15 (*and make asms without Trueprop, beginning with the result:*)
11.16 +val tm = @{term "x*y / y::real"};
11.17 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
11.18 show_types := false;
11.19 "----- evaluate arguments";
11.20 @@ -163,11 +164,11 @@
11.21 "----- step 1: lhs, rhs of rule";
11.22 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
11.23 o Logic.strip_imp_concl) r;
11.24 -term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
11.25 +term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
11.26 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
11.27 "----- step 2: the rule instantiated";
11.28 - val r' = Envir.subst_term (Pattern.match thy (lhs, t)
11.29 - (Vartab.empty, Vartab.empty)) r;
11.30 + val r' = Envir.subst_term
11.31 + (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
11.32 term2str r' = "y ~= 0 ==> x * y / y = x";
11.33 "----- step 3: get the (instantiated) assumption(s)";
11.34 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
11.35 @@ -185,28 +186,38 @@
11.36 o Logic.strip_imp_concl) r';
11.37 term2str t' = "x";
11.38
11.39 -(*===== inhibit exn ============================================================
11.40 -"----------- rewrite_terms_ ----------------------------";
11.41 -"----------- rewrite_terms_ ----------------------------";
11.42 -"----------- rewrite_terms_ ----------------------------";
11.43 -val subte = [str2term "x = 0"];
11.44 -val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
11.45 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; (*NONE..TODO*)
11.46 +"----------- step through 'fun rewrite_terms_' ---------";
11.47 +"----------- step through 'fun rewrite_terms_' ---------";
11.48 +"----------- step through 'fun rewrite_terms_' ---------";
11.49 +"----- step 0: args for rewrite_terms_, local fun";
11.50 +val (thy, ord, erls, equs, t) =
11.51 + (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
11.52 + str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
11.53 +"----- step 1: args for rew_";
11.54 +val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
11.55 +"----- step 2: rew_sub";
11.56 +rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
11.57 +"----- step 3: step through rew_sub -- inefficient: goes into subterms";
11.58 +
11.59 +
11.60 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
11.61 +writeln "----------- rewrite_terms_ 1---------------------------";
11.62 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
11.63 else raise error "rewrite.sml rewrite_terms_ [x = 0]";
11.64
11.65 -val subte = [str2term "M_b 0 = 0"];
11.66 -val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
11.67 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
11.68 +val equs = [str2term "M_b 0 = 0"];
11.69 +val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
11.70 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
11.71 +writeln "----------- rewrite_terms_ 2---------------------------";
11.72 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
11.73 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
11.74
11.75 -val subte = [str2term"x = 0", str2term"M_b 0 = 0"];
11.76 -val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
11.77 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
11.78 +val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
11.79 +val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
11.80 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
11.81 +writeln "----------- rewrite_terms_ 3---------------------------";
11.82 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
11.83 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
11.84 -===== inhibit exn ============================================================*)
11.85
11.86
11.87 "----------- rewrite_inst_ bdvs -------------------------";
11.88 @@ -233,6 +244,7 @@
11.89 trace_rewrite:=true;
11.90 trace_rewrite:=false;--------------------------------------------*)
11.91
11.92 +
11.93 "----------- check diff 2002--2009-3 --------------------";
11.94 "----------- check diff 2002--2009-3 --------------------";
11.95 "----------- check diff 2002--2009-3 --------------------";
11.96 @@ -323,3 +335,10 @@
11.97 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
11.98 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
11.99 "--------------------------------------------------------";
11.100 +
11.101 +
11.102 +(*===== inhibit exn ============================================================
11.103 +===== inhibit exn ============================================================*)
11.104 +
11.105 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.
11.106 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.*)
12.1 --- a/test/Tools/isac/ProgLang/term.sml Mon Sep 27 13:35:06 2010 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,168 +0,0 @@
12.4 -(* tests on Scripts/term_G.sml
12.5 - author: Walther Neuper
12.6 - 051006,
12.7 - (c) due to copyright terms
12.8 -
12.9 -use"../smltest/Scripts/term_G.sml";
12.10 -use"term_G.sml";
12.11 -*)
12.12 -
12.13 -"-----------------------------------------------------------------";
12.14 -"table of contents -----------------------------------------------";
12.15 -"-----------------------------------------------------------------";
12.16 -"----------- inst_bdv --------------------------------------------";
12.17 -"----------- subst_atomic_all ------------------------------------";
12.18 -"----------- Pattern.match ---------------------------------------";
12.19 -"----------- fun matches -----------------------------------------";
12.20 -"------------parse------------------------------------------------";
12.21 -"----------- uminus_to_string ------------------------------------";
12.22 -"-----------------------------------------------------------------";
12.23 -"-----------------------------------------------------------------";
12.24 -
12.25 -
12.26 -"----------- inst_bdv --------------------------------------------";
12.27 -"----------- inst_bdv --------------------------------------------";
12.28 -"----------- inst_bdv --------------------------------------------";
12.29 -if string_of_thm (num_str @{thm d1_isolate_add2}) =
12.30 - "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
12.31 -else raise error "term_G.sml d1_isolate_add2";
12.32 -val subst = [(str2term "bdv", str2term "x")];
12.33 -val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
12.34 -val t' = inst_bdv subst t;
12.35 -if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
12.36 -else raise error "term_G.sml inst_bdv 1";
12.37 -
12.38 -if string_of_thm (num_str @{thm separate_bdvs_add}) =
12.39 - "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
12.40 - \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
12.41 -else raise error "term_G.sml separate_bdvs_add";
12.42 -val subst = [(str2term"bdv_1",str2term"c"),
12.43 - (str2term"bdv_2",str2term"c_2"),
12.44 - (str2term"bdv_3",str2term"c_3"),
12.45 - (str2term"bdv_4",str2term"c_4")];
12.46 -val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
12.47 -val t' = inst_bdv subst t;
12.48 -if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
12.49 - \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
12.50 -else raise error "term_G.sml inst_bdv 2";
12.51 -
12.52 -
12.53 -"----------- subst_atomic_all ------------------------------------";
12.54 -"----------- subst_atomic_all ------------------------------------";
12.55 -"----------- subst_atomic_all ------------------------------------";
12.56 -val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
12.57 -val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
12.58 - (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
12.59 -val (all_Free_subst, t') = subst_atomic_all env t;
12.60 -if all_Free_subst andalso
12.61 - term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
12.62 -else raise error "term_G.sml subst_atomic_all should be 'true'";
12.63 -
12.64 -
12.65 -val (all_Free_subst, t') = subst_atomic_all (tl env) t;
12.66 -if not all_Free_subst andalso
12.67 - term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
12.68 -else raise error "term_G.sml subst_atomic_all should be 'false'";
12.69 -
12.70 -
12.71 -"----------- Pattern.match ---------------------------------------";
12.72 -"----------- Pattern.match ---------------------------------------";
12.73 -"----------- Pattern.match ---------------------------------------";
12.74 -val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
12.75 -val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
12.76 -(* !^^^^^^^^!... necessary for Pattern.match*)
12.77 -val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
12.78 -(*val insts =
12.79 - ([],
12.80 - [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
12.81 - (("a",0),Free ("3","RealDef.real"))])
12.82 - : (indexname * typ) list * (indexname * term) list*)
12.83 -
12.84 -"----- throws exn MATCH...";
12.85 -val t = str2term "x";
12.86 -(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
12.87 -handle MATCH => ([(* (Term.indexname * Term.typ) *)],
12.88 - [(* (Term.indexname * Term.term) *)]);
12.89 -Pattern.MATCH;
12.90 -
12.91 -(*ML {**)
12.92 -val thy = @{theory "Complex_Main"};
12.93 -val PARSE = Syntax.read_term_global thy;
12.94 -val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
12.95 -"-------";
12.96 -val (tye, tme) =
12.97 - (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
12.98 -"-------";
12.99 -val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty,
12.100 - Vartab.empty);
12.101 -"-------";
12.102 -val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
12.103 - (Vartab.empty, Vartab.empty);
12.104 -Vartab.dest tenv;
12.105 -match thy tm (Logic.varify pa);
12.106 -
12.107 -(**}*)
12.108 -
12.109 -"----------- fun matches -----------------------------------------";
12.110 -"----------- fun matches -----------------------------------------";
12.111 -"----------- fun matches -----------------------------------------";
12.112 -(*smltest/IsacKnowledge/polyeq.sml:
12.113 - Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
12.114 -(*smltest/ME/ptyps.sml:
12.115 - |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
12.116 -(*ML {**)
12.117 -val thy = @{theory "Complex_Main"};
12.118 -"----- test 1";
12.119 -val pa = Logic.varify @{term "a = (0::real)"};
12.120 -"----- test 1 true";
12.121 -val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
12.122 -if matches thy tm pa then ()
12.123 - else error "term_G.sml diff.behav. in matches true";
12.124 -"----- test 2 false";
12.125 -val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
12.126 -if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
12.127 - else ();
12.128 -(**}*)
12.129 -
12.130 -"------------parse------------------------------------------------";
12.131 -"------------parse------------------------------------------------";
12.132 -"------------parse------------------------------------------------";
12.133 -(*ML {**)
12.134 -Toplevel.debug := true;
12.135 -(* literal types:
12.136 -PolyML.addPrettyPrinter
12.137 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
12.138 -*)(* pretty types:
12.139 -PolyML.addPrettyPrinter
12.140 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
12.141 -print_depth 99;
12.142 -*)
12.143 -val thy = @{theory "Complex_Main"};
12.144 -val str = "x + z";
12.145 -parse thy str;
12.146 -"---------------";
12.147 -val str = "x + 2*z";
12.148 -val t = (Syntax.read_term_global thy str);
12.149 -val t = numbers_to_string (Syntax.read_term_global thy str);
12.150 -val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
12.151 -cterm_of thy t;
12.152 -val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
12.153 -(**}*)
12.154 -(*Makarius.1003
12.155 -ML {* @{term "2::int"} *}
12.156 -
12.157 -term "(1.24444) :: real"
12.158 -
12.159 -ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
12.160 -*)
12.161 -
12.162 -
12.163 -"----------- uminus_to_string ------------------------------------";
12.164 -"----------- uminus_to_string ------------------------------------";
12.165 -"----------- uminus_to_string ------------------------------------";
12.166 -(*ML {*)
12.167 -val t1 = numbers_to_string @{term "-2::real"};
12.168 -val t2 = numbers_to_string @{term "- 2::real"};
12.169 -if uminus_to_string t2 = t1 then ()
12.170 -else error "term_G.sml diff.behav. in uminus_to_string";
12.171 -(*}*)
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/ProgLang/termC.sml Tue Sep 28 07:28:10 2010 +0200
13.3 @@ -0,0 +1,219 @@
13.4 +(* Title: tests on ProgLang/termC.sml
13.5 + Author: Walther Neuper 051006,
13.6 + (c) due to copyright terms
13.7 +*)
13.8 +"--------------------------------------------------------";
13.9 +"table of contents --------------------------------------";
13.10 +"--------------------------------------------------------";
13.11 +"----------- inst_bdv -----------------------------------";
13.12 +"----------- subst_atomic_all ---------------------------";
13.13 +"----------- Pattern.match ------------------------------";
13.14 +"----------- fun matches --------------------------------";
13.15 +"------------parse---------------------------------------";
13.16 +"----------- uminus_to_string ---------------------------";
13.17 +"--------------------------------------------------------";
13.18 +"--------------------------------------------------------";
13.19 +
13.20 +
13.21 +(*===== inhibit exn ============================================================
13.22 +"----------- inst_bdv -----------------------------------";
13.23 +"----------- inst_bdv -----------------------------------";
13.24 +"----------- inst_bdv -----------------------------------";
13.25 +if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
13.26 + "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then ()
13.27 +else raise error "termC.sml d1_isolate_add2";
13.28 +val subst = [(str2term "bdv", str2term "x")];
13.29 +val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
13.30 +val t' = inst_bdv subst t;
13.31 +if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
13.32 +else raise error "termC.sml inst_bdv 1";
13.33 +
13.34 +if string_of_thm (num_str @{thm separate_bdvs_add}) =
13.35 + "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
13.36 + \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
13.37 +else raise error "termC.sml separate_bdvs_add";
13.38 +val subst = [(str2term"bdv_1",str2term"c"),
13.39 + (str2term"bdv_2",str2term"c_2"),
13.40 + (str2term"bdv_3",str2term"c_3"),
13.41 + (str2term"bdv_4",str2term"c_4")];
13.42 +val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
13.43 +val t' = inst_bdv subst t;
13.44 +if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
13.45 + \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
13.46 +else raise error "termC.sml inst_bdv 2";
13.47 +
13.48 +
13.49 +"----------- subst_atomic_all ---------------------------";
13.50 +"----------- subst_atomic_all ---------------------------";
13.51 +"----------- subst_atomic_all ---------------------------";
13.52 +val t = str2term "(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
13.53 +val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
13.54 + (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
13.55 +val (all_Free_subst, t') = subst_atomic_all env t;
13.56 +if all_Free_subst andalso
13.57 + term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
13.58 +else raise error "termC.sml subst_atomic_all should be 'true'";
13.59 +
13.60 +
13.61 +val (all_Free_subst, t') = subst_atomic_all (tl env) t;
13.62 +if not all_Free_subst andalso
13.63 + term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
13.64 +else raise error "termC.sml subst_atomic_all should be 'false'";
13.65 +===== inhibit exn ============================================================*)
13.66 +
13.67 +
13.68 +"----------- Pattern.match ------------------------------";
13.69 +"----------- Pattern.match ------------------------------";
13.70 +"----------- Pattern.match ------------------------------";
13.71 +(*===== inhibit exn ============================================================
13.72 +val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
13.73 +val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
13.74 +(* !^^^^^^^^!... necessary for Pattern.match*)
13.75 +val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
13.76 +(*val insts =
13.77 + ([],
13.78 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
13.79 + (("a",0),Free ("3","RealDef.real"))])
13.80 + : (indexname * typ) list * (indexname * term) list*)
13.81 +
13.82 +"----- throws exn MATCH...";
13.83 +val t = str2term "x";
13.84 +(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
13.85 +handle MATCH => ([(* (Term.indexname * Term.typ) *)],
13.86 + [(* (Term.indexname * Term.term) *)]);
13.87 +Pattern.MATCH;
13.88 +
13.89 +val thy = @{theory "Complex_Main"};
13.90 +val PARSE = Syntax.read_term_global thy;
13.91 +val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
13.92 +"-------";
13.93 +val (tye, tme) =
13.94 + (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
13.95 +"-------";
13.96 +val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty,
13.97 + Vartab.empty);
13.98 +"-------";
13.99 +val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm)
13.100 + (Vartab.empty, Vartab.empty);
13.101 +Vartab.dest tenv;
13.102 +match thy tm (Logic.varify pa);
13.103 +===== inhibit exn ============================================================*)
13.104 +
13.105 +"----------- fun matches --------------------------------";
13.106 +"----------- fun matches --------------------------------";
13.107 +"----------- fun matches --------------------------------";
13.108 +(*test/../Knowledge/polyeq.sml:
13.109 + Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
13.110 +(*test/../Interpret/ptyps.sml:
13.111 + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
13.112 +val thy = @{theory "Complex_Main"};
13.113 +
13.114 +"----- test 1: OK";
13.115 +val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
13.116 +tracing "paIsa=..."; atomty pa; tracing "...=paIsa";
13.117 +(***
13.118 +*** Const (op =, real => real => bool)
13.119 +*** . Var ((a, 0), real)
13.120 +*** . Const (Groups.zero_class.zero, real)
13.121 +***)
13.122 +"----- test 1a true";
13.123 +val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; (*<<<<<<<---------------*)
13.124 +if matches thy tm pa then ()
13.125 + else error "termC.sml diff.behav. in matches true 1";
13.126 +"----- test 1b false";
13.127 +val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*)
13.128 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"
13.129 + else ();
13.130 +
13.131 +"----- test 2: Nok";
13.132 +val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)
13.133 +tracing "paLo2=..."; atomty pa; tracing "...=paLo2";
13.134 +(***
13.135 +*** Const (op =, real => real => bool)
13.136 +*** . Var ((a, 0), real)
13.137 +*** . Var ((0, 0), real)
13.138 +***)
13.139 +"----- test 2a true";
13.140 +val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
13.141 +if matches thy tm pa then ()
13.142 + else error "termC.sml diff.behav. in matches true 2";
13.143 +"----- test 2b false";
13.144 +val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
13.145 +if matches thy tm pa then ()
13.146 + else error "termC.sml diff.behav. in matches false 2";
13.147 +(* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
13.148 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 2"
13.149 + else ();*)
13.150 +
13.151 +"----- test 3: OK";
13.152 +val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)
13.153 +tracing "paF2=..."; atomty pa; tracing "...=paF2";
13.154 +(***
13.155 +*** Const (op =, real => real => bool)
13.156 +*** . Var ((a, 0), real)
13.157 +*** . Free (0, real)
13.158 +***)
13.159 +"----- test 3a true";
13.160 +val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
13.161 +if matches thy tm pa then ()
13.162 + else error "termC.sml diff.behav. in matches true 3";
13.163 +"----- test 3b false";
13.164 +val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
13.165 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"
13.166 + else ();
13.167 +
13.168 +"----- test 4=3 with specific data";
13.169 +val pa = free2var (str2term "M_b 0");
13.170 +"----- test 4a true";
13.171 +val tm = str2term "M_b 0";
13.172 +if matches thy tm pa then ()
13.173 + else error "termC.sml diff.behav. in matches true 4";
13.174 +"----- test 4b false";
13.175 +val tm = str2term "M_b x";
13.176 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"
13.177 + else ();
13.178 +
13.179 +
13.180 +"------------parse---------------------------------------";
13.181 +"------------parse---------------------------------------";
13.182 +"------------parse---------------------------------------";
13.183 +Toplevel.debug := true;
13.184 +(* literal types:
13.185 +PolyML.addPrettyPrinter
13.186 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
13.187 +*)(* pretty types:
13.188 +PolyML.addPrettyPrinter
13.189 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
13.190 +print_depth 99;
13.191 +*)
13.192 +val thy = @{theory "Complex_Main"};
13.193 +val str = "x + z";
13.194 +parse thy str;
13.195 +"---------------";
13.196 +val str = "x + 2*z";
13.197 +val t = (Syntax.read_term_global thy str);
13.198 +val t = numbers_to_string (Syntax.read_term_global thy str);
13.199 +val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
13.200 +cterm_of thy t;
13.201 +val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
13.202 +
13.203 +(*Makarius.1003
13.204 +ML {* @{term "2::int"} *}
13.205 +
13.206 +term "(1.24444) :: real"
13.207 +
13.208 +ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
13.209 +*)
13.210 +
13.211 +
13.212 +"----------- uminus_to_string ---------------------------";
13.213 +"----------- uminus_to_string ---------------------------";
13.214 +"----------- uminus_to_string ---------------------------";
13.215 +val t1 = numbers_to_string @{term "-2::real"};
13.216 +val t2 = numbers_to_string @{term "- 2::real"};
13.217 +if uminus_to_string t2 = t1 then ()
13.218 +else error "termC.sml diff.behav. in uminus_to_string";
13.219 +
13.220 +
13.221 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.
13.222 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.*)
14.1 --- a/test/Tools/isac/Test_Isac.thy Mon Sep 27 13:35:06 2010 +0200
14.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Sep 28 07:28:10 2010 +0200
14.3 @@ -55,7 +55,7 @@
14.4 use"ProgLang/rewrite.sml"; (*part.*)
14.5 (*
14.6 use"scrtools.sml";
14.7 - use"term.sml";
14.8 + use"termC.sml";
14.9 use"tools.sml";
14.10 cd "../..";
14.11 cd"smltest/ME";