607 > const_in "sqrt" t; |
607 > const_in "sqrt" t; |
608 val it = false : bool |
608 val it = false : bool |
609 *) |
609 *) |
610 |
610 |
611 (*used for calculating built in binary operations in Isabelle2002->Float.ML*) |
611 (*used for calculating built in binary operations in Isabelle2002->Float.ML*) |
612 (*fun calc "op +" (n1, n2) = n1+n2 |
612 (*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2 |
613 | calc "op -" (n1, n2) = n1-n2 |
613 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2 |
614 | calc "op *" (n1, n2) = n1*n2 |
614 | calc "op *" (n1, n2) = n1*n2 |
615 | calc "HOL.divide"(n1, n2) = n1 div n2 |
615 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2 |
616 | calc "Atools.pow"(n1, n2) = power n1 n2 |
616 | calc "Atools.pow"(n1, n2) = power n1 n2 |
617 | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*) |
617 | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*) |
618 fun calc_equ "op <" (n1, n2) = n1 < n2 |
618 fun calc_equ "op <" (n1, n2) = n1 < n2 |
619 | calc_equ "op <=" (n1, n2) = n1 <= n2 |
619 | calc_equ "op <=" (n1, n2) = n1 <= n2 |
620 | calc_equ op_ _ = |
620 | calc_equ op_ _ = |
1161 (*WN050829 caution: is_atom (str2term"q_0/2 * L * x") = true !!! |
1161 (*WN050829 caution: is_atom (str2term"q_0/2 * L * x") = true !!! |
1162 use length (vars term) = 1 instead*) |
1162 use length (vars term) = 1 instead*) |
1163 fun is_atom (Const ("Float.Float",_) $ _) = true |
1163 fun is_atom (Const ("Float.Float",_) $ _) = true |
1164 | is_atom (Const ("ComplexI.I'_'_",_)) = true |
1164 | is_atom (Const ("ComplexI.I'_'_",_)) = true |
1165 | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t |
1165 | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t |
1166 | is_atom (Const ("op +",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1 |
1166 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1 |
1167 | is_atom (Const ("op +",_) $ t1 $ |
1167 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ |
1168 (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = |
1168 (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = |
1169 is_atom t1 andalso is_atom t2 |
1169 is_atom t1 andalso is_atom t2 |
1170 | is_atom (Const _) = true |
1170 | is_atom (Const _) = true |
1171 | is_atom (Free _) = true |
1171 | is_atom (Free _) = true |
1172 | is_atom (Var _) = true |
1172 | is_atom (Var _) = true |
1183 val it = true : bool |
1183 val it = true : bool |
1184 > val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__"; |
1184 > val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__"; |
1185 > is_atom t; |
1185 > is_atom t; |
1186 val it = true : bool |
1186 val it = true : bool |
1187 > val t = str2term "1 + 2*I__"; |
1187 > val t = str2term "1 + 2*I__"; |
1188 > val Const ("op +",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t; |
1188 > val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t; |
1189 *) |
1189 *) |
1190 |
1190 |
1191 (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's |
1191 (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's |
1192 have found a substitution (required for evaluating the preconditions |
1192 have found a substitution (required for evaluating the preconditions |
1193 of _incomplete_ models).*) |
1193 of _incomplete_ models).*) |
1212 (*.add two terms with a type given.*) |
1212 (*.add two terms with a type given.*) |
1213 fun mk_add t1 t2 = |
1213 fun mk_add t1 t2 = |
1214 let val T1 = type_of t1 |
1214 let val T1 = type_of t1 |
1215 val T2 = type_of t2 |
1215 val T2 = type_of t2 |
1216 in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2]) |
1216 in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2]) |
1217 else (Const ("op +", [T1, T2] ---> T1) $ t1 $ t2) |
1217 else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2) |
1218 end; |
1218 end; |
1219 |
1219 |