1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Jul 13 09:49:45 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Jul 13 10:43:21 2021 +0200
1.3 @@ -13,60 +13,14 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -\<close> text \<open>
1.8 -fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = dest_numeral' t
1.9 -(*
1.10 - | string_of_atom (t as Const ("Groups.one_class.one", _)) = HOLogic.dest_numeral t
1.11 - | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = HOLogic.dest_numeral t
1.12 - | string_of_atom (Const (str, _)) = str
1.13 - | string_of_atom (Free _) = true
1.14 - | string_of_atom (Var _) = true
1.15 - | string_of_atom _ = false;
1.16 -*)
1.17 +\<close> ML \<open> (**)
1.18 \<close> ML \<open>
1.19 +HOLogic.dest_number: term -> typ * int;
1.20 +HOLogic.dest_numeral: term -> int;
1.21 \<close> ML \<open>
1.22 +TermC.to_string: term -> string
1.23 \<close> ML \<open>
1.24 -\<close> ML \<open>
1.25 -\<close> ML \<open>
1.26 -\<close> ML \<open>
1.27 -@{term 3}(* = Const ("Num.numeral_class.numeral", _) $ *)
1.28 -\<close> ML \<open>
1.29 -fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =
1.30 - Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;
1.31 -\<close> ML \<open>
1.32 -mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term
1.33 -\<close> ML \<open>
1.34 -\<close> ML \<open>
1.35 -(* this function only accepts the most simple monoms vvvvvvvvvv *)
1.36 -fun ist_monom (Free _) = true (* 2, a *)
1.37 - | ist_monom (Const ("Groups.times_class.times", _) $
1.38 - (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true
1.39 - | ist_monom (Const ("Groups.times_class.times", _) $ (* 2*a, a*b *)
1.40 - Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false
1.41 - | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.42 - (Const ("Groups.times_class.times", _) $
1.43 - (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true
1.44 - | ist_monom (Const ("Transcendental.powr", _) $ (* a^2 *)
1.45 - Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true
1.46 - | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a^2 *)
1.47 - (Const ("Num.numeral_class.numeral", _) $ _) $
1.48 - (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true
1.49 - | ist_monom _ = false;
1.50 -\<close> ML \<open>
1.51 -fun varids (Const ("Num.numeral_class.numeral", _) $ _) = []
1.52 - | varids (Const (s, Type (_,[]))) = [strip_thy s]
1.53 - | varids (Free (s, Type (_,[]))) = [strip_thy s]
1.54 - | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
1.55 -(*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
1.56 - | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
1.57 - | varids (Abs (a, _, t)) = union op = [a] (varids t)
1.58 - | varids (t1 $ t2) = union op = (varids t1) (varids t2)
1.59 - | varids _ = [];
1.60 -\<close> ML \<open>
1.61 -\<close> ML \<open>
1.62 -\<close> ML \<open>
1.63 -\<close> ML \<open>
1.64 -\<close> ML \<open>
1.65 +TermC.to_string
1.66 \<close> ML \<open>
1.67 \<close> ML \<open>
1.68 \<close> ML \<open>
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue Jul 13 09:49:45 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jul 13 10:43:21 2021 +0200
2.3 @@ -29,6 +29,7 @@
2.4 val mk_frac: typ -> int * (int * int) -> term
2.5 val term_of_num: typ -> int -> term
2.6 val num_of_term: term -> int
2.7 + val to_string: term -> string
2.8 val int_of_str: string -> int
2.9 val isastr_of_int: int -> string
2.10 val int_opt_of_string: string -> int option
2.11 @@ -38,6 +39,7 @@
2.12 val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *)
2.13
2.14 val is_atom: term -> bool
2.15 + val string_of_atom: term -> string
2.16 val is_const: term -> bool
2.17 val is_variable: term -> bool
2.18 val is_bdv: string -> bool
2.19 @@ -273,6 +275,8 @@
2.20
2.21 val term_of_num = HOLogic.mk_number;
2.22 fun num_of_term t = t |> HOLogic.dest_number |> snd;
2.23 +(* accomodate string-representation for int to term-orders in Poly.thy and Rational.thy*)
2.24 +fun to_string t = t |> num_of_term |> LibraryC.string_of_int'
2.25
2.26 fun is_const (Const _) = true | is_const _ = false;
2.27 fun is_variable (t as Free _) = not (is_num t)
2.28 @@ -558,6 +562,13 @@
2.29 | is_atom (Free _) = true
2.30 | is_atom (Var _) = true
2.31 | is_atom _ = false;
2.32 +fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = to_string t
2.33 + | string_of_atom (t as Const ("Groups.one_class.one", _)) = to_string t
2.34 + | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = to_string t
2.35 + | string_of_atom (Const (str, _)) = str
2.36 + | string_of_atom (Free (str, _)) = str
2.37 + | string_of_atom (Var ((str, int), _)) = str ^ "_" ^ string_of_int int
2.38 + | string_of_atom _ = "DUMMY-string_of_atom";
2.39
2.40 (* from Pure/term.ML; reports if ALL Free's have found a substitution
2.41 (required for evaluating the preconditions of _incomplete_ models) *)
3.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Jul 13 09:49:45 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jul 13 10:43:21 2021 +0200
3.3 @@ -277,21 +277,18 @@
3.4 (monom2list t1) @ (monom2list t2)
3.5 | monom2list t = [t];
3.6
3.7 -(* use this fun ONLY locally: makes negative numbers with "-" instead of "~" for poly-orders*)
3.8 -fun dest_number' t = t |> TermC.num_of_term |> LibraryC.string_of_int'
3.9 -
3.10 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
3.11 fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str
3.12 - | get_basStr (Const ("Transcendental.powr",_) $ n $ _) = dest_number' n
3.13 + | get_basStr (Const ("Transcendental.powr",_) $ n $ _) = TermC.to_string n
3.14 | get_basStr (Free (str, _)) = str
3.15 | get_basStr t =
3.16 - if TermC.is_num t then dest_number' t
3.17 + if TermC.is_num t then TermC.to_string t
3.18 else "|||"; (* gross gewichtet; für Brüche ect. *)
3.19
3.20 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
3.21 fun get_potStr (Const ("Transcendental.powr", _) $ Free _ $ Free (str, _)) = str
3.22 | get_potStr (Const ("Transcendental.powr", _) $ Free _ $ t) =
3.23 - if TermC.is_num t then dest_number' t else "|||"
3.24 + if TermC.is_num t then TermC.to_string t else "|||"
3.25 | get_potStr (Free _) = "---" (* keine Hochzahl --> kleinst gewichtet *)
3.26 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
3.27
4.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Jul 13 09:49:45 2021 +0200
4.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Jul 13 10:43:21 2021 +0200
4.3 @@ -281,9 +281,9 @@
4.4 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
4.5 fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ =
4.6 if TermC.is_atom arg
4.7 - then SOME (TermC.mk_thmid thmid "" "",
4.8 + then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
4.9 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
4.10 - else SOME (TermC.mk_thmid thmid "" "",
4.11 + else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
4.12 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
4.13 | eval_is_atom _ _ _ _ = NONE;
4.14
5.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Tue Jul 13 09:49:45 2021 +0200
5.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue Jul 13 10:43:21 2021 +0200
5.3 @@ -6,7 +6,6 @@
5.4 "-----------------------------------------------------------------------------------------------";
5.5 "table of contents -----------------------------------------------------------------------------";
5.6 "-----------------------------------------------------------------------------------------------";
5.7 -"----------- fun is_atom -----------------------------------------------------------------------";
5.8 "----------- numerals in Isabelle2011/12/13 -------------";
5.9 "----------- inst_bdv -----------------------------------";
5.10 "----------- subst_atomic_all ---------------------------";
5.11 @@ -36,10 +35,6 @@
5.12 "--------------------------------------------------------";
5.13 "--------------------------------------------------------";
5.14
5.15 -"----------- fun is_atom -----------------------------------------------------------------------";
5.16 -"----------- fun is_atom -----------------------------------------------------------------------";
5.17 -"----------- fun is_atom -----------------------------------------------------------------------";
5.18 -
5.19 "----------- numerals in Isabelle2011/12/13 -------------";
5.20 "----------- numerals in Isabelle2011/12/13 -------------";
5.21 "----------- numerals in Isabelle2011/12/13 -------------";
6.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Tue Jul 13 09:49:45 2021 +0200
6.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Tue Jul 13 10:43:21 2021 +0200
6.3 @@ -7,6 +7,7 @@
6.4 "-----------------------------------------------------------------------------------------------";
6.5 "table of contents -----------------------------------------------------------------------------";
6.6 "-----------------------------------------------------------------------------------------------";
6.7 +"-------- fun eval_is_atom ---------------------------------------------------------------------";
6.8 "-------- fun eval_is_even ---------------------------------------------------------------------";
6.9 "-------- fun eval_const -----------------------------------------------------------------------";
6.10 "-------- fun eval_cancel ----------------------------------------------------------------------";
6.11 @@ -26,6 +27,34 @@
6.12 "-----------------------------------------------------------------------------------------------";
6.13
6.14
6.15 +"-------- fun eval_is_atom ---------------------------------------------------------------------";
6.16 +"-------- fun eval_is_atom ---------------------------------------------------------------------";
6.17 +"-------- fun eval_is_atom ---------------------------------------------------------------------";
6.18 +if is_atom @{term 0} then () else error "is_atom 0 CHANGED";
6.19 +val eval_t = @{term "0 is_atom"};
6.20 +case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
6.21 + SOME ("#is_atom_0_", _) => ()
6.22 +| _ => error "eval_is_atom 0 CHANGED";
6.23 +
6.24 +if is_atom @{term 1} then () else error "is_atom 1 CHANGED";
6.25 +val eval_t = @{term "1 is_atom"};
6.26 +case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
6.27 + SOME ("#is_atom_1_", _) => ()
6.28 +| _ => error "eval_is_atom 1 CHANGED";
6.29 +
6.30 +if is_atom @{term 123} then () else error "is_atom 123 CHANGED";
6.31 +val eval_t = @{term "123 is_atom"};
6.32 +case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
6.33 + SOME ("#is_atom_123_", _) => ()
6.34 +| _ => error "eval_is_atom 123 CHANGED";
6.35 +
6.36 +if is_atom @{term abc} then () else error "is_atom abc CHANGED";
6.37 +val eval_t = @{term "abc is_atom"};
6.38 +case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
6.39 + SOME ("#is_atom_abc_", _) => ()
6.40 +| _ => error "eval_is_atom abc CHANGED";
6.41 +
6.42 +
6.43 "-------- fun eval_is_even ---------------------------------------------------------------------";
6.44 "-------- fun eval_is_even ---------------------------------------------------------------------";
6.45 "-------- fun eval_is_even ---------------------------------------------------------------------";
7.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 13 09:49:45 2021 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 13 10:43:21 2021 +0200
7.3 @@ -208,7 +208,7 @@
7.4 else (i * ~1) |> string_of_int |> curry op ^ "-"
7.5 \<close> ML \<open>
7.6 (* use this fun ONLY locally: makes negative numbers with "-" instead of "~" for poly-orders*)
7.7 -fun dest_number' t = t |> TermC.num_of_term |> string_of_int'
7.8 +fun to_string t = t |> TermC.num_of_term |> string_of_int'
7.9 \<close> ML \<open>
7.10 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
7.11 \<close> ML \<open> (* orig.code *)
7.12 @@ -219,10 +219,10 @@
7.13 raise ERROR("get_basStr: called with t= "^(UnparseC.term t));*)
7.14 \<close> ML \<open> (* \<longrightarrow> Poly.thy *)
7.15 fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str
7.16 - | get_basStr (Const ("Transcendental.powr",_) $ n $ _) = dest_number' n
7.17 + | get_basStr (Const ("Transcendental.powr",_) $ n $ _) = TermC.to_string n
7.18 | get_basStr (Free (str, _)) = str
7.19 | get_basStr t =
7.20 - if TermC.is_num t then dest_number' t
7.21 + if TermC.is_num t then TermC.to_string t
7.22 else "|||"; (* gross gewichtet; für Brüche ect. *)
7.23 \<close> ML \<open>
7.24
7.25 @@ -237,7 +237,7 @@
7.26 \<close> ML \<open> (* \<longrightarrow> Poly.thy *)
7.27 fun get_potStr (Const ("Transcendental.powr", _) $ Free _ $ Free (str, _)) = str
7.28 | get_potStr (Const ("Transcendental.powr", _) $ Free _ $ t) =
7.29 - if TermC.is_num t then dest_number' t else "|||"
7.30 + if TermC.is_num t then TermC.to_string t else "|||"
7.31 | get_potStr (Free _) = "---" (* keine Hochzahl --> kleinst gewichtet *)
7.32 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
7.33
7.34 @@ -1125,59 +1125,6 @@
7.35 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
7.36 then () else error "poly_of_term uminus changed";
7.37
7.38 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
7.39 -\<close> ML \<open>
7.40 -val t = TermC.str2term "x/2 - -(3*x - 2)/9";
7.41 -\<close> ML \<open>
7.42 -val NONE = poly_of_term vs t; (*COMPARE norm_Rational: exception TERM dest_number - 3 + 13 * x
7.43 - BUT: this raises no exn ! ! !*)
7.44 -\<close> ML \<open>
7.45 -Rewrite.trace_on := false;
7.46 -\<close> text \<open>
7.47 -Rewrite.trace_on := true;
7.48 -\<close> ML \<open> (*norm_Rational: exception TERM raised dest_number - 2 + 3 * x*)
7.49 -val SOME (t', _) = rewrite_set_ thy false norm_Rational t;
7.50 -\<close> ML \<open>
7.51 -@{thm real_mult_minus1}
7.52 -\<close> ML \<open>
7.53 -
7.54 -@{term 0};
7.55 -\<close> ML \<open>
7.56 -"----------- fun is_atom -----------------------------------------------------------------------";
7.57 -"----------- fun is_atom -----------------------------------------------------------------------";
7.58 -"----------- fun is_atom -----------------------------------------------------------------------";
7.59 -\<close> ML \<open>
7.60 -\<close> ML \<open>
7.61 -if is_atom @{term 0} then () else error "is_atom 1 CHANGED";
7.62 -val eval_t = @{term "1 is_atom"};
7.63 -case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
7.64 - SOME ("#is_atom__", _) => ()
7.65 -| _ => error "eval_is_atom 1 CHANGED";
7.66 -\<close> ML \<open>
7.67 -Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t ()
7.68 -\<close> ML \<open>
7.69 -\<close> ML \<open>
7.70 -\<close> ML \<open>
7.71 -if is_atom @{term 1} then () else error "is_atom 1 CHANGED";
7.72 -val eval_t = @{term "1 is_atom"};
7.73 -case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
7.74 - SOME ("#is_atom__", _) => ()
7.75 -| _ => error "eval_is_atom 1 CHANGED";
7.76 -\<close> ML \<open>
7.77 -Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t ()
7.78 -\<close> ML \<open>
7.79 -\<close> ML \<open>
7.80 -\<close> ML \<open>
7.81 -val eval_t = @{term "0 is_atom"};
7.82 -\<close> text \<open>
7.83 -string_of_atom
7.84 -\<close> ML \<open>
7.85 -\<close> ML \<open>
7.86 -\<close> ML \<open>
7.87 -\<close> ML \<open>
7.88 -\<close> ML \<open>
7.89 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
7.90 -
7.91 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
7.92 then () else error "poly_of_term 1 changed";
7.93