1.1 --- a/TODO.md Fri May 07 18:12:51 2021 +0200
1.2 +++ b/TODO.md Tue Jun 01 15:41:23 2021 +0200
1.3 @@ -29,11 +29,16 @@
1.4 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.5 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.6
1.7 -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
1.8 - - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
1.9 +* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation, DONE partially;
1.10 + - TODO: ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
1.11 + - TODO: clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
1.12
1.13 -* WN: Part.DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
1.14 +* WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
1.15 Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
1.16 Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
1.17
1.18 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
1.19 + ???
1.20 +
1.21 +* WN: reduce the number of TermC.parse*;
1.22 + - one or two variants should suffice.
2.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Fri May 07 18:12:51 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Jun 01 15:41:23 2021 +0200
2.3 @@ -14,5 +14,54 @@
2.4 ML \<open>
2.5 \<close> ML \<open>
2.6 \<close> ML \<open>
2.7 +\<close> ML \<open>
2.8 +\<close> ML \<open>
2.9 +\<close> ML \<open>
2.10 +\<close> ML \<open>
2.11 +\<close> ML \<open>
2.12 +\<close> ML \<open>
2.13 +@{term 3}(* = Const ("Num.numeral_class.numeral", _) $ *)
2.14 +\<close> ML \<open>
2.15 +fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =
2.16 + Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;
2.17 +\<close> ML \<open>
2.18 +mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term
2.19 +\<close> ML \<open>
2.20 +\<close> ML \<open>
2.21 +(* this function only accepts the most simple monoms vvvvvvvvvv *)
2.22 +fun ist_monom (Free _) = true (* 2, a *)
2.23 + | ist_monom (Const ("Groups.times_class.times", _) $
2.24 + (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true
2.25 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 2*a, a*b *)
2.26 + Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false
2.27 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
2.28 + (Const ("Groups.times_class.times", _) $
2.29 + (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true
2.30 + | ist_monom (Const ("Transcendental.powr", _) $ (* a^2 *)
2.31 + Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true
2.32 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a^2 *)
2.33 + (Const ("Num.numeral_class.numeral", _) $ _) $
2.34 + (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true
2.35 + | ist_monom _ = false;
2.36 +\<close> ML \<open>
2.37 +fun varids (Const ("Num.numeral_class.numeral", _) $ _) = []
2.38 + | varids (Const (s, Type (_,[]))) = [strip_thy s]
2.39 + | varids (Free (s, Type (_,[]))) = [strip_thy s]
2.40 + | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
2.41 +(*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
2.42 + | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
2.43 + | varids (Abs (a, _, t)) = union op = [a] (varids t)
2.44 + | varids (t1 $ t2) = union op = (varids t1) (varids t2)
2.45 + | varids _ = [];
2.46 +\<close> ML \<open>
2.47 +\<close> ML \<open>
2.48 +\<close> ML \<open>
2.49 +\<close> ML \<open>
2.50 +\<close> ML \<open>
2.51 +\<close> ML \<open>
2.52 +\<close> ML \<open>
2.53 +\<close> ML \<open>
2.54 +\<close> ML \<open>
2.55 +\<close> ML \<open>
2.56 \<close>
2.57 end
2.58 \ No newline at end of file
3.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Fri May 07 18:12:51 2021 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jun 01 15:41:23 2021 +0200
3.3 @@ -26,11 +26,12 @@
3.4 val inst_abs: term -> term
3.5 val inst_bdv: (term * term) list -> term -> term
3.6
3.7 + val mk_frac: typ -> int * (int * int) -> term
3.8 val term_of_num: typ -> int -> term
3.9 val num_of_term: term -> int
3.10 val int_of_str: string -> int
3.11 val isastr_of_int: int -> string
3.12 - val int_opt_of_string: string -> int option (* belongs to TermC *)
3.13 + val int_opt_of_string: string -> int option
3.14
3.15 val isalist2list: term -> term list
3.16 val list2isalist: typ -> term list -> term
3.17 @@ -50,6 +51,7 @@
3.18 val dest_listT: typ -> typ
3.19 val is_num: term -> bool
3.20 val is_num': string -> bool
3.21 + val string_of_num: term -> string
3.22 val variable_constant_pair: term * term -> bool
3.23
3.24 val mk_add: term -> term -> term
3.25 @@ -88,13 +90,14 @@
3.26 val uminus_to_string: term -> term
3.27
3.28 val var2free: term -> term
3.29 - val vars: term -> term list (* recognises numerals, should replace "fun vars_of" *)
3.30 + val vars: term -> term list (* recognises numerals, should replace "fun vars_of" TODOO*)
3.31 val vars': term list -> term list
3.32 - val vars_of: term -> term list (* deprecated *)
3.33 + val vars_of: term -> term list (* deprecated TODOO: see differences in test/../termC.sml*)
3.34 val dest_list': term -> term list
3.35 val negates: term -> term -> bool
3.36
3.37 \<^isac_test>\<open>
3.38 + val mk_negative: typ -> term -> term
3.39 val scala_of_term: term -> string
3.40 val atomtyp(*<-- atom_typ TODO*): typ -> unit
3.41 val atomty: term -> unit
3.42 @@ -243,15 +246,33 @@
3.43 if n < 0 then "-" ^ ((string_of_int o abs) n)
3.44 else string_of_int n;
3.45 val int_of_str = Value.parse_int;
3.46 +val int_opt_of_string = ThmC_Def.int_opt_of_string
3.47 +fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
3.48
3.49 -val int_opt_of_string = ThmC_Def.int_opt_of_string
3.50 +fun is_num (Const ("Num.numeral_class.numeral", _) $ _) = true
3.51 + | is_num (Const ("Groups.uminus_class.uminus", _) $
3.52 + (Const ("Num.numeral_class.numeral", _) $ _)) = true
3.53 + | is_num (Const ("Groups.one_class.one", _)) = true
3.54 + | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) = true
3.55 + | is_num (Const ("Groups.zero_class.zero", _)) = true
3.56 + | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.zero_class.zero", _)) = true
3.57 + | is_num _ = false;
3.58
3.59 -fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
3.60 -fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false;
3.61 -fun term_of_num ntyp n = Free (str_of_int n, ntyp);
3.62 -fun num_of_term (t as (Free (istr, _))) =
3.63 - (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
3.64 - | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
3.65 +fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
3.66 +
3.67 +fun mk_negative T t = Const ("Groups.uminus_class.uminus", T --> T) $ t
3.68 +fun mk_frac T (sg, (i1, i2)) =
3.69 + if sg = 1 then
3.70 + if i2 = 1 then HOLogic.mk_number T i1
3.71 + else Const ("Rings.divide_class.divide", T --> T --> T) $
3.72 + HOLogic.mk_number T i1 $ HOLogic.mk_number T i2
3.73 + else (*take negative*)
3.74 + if i2 = 1 then mk_negative T (HOLogic.mk_number T i1)
3.75 + else Const ("Rings.divide_class.divide", T --> T --> T) $
3.76 + mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2
3.77 +
3.78 +val term_of_num = HOLogic.mk_number;
3.79 +fun num_of_term t = t |> HOLogic.dest_number |> snd;
3.80
3.81 fun is_const (Const _) = true | is_const _ = false;
3.82 fun is_variable (t as Free _) = not (is_num t)
3.83 @@ -272,7 +293,7 @@
3.84 fun vars t =
3.85 let
3.86 fun scan vs (Const _) = vs
3.87 - | scan vs (t as Free (s, _)) = if is_num' s then vs else t :: vs
3.88 + | scan vs (t as Free _) = (*if is_num' s then vs else*) t :: vs
3.89 | scan vs (t as Var _) = t :: vs
3.90 | scan vs (Bound _) = vs
3.91 | scan vs (Abs (_, _, t)) = scan vs t
3.92 @@ -435,10 +456,10 @@
3.93 fun mk_factroot op_(*=thy.sqrt*) T fact root =
3.94 Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $
3.95 (Const (op_, T --> T) $ term_of_num T root);
3.96 -fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ Free (str_of_int n, ntyp);
3.97 -fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ Free (str_of_int n, ntyp) $ v;
3.98 +fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ HOLogic.mk_number ntyp n;
3.99 +fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ HOLogic.mk_number ntyp n $ v;
3.100 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =
3.101 - Const (op_, Top) $ Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
3.102 + Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;
3.103 fun mk_thmid thmid n1 n2 =
3.104 thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
3.105 fun mk_add t1 t2 =
3.106 @@ -526,7 +547,7 @@
3.107 fun parse_patt thy str = (thy, str)
3.108 |>> ThyC.to_ctxt
3.109 |-> Proof_Context.read_term_pattern
3.110 - |> numbers_to_string (*TODO drop*)
3.111 +(*|> numbers_to_string TODO drop*)
3.112 |> typ_a2real; (*TODO drop*)
3.113 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
3.114
3.115 @@ -571,7 +592,9 @@
3.116 val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
3.117 ["Groups.plus_class.plus", "Groups.minus_class.minus",
3.118 "Rings.divide_class.divide", "Groups.times_class.times",
3.119 - "Transcendental.powr"];
3.120 + "Transcendental.powr",
3.121 + "Num.numeral_class.numeral", "Num.num.Bit0", "Num.num.Bit1", "Num.num.One",
3.122 + "Groups.uminus_class.uminus", "Groups.one_class.one"];
3.123 (* treat Free, Const, Var as variables in polynomials *)
3.124 fun vars_of t =
3.125 let
3.126 @@ -614,4 +637,4 @@
3.127 in trm' end
3.128
3.129
3.130 -end
3.131 \ No newline at end of file
3.132 +end
4.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Fri May 07 18:12:51 2021 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Tue Jun 01 15:41:23 2021 +0200
4.3 @@ -50,7 +50,8 @@
4.4
4.5 (** transform Isabelle's binary numerals to "Free (string, T)" **)
4.6
4.7 -val num_to_Free = (* Makarius 100308 *)
4.8 +val num_to_Free = (**)I(* Makarius 100308 *)
4.9 +(** )
4.10 let
4.11 fun dest_num t =
4.12 (case try HOLogic.dest_number t of
4.13 @@ -61,8 +62,10 @@
4.14 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
4.15 | to_str t = perhaps dest_num t;
4.16 in to_str end
4.17 +( **)
4.18
4.19 -val uminus_to_string =
4.20 +val uminus_to_string = (**)I
4.21 +(** )
4.22 let
4.23 fun dest_num t =
4.24 case t of
4.25 @@ -76,8 +79,10 @@
4.26 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
4.27 | to_str t = perhaps dest_num t;
4.28 in to_str end;
4.29 +( **)
4.30
4.31 -fun numerals_to_Free thm =
4.32 +fun numerals_to_Free thm = (**)thm
4.33 +(** )
4.34 let
4.35 val prop = Thm.plain_prop_of thm
4.36 val prop' = num_to_Free prop;
4.37 @@ -87,5 +92,6 @@
4.38 Skip_Proof.make_thm (Thm.theory_of_thm thm) prop'
4.39 |> Thm.put_name_hint (Thm.get_name_hint thm)
4.40 end;
4.41 +( **)
4.42
4.43 (**)end(**)
5.1 --- a/src/Tools/isac/Build_Isac.thy Fri May 07 18:12:51 2021 +0200
5.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Jun 01 15:41:23 2021 +0200
5.3 @@ -41,27 +41,23 @@
5.4 ML_file contextC.sml
5.5 ML_file environment.sml
5.6 ( ** ) "BaseDefinitions/BaseDefinitions"( **)
5.7 -
5.8 -(* theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.9 - $ISABELLE_ISAC/ProgLang
5.10 +(*
5.11 + theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.12 + at $ISABELLE_ISAC/ProgLang
5.13 ML_file evaluate.sml
5.14 -
5.15 theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.16 - $ISABELLE_ISAC/ProgLang
5.17 - theory Prog_Expr imports Calculate ListC
5.18 - $ISABELLE_ISAC/ProgLang
5.19 theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.20 - theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.21 + theory Prog_Expr imports Calculate ListC Program
5.22 + theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.23 theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.24 - theory Auto_Prog imports Program Prog_Tac Tactical begin
5.25 - $ISABELLE_ISAC/ProgLang
5.26 + theory Auto_Prog imports Prog_Tac Tactical
5.27 theory ProgLang imports Prog_Expr Auto_Prog
5.28 - $ISABELLE_ISAC/ProgLang
5.29 + at $ISABELLE_ISAC/ProgLang
5.30 ( ** ) "ProgLang/ProgLang"( **)
5.31 (*
5.32 theory MathEngBasic imports
5.33 "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
5.34 - $ISABELLE_ISAC/MathEngBasic
5.35 + at $ISABELLE_ISAC/MathEngBasic
5.36 ML_file thmC.sml
5.37 ML_file problem.sml
5.38 ML_file method.sml
6.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri May 07 18:12:51 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jun 01 15:41:23 2021 +0200
6.3 @@ -186,15 +186,17 @@
6.4 subsubsection \<open>for predicates in specifications (ML)\<close>
6.5 ML \<open>
6.6 (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)
6.7 -(*. a 'monomial t in variable v' is a term t with
6.8 +(*. a "monomial t in variable v" is a term t with
6.9 either (1) v NOT existent in t, or (2) v contained in t,
6.10 if (1) then degree 0
6.11 - if (2) then v is a factor on the very right, ev. with exponent.*)
6.12 + if (2) then v is a factor on the very right, casually with exponent.*)
6.13 fun factor_right_deg (*case 2*)
6.14 - (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Transcendental.powr",_) $ vv $ Free (d, _))) v =
6.15 - if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (TermC.int_of_str d) else NONE
6.16 - | factor_right_deg (Const ("Transcendental.powr",_) $ vv $ Free (d,_)) v =
6.17 - if (vv = v) then SOME (TermC.int_of_str d) else NONE
6.18 + (Const ("Groups.times_class.times", _) $
6.19 + t1 $ (Const ("Transcendental.powr",_) $ vv $ num)) v =
6.20 + if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (snd (HOLogic.dest_number num))
6.21 + else NONE
6.22 + | factor_right_deg (Const ("Transcendental.powr",_) $ vv $ num) v =
6.23 + if (vv = v) then SOME (snd (HOLogic.dest_number num)) else NONE
6.24 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =
6.25 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
6.26 | factor_right_deg vv v =
6.27 @@ -269,17 +271,17 @@
6.28 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
6.29 fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str
6.30 | get_basStr (Free (str, _)) = str
6.31 + | get_basStr (Const ("Num.numeral_class.numeral", _) $ _) = "123"
6.32 | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
6.33 -(*| get_basStr t =
6.34 - raise ERROR("get_basStr: called with t= "^(UnparseC.term t));*)
6.35
6.36 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
6.37 -fun get_potStr (Const ("Transcendental.powr",_) $ Free _ $ Free (str, _)) = str
6.38 - | get_potStr (Const ("Transcendental.powr",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
6.39 +fun get_potStr (Const ("Transcendental.powr",_) $ Free _ $ t) =
6.40 + (case t of
6.41 + Free (str, _) => str
6.42 + | t =>
6.43 + if TermC.is_num t then "123" else "|||" (* gross gewichtet *))
6.44 | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
6.45 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
6.46 -(*| get_potStr t =
6.47 - raise ERROR("get_potStr: called with t= "^(UnparseC.term t));*)
6.48
6.49 (* Umgekehrte string_ord *)
6.50 val string_ord_rev = rev_order o string_ord;
6.51 @@ -312,12 +314,7 @@
6.52
6.53 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
6.54 (keine Variablen) enthaelt *)
6.55 -fun filter_num [] = true
6.56 - | filter_num [Free x] = if (TermC.is_num (Free x)) then true
6.57 - else false
6.58 - | filter_num ((Free _)::_) = false
6.59 - | filter_num ts =
6.60 - (filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;
6.61 +fun filter_num ts = fold (curry and_) (map TermC.is_num ts) true
6.62
6.63 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
6.64 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
6.65 @@ -325,23 +322,19 @@
6.66
6.67 (* Berechnet den Gesamtgrad eines Monoms *)
6.68 local
6.69 - fun counter (n, []) = n
6.70 - | counter (n, x :: xs) =
6.71 - if (is_nums x) then
6.72 - counter (n, xs)
6.73 - else
6.74 - (case x of
6.75 - (Const ("Transcendental.powr", _) $ Free _ $ Free (str_h, T)) =>
6.76 - if (is_nums (Free (str_h, T))) then
6.77 - counter (n + (the (TermC.int_opt_of_string str_h)), xs)
6.78 - else counter (n + 1000, xs) (*FIXME.MG?!*)
6.79 - | (Const ("Transcendental.powr", _) $ Free _ $ _ ) =>
6.80 - counter (n + 1000, xs) (*FIXME.MG?!*)
6.81 - | (Free _) => counter (n + 1, xs)
6.82 - (*| _ => raise ERROR("monom_degree: called with factor: "^(UnparseC.term x)))*)
6.83 - | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
6.84 + fun counter (n, []) = n
6.85 + | counter (n, x :: xs) =
6.86 + if (is_nums x) then counter (n, xs)
6.87 + else
6.88 + (case x of
6.89 + (Const ("Transcendental.powr", _) $ Free _ $ Const ("Num.numeral_class.numeral", _) $ num) =>
6.90 + counter (n + HOLogic.dest_numeral num, xs)
6.91 + | (Const ("Transcendental.powr", _) $ Free _ $ _ ) => counter (n + 1000, xs) (*FIXME.MG?!*)
6.92 + | (Free _) => counter (n + 1, xs)
6.93 + (*| _ => raise ERROR("monom_degree: called with factor: "^(UnparseC.term x)))*)
6.94 + | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
6.95 in
6.96 - fun monom_degree l = counter (0, l)
6.97 + fun monom_degree l = counter (0, l)
6.98 end;(*local*)
6.99
6.100 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
6.101 @@ -431,12 +424,12 @@
6.102
6.103 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
6.104 fun sort_variables t =
6.105 - let
6.106 - val ll = map monom2list (poly2list t);
6.107 - val lls = map sort_varList ll;
6.108 - val T = type_of t;
6.109 - val ls = map (create_monom T) lls;
6.110 - in create_polynom T ls end;
6.111 + let
6.112 + val ll = map monom2list (poly2list t);
6.113 + val lls = map sort_varList ll;
6.114 + val T = type_of t;
6.115 + val ls = map (create_monom T) lls;
6.116 + in create_polynom T ls end;
6.117
6.118 (* sorts the monoms of an expanded and variable-sorted polynomial
6.119 by total_degree *)
6.120 @@ -463,7 +456,7 @@
6.121 (case a of
6.122 "Transcendental.powr" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
6.123 | _ => (((a, 0), T), 0))
6.124 - | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
6.125 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
6.126 | dest_hd' (Var v) = (v, 2)
6.127 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
6.128 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
6.129 @@ -549,7 +542,7 @@
6.130 ((is_polyexp t1) andalso (is_polyexp t2))
6.131 | is_polyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
6.132 ((is_polyexp t1) andalso (is_polyexp t2))
6.133 - | is_polyexp _ = false;
6.134 + | is_polyexp num = TermC.is_num num;
6.135 \<close>
6.136
6.137 subsubsection \<open>for hard-coded AC rewriting\<close>
7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri May 07 18:12:51 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Jun 01 15:41:23 2021 +0200
7.3 @@ -1155,7 +1155,7 @@
7.4 | pr_ord GREATER = "GREATER";
7.5
7.6 fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
7.7 - | dest_hd' x (t as Free (a, T)) =
7.8 + | dest_hd' x (t as Free (a, T)) = (*TODOO handle this as numeral, too? see EqSystem.thy*)
7.9 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
7.10 else (((a, 0), T), 1)
7.11 | dest_hd' _ (Var v) = (v, 2)
7.12 @@ -1163,18 +1163,17 @@
7.13 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
7.14 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
7.15
7.16 -fun size_of_term' x (Const ("Transcendental.powr",_) $ Free (var,_) $ Free (pot,_)) =
7.17 +fun size_of_term' x (Const ("Transcendental.powr",_) $
7.18 + Free (var, _) $ Const ("Num.numeral_class.numeral", _) $ pot) =
7.19 (case x of (*WN*)
7.20 - (Free (xstr,_)) =>
7.21 - (if xstr = var then 1000*(the (TermC.int_opt_of_string pot)) else 3)
7.22 - | _ => raise ERROR ("size_of_term' called with subst = "^
7.23 - (UnparseC.term x)))
7.24 - | size_of_term' x (Free (subst,_)) =
7.25 + (Free (xstr, _)) =>
7.26 + (if xstr = var then 1000 * (HOLogic.dest_numeral pot) else 3)
7.27 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
7.28 + | size_of_term' x (Free (subst, _)) =
7.29 (case x of
7.30 - (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
7.31 - | _ => raise ERROR ("size_of_term' called with subst = "^
7.32 - (UnparseC.term x)))
7.33 - | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
7.34 + (Free (xstr, _)) => (if xstr = subst then 1000 else 1)
7.35 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
7.36 + | size_of_term' x (Abs (_, _, body)) = 1 + size_of_term' x body
7.37 | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
7.38 | size_of_term' _ _ = 1;
7.39
8.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri May 07 18:12:51 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jun 01 15:41:23 2021 +0200
8.3 @@ -157,24 +157,19 @@
8.4 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
8.5 | eval_kleiner _ _ _ _ = NONE;
8.6
8.7 -fun ist_monom (Free _) = true
8.8 - | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) =
8.9 - if TermC.is_num' num then true else false
8.10 - | ist_monom _ = false;
8.11 -(*. this function only accepts the most simple monoms vvvvvvvvvv .*)
8.12 -fun ist_monom (Free _) = true (* 2, a *)
8.13 - | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
8.14 - if TermC.is_num' id then false else true
8.15 +fun ist_monom (Free _) = true (* 2, a *)
8.16 + | ist_monom (Const ("Groups.times_class.times", _) $
8.17 + (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true
8.18 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 2*a, a*b *)
8.19 + Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false
8.20 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
8.21 - (Const ("Groups.times_class.times", _) $
8.22 - Free (num, _) $ Free _) $ Free (id, _)) =
8.23 - if TermC.is_num' num andalso not (TermC.is_num' id) then true else false
8.24 - | ist_monom (Const ("Transcendental.powr", _) $ Free _ $ Free _) =
8.25 - true (* a^2 *)
8.26 - | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
8.27 - (Const ("Transcendental.powr", _) $
8.28 - Free _ $ Free _)) =
8.29 - if TermC.is_num' num then true else false
8.30 + (Const ("Groups.times_class.times", _) $
8.31 + (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true
8.32 + | ist_monom (Const ("Transcendental.powr", _) $ (* a^2 *)
8.33 + Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true
8.34 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a^2 *)
8.35 + (Const ("Num.numeral_class.numeral", _) $ _) $
8.36 + (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true
8.37 | ist_monom _ = false;
8.38
8.39 (* is this a univariate monomial ? *)
9.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri May 07 18:12:51 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Jun 01 15:41:23 2021 +0200
9.3 @@ -123,12 +123,15 @@
9.4 ML \<open>
9.5 fun monom_of_term vs (c, es) (t as Const _) =
9.6 (c, list_update es (find_index (curry op = t) vs) 1)
9.7 - | monom_of_term vs (c, es) (t as Free (id, _)) =
9.8 - if TermC.is_num' id
9.9 - then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
9.10 + | monom_of_term vs (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
9.11 + if TermC.is_num t
9.12 + then (t |> HOLogic.dest_number |> snd |> string_of_int
9.13 + |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
9.14 else (c, list_update es (find_index (curry op = t) vs) 1)
9.15 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $ Free (e, _)) =
9.16 - (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
9.17 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $
9.18 + (t as (Const ("Num.numeral_class.numeral", _) $ _)) $
9.19 + (Const ("Num.numeral_class.numeral", _) $ num)) =
9.20 + (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
9.21 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
9.22 let val (c', es') = monom_of_term vs (c, es) m1
9.23 in monom_of_term vs (c', es') m2 end
9.24 @@ -179,7 +182,7 @@
9.25 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
9.26 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
9.27 | term_of_es baseT expT (v :: vs) (e :: es) =
9.28 - Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
9.29 + Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
9.30 :: term_of_es baseT expT vs es
9.31 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
9.32
9.33 @@ -189,9 +192,10 @@
9.34 if c = 1
9.35 then
9.36 if es' = [] (*if es = [0,0,0,...]*)
9.37 - then Free (TermC.isastr_of_int c, baseT)
9.38 + then HOLogic.mk_number baseT c
9.39 else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
9.40 - else foldl (HOLogic.mk_binop "Groups.times_class.times") (Free (TermC.isastr_of_int c, baseT), es')
9.41 + else foldl (HOLogic.mk_binop "Groups.times_class.times")
9.42 + (HOLogic.mk_number baseT c, es')
9.43 end
9.44
9.45 fun term_of_poly baseT expT vs p =
9.46 @@ -203,7 +207,7 @@
9.47 ML \<open>
9.48 fun mk_noteq_0 baseT t =
9.49 Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
9.50 - (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
9.51 + (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
9.52
9.53 fun mk_asms baseT ts =
9.54 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
9.55 @@ -311,12 +315,12 @@
9.56 (Const ("Groups.plus_class.plus", _) $
9.57 nofrac $
9.58 (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
9.59 - = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
9.60 + = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
9.61 | check_frac_sum
9.62 (Const ("Groups.plus_class.plus", _) $
9.63 (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
9.64 nofrac)
9.65 - = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
9.66 + = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
9.67 | check_frac_sum _ = NONE
9.68
9.69 (* prepare a term for addition by providing the least common denominator as a product
10.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri May 07 18:12:51 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Jun 01 15:41:23 2021 +0200
10.3 @@ -46,34 +46,30 @@
10.4
10.5 (*-------------------------functions---------------------*)
10.6 (*evaluation square-root over the integers*)
10.7 -fun eval_sqrt (_ : string) (_ : string) (t as
10.8 - (Const(op0, _) $ arg)) _(*thy*) =
10.9 +fun eval_sqrt (_ : string) (_ : string) (t as (Const (op0, _) $ arg)) _(*thy*) =
10.10 (case arg of
10.11 - Free (n1,t1) =>
10.12 - (case TermC.int_opt_of_string n1 of
10.13 - SOME ni =>
10.14 - if ni < 0 then NONE
10.15 - else
10.16 - let val fact = Eval.squfact ni;
10.17 - in if fact*fact = ni
10.18 - then SOME ("#sqrt #"^(string_of_int ni)^" = #"
10.19 - ^(string_of_int (if ni = 0 then 0
10.20 - else ni div fact)),
10.21 - HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num t1 fact))
10.22 - else if fact = 1 then NONE
10.23 - else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
10.24 - ^(string_of_int fact)^" * #"
10.25 - ^(string_of_int fact)^" * #"
10.26 - ^(string_of_int (ni div (fact*fact))^")"),
10.27 - HOLogic.Trueprop $
10.28 - (TermC.mk_equality
10.29 - (t,
10.30 - (TermC.mk_factroot op0 t1 fact
10.31 - (ni div (fact*fact))))))
10.32 - end
10.33 - | NONE => NONE)
10.34 - | _ => NONE)
10.35 -
10.36 + (Const ("Num.numeral_class.numeral", T) $ num) =>
10.37 + let val ni = HOLogic.dest_numeral num
10.38 + in
10.39 + if ni < 0 then NONE
10.40 + else
10.41 + let val fact = Eval.squfact ni;
10.42 + in
10.43 + if fact * fact = ni
10.44 + then
10.45 + SOME ("#sqrt #" ^ string_of_int ni ^ " = #"
10.46 + ^ string_of_int (if ni = 0 then 0 else ni div fact),
10.47 + HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num T fact))
10.48 + else if fact = 1 then NONE
10.49 + else
10.50 + SOME ("#sqrt #" ^ string_of_int ni ^ " = sqrt (#"
10.51 + ^ string_of_int fact ^ " * #" ^ string_of_int fact ^ " * #"
10.52 + ^ string_of_int (ni div (fact * fact)) ^ ")",
10.53 + HOLogic.Trueprop $ TermC.mk_equality
10.54 + (t, (TermC.mk_factroot op0 T fact (ni div (fact*fact)))))
10.55 + end
10.56 + end
10.57 + | _ => NONE)
10.58 | eval_sqrt _ _ _ _ = NONE;
10.59 (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0");
10.60 > eval_sqrt thmid op_ t thy;
10.61 @@ -96,7 +92,7 @@
10.62 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
10.63 (case a of "NthRoot.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
10.64 | _ => (((a, 0), T), 0))
10.65 - | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
10.66 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
10.67 | dest_hd' (Var v) = (v, 2)
10.68 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
10.69 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
11.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Fri May 07 18:12:51 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Tue Jun 01 15:41:23 2021 +0200
11.3 @@ -8,12 +8,7 @@
11.4 consts
11.5
11.6 (*descriptions in the related problem*)
11.7 - Term :: "real => una"
11.8 -(*TERM --> Const ("Pure.term", "RealDef.real => prop") (*!!!*) $
11.9 - Free ("ttt", "RealDef.real")
11.10 - term --> Free ("term", "RealDef.real => RealDef.real") $
11.11 - Free ("ttt", "RealDef.real")
11.12 - but 'term' is a keyword in *.thy*)
11.13 + Term :: "real => una" (*"term" is a keyword in *.thy*)
11.14 normalform :: "real => una"
11.15
11.16 (*the CAS-command*)
12.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri May 07 18:12:51 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Jun 01 15:41:23 2021 +0200
12.3 @@ -59,8 +59,9 @@
12.4 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
12.5 | atom _ = false;
12.6
12.7 -fun varids (Const (s, Type (_,[]))) = [strip_thy s]
12.8 - | varids (Free (s, Type (_,[]))) = if TermC.is_num' s then [] else [strip_thy s]
12.9 +fun varids (Const ("Num.numeral_class.numeral", _) $ _) = []
12.10 + | varids (Const (s, Type (_,[]))) = [strip_thy s]
12.11 + | varids (Free (s, Type (_,[]))) = [strip_thy s]
12.12 | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
12.13 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
12.14 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
12.15 @@ -297,7 +298,7 @@
12.16 (case a of
12.17 "Transcendental.powr" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
12.18 | _ => (((a, 0), T), 0))
12.19 - | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
12.20 + | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
12.21 | dest_hd' (Var v) = (v, 2)
12.22 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
12.23 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
13.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Fri May 07 18:12:51 2021 +0200
13.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Jun 01 15:41:23 2021 +0200
13.3 @@ -89,14 +89,19 @@
13.4 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
13.5 and rew_sub thy i bdv tless rls put_asm lrd r t =
13.6 (let
13.7 +(** )val _ = @{print}{a = "@ rew_sub: 1 < ?n \<Longrightarrow> NTH ?n..", r = UnparseC.term r};( *TODOO*)
13.8 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
13.9 +(** )val _ = @{print}{a = "@ rew_sub NO: patterns..", lhs = UnparseC.term lhs, rhs = UnparseC.term rhs};( *TODOO*)
13.10 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
13.11 handle Pattern.MATCH => raise NO_REWRITE
13.12 +(** )val _ = @{print}{a = "@ Envir.subst_term: OK gives (3 + - 1)", r' = UnparseC.term r'};( *TODOO*)
13.13 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
13.14 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
13.15 val _ = trace_in2 i "eval asms" thy r';
13.16 +(** )val _ = @{print}{a = "@ eval asms", r' = UnparseC.term r'};( *TODOO*)
13.17 val (t'', p'') = (*conditional rewriting*)
13.18 let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
13.19 +(** )val _ = @{print}{a = "@ eval__true asms", simpl_p' = UnparseC.terms simpl_p', nofalse = nofalse};( *TODOO*)
13.20 in
13.21 if nofalse
13.22 then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
13.23 @@ -140,7 +145,7 @@
13.24 (*asm false .. thm not applied ^^^; continue until False vvv*)
13.25 else chk (indets @ [t] @ a') asms);
13.26 in chk [] asms end
13.27 -and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
13.28 +and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
13.29 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
13.30 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
13.31 let
14.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Fri May 07 18:12:51 2021 +0200
14.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Tue Jun 01 15:41:23 2021 +0200
14.3 @@ -25,54 +25,36 @@
14.4 \<close> ML \<open>
14.5 (*** evaluate binary associative operations ***)
14.6
14.7 -fun eval_binop (_(*thmid*) : string) (op_: string)
14.8 - (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
14.9 - if op0 = op0' then
14.10 - case (Eval.numeral t1, Eval.numeral t2) of
14.11 - (SOME n1, SOME n2) =>
14.12 - let
14.13 - val (T1, _, _) = TermC.dest_binop_typ t0
14.14 - val res =
14.15 - Eval.calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
14.16 - (*WN071229 "Rings.divide_class.divide" never tried*)
14.17 - val rhs = Eval.var_op_float v op_ t0 T1 res
14.18 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
14.19 - in SOME ("#: " ^ UnparseC.term prop, prop) end
14.20 - | _ => NONE
14.21 +fun eval_binop _ _
14.22 + (t as ((opp as Const (op0, _)) $ (Const (op0', _) $ v $ t1) $ t2)) _ =(* binary . (v.n1).n2 *)
14.23 + if op0 = op0' andalso TermC.is_num t1 andalso TermC.is_num t2 then
14.24 + let
14.25 + val op' = if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0
14.26 + val res = Eval.calcul op' (t1, t2);
14.27 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
14.28 + in SOME ("#: " ^ UnparseC.term prop, prop) end
14.29 else NONE
14.30 - | eval_binop _ (op_ : string)
14.31 - (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
14.32 - if op0 = op0' then
14.33 - case (Eval.numeral t1, Eval.numeral t2) of
14.34 - (SOME n1, SOME n2) =>
14.35 - if op0 = "Groups.minus_class.minus" then NONE
14.36 - else let
14.37 - val (T1, _, _) = TermC.dest_binop_typ t0
14.38 - val res = Eval.calcul op0 n1 n2
14.39 - val rhs = Eval.float_op_var v op_ t0 T1 res
14.40 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
14.41 - in SOME ("#: " ^ UnparseC.term prop, prop) end
14.42 - | _ => NONE
14.43 + | eval_binop _ (_ : string)
14.44 + (t as ((opp as Const (op0, _)) $ t1 $ (Const (op0', _) $ t2 $ v))) _ =(* binary . n1.(n2.v) *)
14.45 + if op0 = op0' andalso op0 <> "Groups.minus_class.minus"
14.46 + andalso TermC.is_num t1 andalso TermC.is_num t2 then
14.47 + let
14.48 + val res = Eval.calcul op0 (t1, t2);
14.49 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ res $ v));
14.50 + in
14.51 + SOME ("#: " ^ UnparseC.term prop, prop)
14.52 + end
14.53 else NONE
14.54 - | eval_binop _ _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
14.55 - (case (Eval.numeral t1, Eval.numeral t2) of
14.56 - (SOME n1, SOME n2) =>
14.57 - let
14.58 - val (_, _, Trange) = TermC.dest_binop_typ t0;
14.59 - val res = Eval.calcul op0 n1 n2;
14.60 - val rhs = Eval.term_of_float Trange res;
14.61 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs));
14.62 - in SOME ("#: " ^ UnparseC.term prop, prop) end
14.63 - | _ => NONE)
14.64 + | eval_binop _ _ (t as (Const (op0, _) $ t1 $ t2)) _ = (* binary . n1.n2 *)
14.65 + if TermC.is_num t1 andalso TermC.is_num t2 then
14.66 + let
14.67 + val res = Eval.calcul op0 (t1, t2);
14.68 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
14.69 + in
14.70 + SOME ("#: " ^ UnparseC.term prop, prop)
14.71 + end
14.72 + else NONE
14.73 | eval_binop _ _ _ _ = NONE;
14.74 -(*
14.75 -> val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
14.76 -> UnparseC.term t;
14.77 -val it = "-1 + 2 = 1"
14.78 -> val t = str2term "-1 * (-1 * a)";
14.79 -> val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
14.80 -> UnparseC.term t;
14.81 -val it = "-1 * (-1 * a) = 1 * a"*)
14.82 \<close> ML \<open>
14.83 \<close> ML \<open>
14.84 \<close>
15.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Fri May 07 18:12:51 2021 +0200
15.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Jun 01 15:41:23 2021 +0200
15.3 @@ -310,12 +310,12 @@
15.4 (case arg of
15.5 Const (n1, _) =>
15.6 SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
15.7 - | Free (n1, _) =>
15.8 - if TermC.is_num' n1
15.9 - then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
15.10 - else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
15.11 - | _ => (*NONE*)
15.12 - SOME (TermC.mk_thmid thmid (UnparseC.term arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
15.13 + | n1 =>
15.14 + if TermC.is_num n1
15.15 + then SOME (TermC.mk_thmid thmid (TermC.string_of_num n1) "",
15.16 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
15.17 + else SOME (TermC.mk_thmid thmid (UnparseC.term n1) "",
15.18 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
15.19 | eval_const _ _ _ _ = NONE;
15.20
15.21 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
15.22 @@ -336,17 +336,19 @@
15.23 (*.evaluate < and <= for numerals.*)
15.24 (*("le" ,("Orderings.ord_class.less" , Prog_Expr.eval_equ "#less_")),
15.25 ("leq" ,("Orderings.ord_class.less_eq" , Prog_Expr.eval_equ "#less_equal_"))*)
15.26 -fun eval_equ (thmid:string) (_(*op_*)) (t as
15.27 - (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
15.28 - (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
15.29 - (SOME n1', SOME n2') =>
15.30 - if Eval.calc_equ (strip_thy op0) (n1', n2')
15.31 - then SOME (TermC.mk_thmid thmid n1 n2,
15.32 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
15.33 - else SOME (TermC.mk_thmid thmid n1 n2,
15.34 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
15.35 - | _ => NONE)
15.36 -
15.37 +fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =
15.38 + if TermC.is_num t1 andalso TermC.is_num t2 then
15.39 + let
15.40 + val n1 = t1 |> HOLogic.dest_number |> snd
15.41 + val n2 = t2 |> HOLogic.dest_number |> snd
15.42 + in
15.43 + if Eval.calc_equ (strip_thy op0) (n1, n2)
15.44 + then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
15.45 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
15.46 + else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
15.47 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
15.48 + end
15.49 + else NONE
15.50 | eval_equ _ _ _ _ = NONE;
15.51
15.52
15.53 @@ -429,25 +431,21 @@
15.54
15.55 (*. evaluate HOL.divide .*)
15.56 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
15.57 -fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
15.58 - (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
15.59 - (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
15.60 - (SOME n1', SOME n2') =>
15.61 - let
15.62 - val sg = Eval.sign_mult n1' n2';
15.63 - val (T1,T2,Trange) = TermC.dest_binop_typ t0;
15.64 - val gcd' = Eval.gcd (abs n1') (abs n2');
15.65 - in if gcd' = abs n2'
15.66 - then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
15.67 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
15.68 - in SOME (TermC.mk_thmid thmid n1 n2, prop) end
15.69 - else if 0 < n2' andalso gcd' = 1 then NONE
15.70 - else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
15.71 - ((abs n2') div gcd')
15.72 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
15.73 - in SOME (TermC.mk_thmid thmid n1 n2, prop) end
15.74 - end
15.75 - | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))
15.76 +fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ =
15.77 + if TermC.is_num t1 andalso TermC.is_num t2 then
15.78 + let
15.79 + val (T, _) = HOLogic.dest_number t1;
15.80 + val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
15.81 + val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
15.82 + in
15.83 + if (i1', i2') = (i1, i2) then NONE
15.84 + else
15.85 + let
15.86 + val res = TermC.mk_frac T res_int;
15.87 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
15.88 + in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end
15.89 + end
15.90 + else NONE
15.91 | eval_cancel _ _ _ _ = NONE;
15.92
15.93 (* get the argument from a function-definition *)
16.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Fri May 07 18:12:51 2021 +0200
16.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Tue Jun 01 15:41:23 2021 +0200
16.3 @@ -14,16 +14,22 @@
16.4 val squfact: int -> int
16.5 val gcd: int -> int -> int
16.6 val sqrt: int -> int
16.7 + val cancel_int: int * int -> int * (int * int)
16.8 val adhoc_thm: theory -> string * Eval_Def.eval_fn -> term -> (string * thm) option
16.9 val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option
16.10 val norm: term -> term
16.11 val popt2str: ('a * term) option -> string
16.12 +(** )
16.13 val numeral: term -> ((int * int) * (int * int)) option
16.14 - val calcul: string -> float -> float -> float
16.15 +( **)
16.16 + val calcul: string -> term * term -> term
16.17 +(** )
16.18 val term_of_float: typ -> float -> term
16.19 val var_op_float: term -> string -> typ -> typ ->float -> term
16.20 val float_op_var: term -> string -> typ -> typ -> float -> term
16.21 +( **)
16.22 val trace_on: bool Unsynchronized.ref
16.23 + val int_of_numeral: term -> int
16.24 \<^isac_test>\<open>
16.25 val get_pair: theory -> string -> Eval_Def.eval_fn -> term -> (string * term) option
16.26 val mk_rule: term list * term * term -> term
16.27 @@ -61,6 +67,14 @@
16.28 else if n = 0 then 0 else 1;
16.29 fun sign_mult n1 n2 = (sign n1) * (sign n2);
16.30
16.31 +fun cancel_int (i1, i2) =
16.32 + let
16.33 + val sg = sign_mult i1 i2;
16.34 + val gcd' = gcd (abs i1) (abs i2);
16.35 + in
16.36 + (sg, ((abs i1) div gcd', (abs i2) div gcd'))
16.37 + end;
16.38 +
16.39 infix dvd;
16.40 fun d dvd n = n mod d = 0;
16.41 fun divisors n =
16.42 @@ -109,14 +123,14 @@
16.43 fun trace_calc4 str t1 t2 =
16.44 if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
16.45
16.46 -fun get_pair thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
16.47 +fun get_pair thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
16.48 if op_ = op0 then
16.49 let val popt = ef op_ t thy
16.50 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
16.51 else get_pair thy op_ ef arg
16.52 | get_pair thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
16.53 - ef "Prog_Expr.ident" t thy (* not nested *)
16.54 - | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *)
16.55 + ef "Prog_Expr.ident" t thy (* not nested *)
16.56 + | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
16.57 (trace_calc1 "1.. get_pair: binop = " op_;
16.58 if op_ = op0 then
16.59 let
16.60 @@ -165,7 +179,7 @@
16.61 fun adhoc_thm1_ thy (op_, eval_fn) ct =
16.62 case eval_fn op_ ct thy of
16.63 NONE => NONE
16.64 - | SOME (thmid,t) => SOME (thmid, Skip_Proof.make_thm thy t);
16.65 + | SOME (thmid, t) => SOME (thmid, Skip_Proof.make_thm thy t);
16.66
16.67 (** for ordered and conditional rewriting **)
16.68
16.69 @@ -194,49 +208,46 @@
16.70 else (*3*) mk_rule (prems, concl, @{term True})
16.71 end;
16.72
16.73 -(* convert int and float to internal floatingpoint prepresentation.*)
16.74 +(* convert int and float to internal floatingpoint prepresentation *)
16.75 +(** )
16.76 fun numeral (Free (str, _)) =
16.77 (case ThmC_Def.int_opt_of_string str of
16.78 - SOME i => SOME ((i, 0), (0, 0))
16.79 - | NONE => NONE)
16.80 + SOME i => SOME ((i, 0), (0, 0))
16.81 + | NONE => NONE)
16.82 | numeral (Const ("Float.Float", _) $
16.83 (Const ("Product_Type.Pair", _) $
16.84 (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
16.85 - (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
16.86 + (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_)))) =
16.87 (case (ThmC_Def.int_opt_of_string v1, ThmC_Def.int_opt_of_string v2, ThmC_Def.int_opt_of_string p1, ThmC_Def.int_opt_of_string p2) of
16.88 - (SOME v1', SOME v2', SOME p1', SOME p2') =>
16.89 - SOME ((v1', v2'), (p1', p2'))
16.90 - | _ => NONE)
16.91 + (SOME v1', SOME v2', SOME p1', SOME p2') => SOME ((v1', v2'), (p1', p2'))
16.92 + | _ => NONE)
16.93 | numeral _ = NONE;
16.94 +( **)
16.95
16.96 (*** handle numerals in eval_binop ***)
16.97 -(* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:
16.98 - Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
16.99
16.100 -(* used for calculating built in binary operations in Isabelle2002.
16.101 - integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0) *)
16.102 -fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
16.103 - if b < d
16.104 - then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
16.105 - else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
16.106 - | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
16.107 - ((a - c,0),(0,0))
16.108 - | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
16.109 - ((a * c, b + d), (0, 0))
16.110 - | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
16.111 - ((a div c, 0), (0, 0))
16.112 - | calcul "Transcendental.powr" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
16.113 - ((power a c, 0), (0, 0))
16.114 - | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
16.115 - raise ERROR ("calcul: not impl. for Float (("^
16.116 - (string_of_int a )^", "^(string_of_int b )^"), ("^
16.117 - (string_of_int p11)^", "^(string_of_int p12)^")) "^op_^" (("^
16.118 - (string_of_int c )^", "^(string_of_int d )^"), ("^
16.119 - (string_of_int p21)^", "^(string_of_int p22)^"))");
16.120 -(*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
16.121 -val it = ((1,0),(0,0))*)
16.122 +(* preliminary HACK *)
16.123 +fun int_of_numeral (Const ("Groups.zero_class.zero", _)) = 0
16.124 + | int_of_numeral (Const ("Groups.one_class.one", _)) = 1
16.125 + | int_of_numeral (Const ("Groups.uminus_class.uminus", _) $ t) = ~1 * int_of_numeral t
16.126 + | int_of_numeral (Const ("Num.numeral_class.numeral", _) $ n) = HOLogic.dest_numeral n
16.127 + | int_of_numeral t = raise TERM ("int_of_numeral", [t]);
16.128 +
16.129 +fun calcul op_ (t1, t2) =
16.130 + let
16.131 + val (T, _) = HOLogic.dest_number t1
16.132 + val (i1, i2) = (int_of_numeral t1, int_of_numeral t2)
16.133 + val result =
16.134 + case op_ of
16.135 + "Groups.plus_class.plus" => i1 + i2 (* preliminary HACK *)
16.136 + | "Groups.minus_class.minus" => i1 - i2 (* preliminary HACK *)
16.137 + | "Groups.times_class.times" => i1 * i2 (* preliminary HACK *)
16.138 + | "Transcendental.powr" => power i1 i2 (* preliminary HACK *)
16.139 + | str => raise ERROR ("calcul not impl.for op_ " ^ str)
16.140 + in HOLogic.mk_number T result end;
16.141
16.142 (*.convert internal floatingpoint prepresentation to int and float.*)
16.143 +(** )
16.144 fun term_of_float T ((val1, 0), ( 0, 0)) =
16.145 TermC.term_of_num T val1
16.146 | term_of_float T ((val1, val2), (precision1, precision2)) =
16.147 @@ -247,6 +258,7 @@
16.148 (TermC.pairt (Free (TermC.str_of_int precision1, T))
16.149 (Free (TermC.str_of_int precision2, T))))
16.150 end;
16.151 +( **)
16.152 (*> val t = str2term "Float ((1,2),(0,0))";
16.153 > val Const ("Float.Float", fT) $ _ = t;
16.154 > atomtyp fT;
16.155 @@ -260,6 +272,7 @@
16.156 val it = true : bool*)
16.157
16.158 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
16.159 +(** )
16.160 fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
16.161 TermC.mk_var_op_num v op_ optype ntyp v1
16.162 | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
16.163 @@ -271,6 +284,7 @@
16.164 (TermC.pairt (Free (TermC.str_of_int p1, T))
16.165 (Free (TermC.str_of_int p2, T)))))
16.166 end;
16.167 +( **)
16.168 (*> val t = str2term "a + b";
16.169 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
16.170 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
16.171 @@ -278,6 +292,7 @@
16.172 val it = true : bool*)
16.173
16.174 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
16.175 +(** )
16.176 fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
16.177 TermC.mk_num_op_var v op_ optype ntyp v1
16.178 | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
16.179 @@ -289,6 +304,7 @@
16.180 (TermC.pairt (Free (TermC.str_of_int p1, T))
16.181 (Free (TermC.str_of_int p2, T))))) $ v
16.182 end;
16.183 +( **)
16.184 (*> val t = str2term "a + b";
16.185 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
16.186 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
17.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Fri May 07 18:12:51 2021 +0200
17.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Tue Jun 01 15:41:23 2021 +0200
17.3 @@ -73,8 +73,11 @@
17.4 case Subst.T_from_string_eqs @{theory} string_eqs of
17.5 [(Free ("bdv_1", _), Free ("x", _)),
17.6 (Free ("bdv_2", _), Free ("y", _)),
17.7 - (Free ("xxx", _), Const ("Groups.plus_class.plus", _) $ Free ("aaa", _) $ Free ("111", _))] => ()
17.8 -| _ => error "";
17.9 + (Free ("xxx", _),
17.10 + Const ("Groups.plus_class.plus", _) $ Free ("aaa", _) $
17.11 + (Const ("Num.numeral_class.numeral", _) $
17.12 + (Const ("Num.num.Bit1", _) $ _ )))] => ()
17.13 +| _ => error "fun T_from_string_eqs";
17.14
17.15 "-------- fun input_to_terms -------------------------------------------------";
17.16 "-------- fun input_to_terms -------------------------------------------------";
18.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Fri May 07 18:12:51 2021 +0200
18.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue Jun 01 15:41:23 2021 +0200
18.3 @@ -3,16 +3,17 @@
18.4 (c) due to copyright terms
18.5 *)
18.6
18.7 -"--------------------------------------------------------";
18.8 -"table of contents --------------------------------------";
18.9 -"--------------------------------------------------------";
18.10 +"-----------------------------------------------------------------------------------------------";
18.11 +"table of contents -----------------------------------------------------------------------------";
18.12 +"-----------------------------------------------------------------------------------------------";
18.13 "----------- numerals in Isabelle2011/12/13 -------------";
18.14 "----------- inst_bdv -----------------------------------";
18.15 "----------- subst_atomic_all ---------------------------";
18.16 "----------- Pattern.match ------------------------------";
18.17 "----------- fun TermC.matches --------------------------------";
18.18 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------";
18.19 -"----------- fun TermC.vars_of -----------------------------------------------------------------------";
18.20 +"----------- fun TermC.vars_of -----------------------------------------------------------------";
18.21 +"----------- fun TermC.vars --------------------------------------------------------------------";
18.22 "----------- uminus_to_string ---------------------------";
18.23 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
18.24 "----------- check writeln, tracing for string markup ---";
18.25 @@ -20,7 +21,7 @@
18.26 "----------- fun str_of_int --------------------------------------------------------------------";
18.27 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";
18.28 "----------- fun TermC.contains_Var ------------------------------------------------------------------";
18.29 -"----------- fun ThmC_Def.int_opt_of_string, fun TermC.is_num ----------------------------------------------------";
18.30 +"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";
18.31 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
18.32 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
18.33 "----------- fun TermC.strip_imp_prems' --------------------------------------------------------------";
18.34 @@ -30,6 +31,7 @@
18.35 "----------- fun TermC.is_list -----------------------------------------------------------------------";
18.36 "----------- fun inst_abs ----------------------------------------------------------------------";
18.37 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
18.38 +"----------- fun mk_frac, proper term with uminus ----------------------------------------------";
18.39 "--------------------------------------------------------";
18.40 "--------------------------------------------------------";
18.41
18.42 @@ -184,18 +186,18 @@
18.43 "----------- inst_bdv -----------------------------------";
18.44 "----------- inst_bdv -----------------------------------";
18.45 if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm d1_isolate_add2} =
18.46 - "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = -1 * ?a)"
18.47 + "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)"
18.48 then ()
18.49 else error "termC.sml d1_isolate_add2";
18.50 val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
18.51 val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm d1_isolate_add2});
18.52 val t' = TermC.inst_bdv subst t;
18.53 - if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = -1 * ?a)"
18.54 + if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)"
18.55 then ()
18.56 else error "termC.sml inst_bdv 1";
18.57 if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm separate_bdvs_add} =
18.58 - "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n "
18.59 - ^ "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
18.60 + "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n " ^
18.61 + "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"
18.62 then () else error "termC.sml separate_bdvs_add";
18.63 (*default_print_depth 5;*)
18.64
18.65 @@ -207,8 +209,8 @@
18.66 val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm separate_bdvs_add});
18.67 val t' = TermC.inst_bdv subst t;
18.68
18.69 -if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n"
18.70 - ^ "(?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
18.71 +if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^
18.72 + "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"
18.73 then () else error "termC.sml inst_bdv 2";
18.74
18.75 "----------- subst_atomic_all ---------------------------";
18.76 @@ -297,8 +299,8 @@
18.77 else error "termC.sml diff.behav. in TermC.matches true 2";
18.78 "----- test 2b false";
18.79 val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
18.80 - if TermC.matches thy tm pa then ()
18.81 - else error "termC.sml diff.behav. in TermC.matches false 2";
18.82 + if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"
18.83 + else ();
18.84 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
18.85 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"
18.86 else ();*)
18.87 @@ -400,9 +402,9 @@
18.88 |> writeln
18.89 end *)
18.90
18.91 -"----------- fun TermC.vars_of -----------------------------------------------------------------------";
18.92 -"----------- fun TermC.vars_of -----------------------------------------------------------------------";
18.93 -"----------- fun TermC.vars_of -----------------------------------------------------------------------";
18.94 +"----------- fun TermC.vars_of -----------------------------------------------------------------";
18.95 +"----------- fun TermC.vars_of -----------------------------------------------------------------";
18.96 +"----------- fun TermC.vars_of -----------------------------------------------------------------";
18.97 val thy = @{theory Partial_Fractions};
18.98 val ctxt = Proof_Context.init_global @{theory}
18.99
18.100 @@ -411,10 +413,24 @@
18.101 | _ => error "TermC.vars_of (x \<up> 2 + -1 * x * y) ..changed";
18.102
18.103 val SOME t = TermC.parseNEW ctxt "3 = 3 * AA / 4";
18.104 -
18.105 case TermC.vars_of t of [Const ("Partial_Fractions.AA", _), Const ("HOL.eq", _)] => ()
18.106 | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";
18.107 +
18.108
18.109 +"----------- fun TermC.vars --------------------------------------------------------------------";
18.110 +"----------- fun TermC.vars --------------------------------------------------------------------";
18.111 +"----------- fun TermC.vars --------------------------------------------------------------------";
18.112 +val thy = @{theory Partial_Fractions};
18.113 +val ctxt = Proof_Context.init_global @{theory}
18.114 +
18.115 +val SOME t = TermC.parseNEW ctxt "x \<up> 2 + -1 * x * y";
18.116 +case TermC.vars t of [Free ("x", _), Free ("y", _)] => ()
18.117 +| _ => error "TermC.vars_of (x \<up> 2 + -1 * x * y) ..changed";
18.118 +
18.119 +val SOME t = TermC.parseNEW ctxt "3 = 3 * AA / 4";
18.120 +case TermC.vars t of [] => ()
18.121 +| _ => error "TermC.vars (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";
18.122 +
18.123
18.124 "----------- uminus_to_string ---------------------------";
18.125 "----------- uminus_to_string ---------------------------";
18.126 @@ -581,9 +597,9 @@
18.127 val t = TermC.parse_patt @{theory} "z = 3";
18.128 if TermC.contains_Var t = false then () else error "TermC.contains_Var ?z = 3";
18.129
18.130 -"----------- fun ThmC_Def.int_opt_of_string, fun TermC.is_num ----------------------------------------------------";
18.131 -"----------- fun ThmC_Def.int_opt_of_string, fun TermC.is_num ----------------------------------------------------";
18.132 -"----------- fun ThmC_Def.int_opt_of_string, fun TermC.is_num ----------------------------------------------------";
18.133 +"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";
18.134 +"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";
18.135 +"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";
18.136 case ThmC_Def.int_opt_of_string "123" of
18.137 SOME 123 => () | _ => raise error "ThmC_Def.int_opt_of_string 123 changed";
18.138 case ThmC_Def.int_opt_of_string "(-123)" of
18.139 @@ -687,9 +703,50 @@
18.140 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
18.141 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
18.142 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
18.143 -if ThmC_Def.num_to_Free @{term "123::real"} = Free ("123", HOLogic.realT)
18.144 -then () else error "ThmC_Def.num_to_Free '123' changed";
18.145 -if ThmC_Def.num_to_Free @{term "1::real"} = Free ("1", HOLogic.realT)
18.146 -then () else error "ThmC_Def.num_to_Free '1' changed";
18.147 -if ThmC_Def.num_to_Free @{term "0::real"} = Free ("0", HOLogic.realT)
18.148 -then () else error "ThmC_Def.num_to_Free '0' changed";
18.149 +case ThmC_Def.num_to_Free @{term "123::real"} of
18.150 + Const ("Num.numeral_class.numeral", _) $
18.151 + (Const ("Num.num.Bit1", _) $
18.152 + (Const ("Num.num.Bit1", _) $
18.153 + (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ (Const ("Num.num.Bit1", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))))))) => ()
18.154 +| _ => error "ThmC_Def.num_to_Free '123' changed";
18.155 +
18.156 +case ThmC_Def.num_to_Free @{term "1::real"} of
18.157 + Const ("Groups.one_class.one", _) => ()
18.158 +| _ => error "ThmC_Def.num_to_Free '1' changed";
18.159 +
18.160 +case ThmC_Def.num_to_Free @{term "0::real"} of
18.161 + Const ("Groups.zero_class.zero", _) => ()
18.162 +| _ => error "ThmC_Def.num_to_Free '0' changed";
18.163 +
18.164 +"----------- fun mk_frac, proper term with uminus ----------------------------------------------";
18.165 +"----------- fun mk_frac, proper term with uminus ----------------------------------------------";
18.166 +"----------- fun mk_frac, proper term with uminus ----------------------------------------------";
18.167 + TermC.mk_frac: typ -> int * (int * int) -> term;
18.168 + TermC.mk_frac HOLogic.realT (~1, (6, 8));
18.169 +"~~~~~ fun mk_frac , args:"; val (T, (sg, (i1, i2))) = (HOLogic.realT, (~1, (6, 8)));
18.170 +val xxx = (*return value*) Const ("Rings.divide_class.divide", T --> T) $
18.171 + mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2;
18.172 +
18.173 +val (T_div, T_uminus) =
18.174 +case xxx of
18.175 + Const ("Rings.divide_class.divide", T_div) $ (* divide *)
18.176 + (Const ("Groups.uminus_class.uminus", T_uminus) $ (* uminus *)
18.177 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ))) $
18.178 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ))
18.179 + => (T_div, T_uminus)
18.180 +| _ => error "mk_frac 6 / - 8 \<longrightarrow> - 3 / 4 CHANGED";
18.181 +
18.182 +case T_div of
18.183 + Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]) => ()
18.184 +| _ => error "T_div CHANGED in fun mk_frac";
18.185 +case T_uminus of
18.186 + Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]) => ()
18.187 +| _ => error "T_uminus CHANGED in fun mk_frac";
18.188 +
18.189 +(* IMproper term for "6 / - 8 = - 3 / (4::real)"
18.190 +
18.191 + (Const ("Groups.uminus_class.uminus", _) $ (* uminus *)
18.192 + (Const ("Rings.divide_class.divide", _) $ (* divide *)
18.193 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ))) $
18.194 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ _ ) ))))
18.195 +*)
19.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri May 07 18:12:51 2021 +0200
19.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue Jun 01 15:41:23 2021 +0200
19.3 @@ -19,6 +19,7 @@
19.4 "----------- fun mono_deg_in -------------------------------------------------------------------";
19.5 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
19.6 "-------- investigate (new 2002) uniary minus -----------";
19.7 +"----------- fun sort_variables ----------------------------------------------------------------";
19.8 "-------- check make_polynomial with simple terms -------";
19.9 "-------- fun is_multUnordered --------------------------";
19.10 "-------- examples from textbook Schalk I ---------------";
19.11 @@ -196,15 +197,15 @@
19.12 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
19.13 val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
19.14 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
19.15 -if UnparseC.term t' = "-8 - 2 * x + x \<up> 2 is_expanded_in x = True"
19.16 - andalso id = "-8 - 2 * x + x \<up> 2 is_expanded_in x = True"
19.17 +if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
19.18 + andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
19.19 then () else error "eval_is_expanded_in x ..changed";
19.20
19.21 val thy = @{theory Partial_Fractions}
19.22 val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
19.23 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
19.24 -if UnparseC.term t' = "-8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
19.25 - andalso id = "-8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
19.26 +if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
19.27 + andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
19.28 then () else error "eval_is_expanded_in AA ..changed";
19.29
19.30
20.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Fri May 07 18:12:51 2021 +0200
20.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Jun 01 15:41:23 2021 +0200
20.3 @@ -256,21 +256,21 @@
20.4
20.5 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
20.6 writeln "---------- rewrite_terms_ 1---------------------------";
20.7 -if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
20.8 +if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
20.9 else error "rewrite.sml rewrite_terms_ [x = 0]";
20.10
20.11 val equs = [TermC.str2term "M_b 0 = 0"];
20.12 -val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
20.13 +val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
20.14 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
20.15 writeln "---------- rewrite_terms_ 2---------------------------";
20.16 -if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
20.17 +if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
20.18 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
20.19
20.20 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
20.21 -val t = TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
20.22 +val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
20.23 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
20.24 writeln "---------- rewrite_terms_ 3---------------------------";
20.25 -if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
20.26 +if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
20.27 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
20.28
20.29
21.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Fri May 07 18:12:51 2021 +0200
21.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Tue Jun 01 15:41:23 2021 +0200
21.3 @@ -49,7 +49,7 @@
21.4 (@{theory Isac_Knowledge},
21.5 Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
21.6
21.7 -if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
21.8 +if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = - 1 * ?z1" then ()
21.9 else error "input to revert_sym_rule CHANGED";
21.10
21.11 (*if*) is_sym (cut_id id) (*then*);
21.12 @@ -61,11 +61,11 @@
21.13 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
21.14 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
21.15 ;
21.16 -if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
21.17 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "- 1 * ?z = - ?z"
21.18 then () else error "fun revert_sym_rule changed 1";
21.19
21.20 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
21.21 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
21.22 ;
21.23 -if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
21.24 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b"
21.25 then () else error "fun revert_sym_rule changed 2"
22.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri May 07 18:12:51 2021 +0200
22.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue Jun 01 15:41:23 2021 +0200
22.3 @@ -35,8 +35,11 @@
22.4 (* ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt
22.5 IN Minimsubpbl/150-add-given.sml IS CAUSED HEREBY:*)
22.6 case oris of
22.7 - ((1, [1], "#Given", Const ("Input_Descript.equality", _),
22.8 - [Const ("HOL.eq", _) $ _ $ Free ("2", _)]) :: _) => ()
22.9 + [(1, [1], "#Given", Const ("Input_Descript.equality", _),
22.10 + [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Const ("Partial_Fractions.AA", _) $ Const ("Groups.one_class.one", _)) $
22.11 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))]),
22.12 + (2, [1], "#Given", Const ("Input_Descript.solveFor", _), [Const ("Partial_Fractions.AA", _)]),
22.13 + (3, [1], "#Find", Const ("Input_Descript.solutions", _), [Free ("L", _)])] => ()
22.14 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
22.15 | _ => error ""
22.16
22.17 @@ -48,8 +51,11 @@
22.18 val oris = O_Model.init fmz thy yyy
22.19 ;
22.20 case oris of
22.21 - ((1, [1], "#Given", Const ("Input_Descript.equality", _),
22.22 - [Const ("HOL.eq", _) $ _ $ Free ("2", _)]) :: _) => ()
22.23 + [(1, [1], "#Given", Const ("Input_Descript.equality", _),
22.24 + [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Const ("Partial_Fractions.AA", _) $ Const ("Groups.one_class.one", _)) $
22.25 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))]),
22.26 + (2, [1], "#Given", Const ("Input_Descript.solveFor", _), [Const ("Partial_Fractions.AA", _)]),
22.27 + (3, [1], "#Find", Const ("Input_Descript.solutions", _), [Free ("L", _)])] => ()
22.28 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
22.29 | _ => error ""
22.30
22.31 @@ -57,12 +63,13 @@
22.32 val ctxt = ContextC.initialise' thy fmz;
22.33 (*ADD check*)
22.34 case TermC.parseNEW ctxt "equality (x+1=(2::real))" of
22.35 - SOME (Const ("Input_Descript.equality", _) (* <<< ---------------- this needs to be recognised *) $
22.36 - (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
22.37 - Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => ()
22.38 + SOME (Const ("Input_Descript.equality", _) $
22.39 + (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("x", _) $ Const ("Groups.one_class.one", _)) $
22.40 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _))))
22.41 + ) => ()
22.42 | SOME (Free ("equality", _) $
22.43 (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
22.44 - Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => error ""
22.45 + Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => error "xxx"
22.46 | _ => error "something is wrong with initialising Minisubpnl";
22.47
22.48 val [(fmz, (dI',pI',mI'))] = [(fmz''''', spec''''')];
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Jun 01 15:41:23 2021 +0200
23.3 @@ -0,0 +1,38 @@
23.4 +(* Title: "ProgLang/calculate.sml"
23.5 + Author: Walther Neuper 2021
23.6 + (c) copyright due to lincense terms.
23.7 +*)
23.8 +
23.9 +"-----------------------------------------------------------------------------------------------";
23.10 +"table of contents -----------------------------------------------------------------------------";
23.11 +"-----------------------------------------------------------------------------------------------";
23.12 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
23.13 +"-----------------------------------------------------------------------------------------------";
23.14 +"-----------------------------------------------------------------------------------------------";
23.15 +"-----------------------------------------------------------------------------------------------";
23.16 +
23.17 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
23.18 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
23.19 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
23.20 +val (t1, t2) = (@{term 3}, @{term "2::real"});
23.21 +val t = HOLogic.mk_binop "Groups.plus_class.plus" (t1, t2);
23.22 +
23.23 + eval_binop "" "" t "";
23.24 +"~~~~~ fun eval_binop , args:"; val (_, _, (t as (Const (op0, t0) $ t1 $ t2)), _) =(* binary . n1.n2 *)
23.25 + ((), (), t, ());
23.26 + (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
23.27 + val res = calcul op0 (t1, t2);
23.28 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
23.29 + (*in*)
23.30 + val xxx = SOME ("#: " ^ UnparseC.term prop, prop);
23.31 + (*end*)
23.32 +
23.33 +case xxx of
23.34 + SOME
23.35 + ("#: (3::'a) + 2 = (5::'a)",
23.36 + Const ("HOL.Trueprop", _) $
23.37 + (Const ("HOL.eq", _) $
23.38 + (Const ("Groups.plus_class.plus", _) $ _ $
23.39 + (Const ("Num.numeral_class.numeral", _) $ _ )) $
23.40 + _ )) => ()
23.41 +| _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED"
24.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Fri May 07 18:12:51 2021 +0200
24.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Jun 01 15:41:23 2021 +0200
24.3 @@ -1,5 +1,4 @@
24.4 (* Title: "ProgLang/evaluate.sml"
24.5 - test calculation of values for function constants
24.6 Author: Walther Neuper 2000
24.7 (c) copyright due to lincense terms.
24.8 *)
24.9 @@ -14,9 +13,11 @@
24.10 "----------- calculate from Prog --------------------------------- -----------------------------";
24.11 "----------- calculate from script --requires 'setup'----";
24.12 "----------- calculate check test-root-equ --------------";
24.13 -"----------- check calcul,ate bottom up -----------------";
24.14 +"----------- check calculate bottom up -----------------";
24.15 "----------- Prog_Expr.pow Power.power_class.power ---------";
24.16 " ================= evaluate.sml: calculate_ 2002 ======";
24.17 +"----------- fun cancel_int --------------------------------------------------------------------";
24.18 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
24.19 "----------- get_pair with 3 args -----------------------";
24.20 "----------- calculate (2 * x is_const) -----------------";
24.21 "----------- fun get_pair: examples ------------------------------------------------------------";
24.22 @@ -46,11 +47,11 @@
24.23 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
24.24 val thy = @{theory};
24.25 val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
24.26 -val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
24.27 -val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
24.28 -val pow = ("Transcendental.powr" ,eval_binop "#power_") : string * Eval_Def.eval_fn;
24.29 +val plus = ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
24.30 +val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
24.31 +val pow = ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn;
24.32
24.33 -"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
24.34 +"~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
24.35 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
24.36 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
24.37 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
24.38 @@ -76,7 +77,7 @@
24.39 val thy = @{theory "Test"};
24.40 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
24.41 val (dI',pI',mI') =
24.42 - ("Test",["calculate", "test"],["Test", "test_calculate"]);
24.43 + ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
24.44
24.45 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
24.46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.47 @@ -158,13 +159,17 @@
24.48 (*--------------(5): reproduce (1) with simpler term: ------------*)
24.49 val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
24.50 case rewrite_set_ thy false rls t of
24.51 - SOME (Free ("4", _), []) => ()
24.52 -| _ => error "rewrite_set_ (3+5)/2 changed";
24.53 + SOME (t', []) =>
24.54 + if UnparseC.term t' = "4" then ()
24.55 + else error "rewrite_set_ (3+5)/2 changed 1"
24.56 +| _ => error "rewrite_set_ (3+5)/2 changed 2";
24.57
24.58 val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
24.59 case rewrite_set_ thy false rls t of
24.60 - SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
24.61 -| _ => error "rewrite_set_ (3+1+2*x)/2 changed";
24.62 + SOME (t', _) =>
24.63 + if UnparseC.term t' = "x + (1 / 2 + 3 / 2)" (*ERROR should be : 2 * x SEE ABOVE*) then ()
24.64 + else error "rewrite_set_ (3+1+2*x)/2 changed 1"
24.65 +| _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
24.66
24.67 Rewrite.trace_on:=false; (*=true3.6.03*)
24.68
24.69 @@ -200,7 +205,7 @@
24.70 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
24.71 val t = (Thm.term_of o the o (TermC.parse thy)) "x + (-1 + -3) / 2";
24.72 val SOME (res, []) = rewrite_set_ thy false rls t;
24.73 -if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
24.74 +if UnparseC.term res = "x + - 2" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
24.75 "x + (-4) / 2";
24.76 (*
24.77 ### trying calc. 'cancel'
24.78 @@ -217,24 +222,6 @@
24.79
24.80 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
24.81
24.82 -"----------- Prog_Expr.pow Power.power_class.power ---------";
24.83 -"----------- Prog_Expr.pow Power.power_class.power ---------";
24.84 -"----------- Prog_Expr.pow Power.power_class.power ---------";
24.85 -val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
24.86 -TermC.atomty t;
24.87 -(*** -------------
24.88 -*** Const ( Nat.power, ['a, nat] => 'a)
24.89 -*** . Free ( 1, 'a)
24.90 -*** . Free ( aaa, nat) *)
24.91 -
24.92 -val t = TermC.str2term "1 \<up> aaa";
24.93 -TermC.atomty t;
24.94 -(****
24.95 -*** Const (Prog_Expr.pow, real => real => real)
24.96 -*** . Free (1, real)
24.97 -*** . Free (aaa, real)
24.98 -*** *);
24.99 -
24.100 " ================= evaluate.sml: calculate_ 2002 =================== ";
24.101 " ================= evaluate.sml: calculate_ 2002 =================== ";
24.102 " ================= evaluate.sml: calculate_ 2002 =================== ";
24.103 @@ -291,10 +278,64 @@
24.104 val SOME (id,t') = eval_fn op_ t thy;
24.105 (*** calc: operator = pow not defined*)
24.106
24.107 - val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
24.108 - val SOME (id,t') = eval_binop thmid op_ t thy;
24.109 +case (op_, t) of
24.110 + ("Transcendental.powr",
24.111 + Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
24.112 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => ()
24.113 +| _ => error "3 \<up> 2 CHANGED";
24.114 + val SOME (id, t') = eval_binop thmid op_ t thy;
24.115 (*** calc: operator = pow not defined*)
24.116
24.117 +if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED";
24.118 +
24.119 +
24.120 +"----------- fun cancel_int --------------------------------------------------------------------";
24.121 +"----------- fun cancel_int --------------------------------------------------------------------";
24.122 +"----------- fun cancel_int --------------------------------------------------------------------";
24.123 +if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED";
24.124 +if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED";
24.125 +if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
24.126 +
24.127 +
24.128 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
24.129 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
24.130 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
24.131 +val (t1, t2) = (@{term 3}, @{term "2::real"});
24.132 +
24.133 +"~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
24.134 + val (Const ("Num.numeral_class.numeral", _) $ n1) = t1;
24.135 + val (Const ("Num.numeral_class.numeral", _) $ n2) = t2;
24.136 + val (T, _) = HOLogic.dest_number t1
24.137 + val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
24.138 + val result =
24.139 + case op_ of
24.140 + "Groups.plus_class.plus" => i1 + i2
24.141 + | "Groups.minus_class.minus" => i1 - i2
24.142 + | "Groups.times_class.times" => i1 * i2
24.143 + | "Transcendental.powr" => power i1 i2
24.144 + | str => raise ERROR ("calcul not impl.for op_ " ^ str)
24.145 + (*in*)
24.146 + val xxx = HOLogic.mk_number T result;
24.147 + (*end*)
24.148 +case HOLogic.dest_number xxx of
24.149 + (_, 5) => ()
24.150 +| _ => error "calcul + 2 3 CHANGED";
24.151 +
24.152 +case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of
24.153 + (_, 1) => xxx
24.154 +| _ => error "calcul - 2 3 CHANGED";
24.155 +
24.156 +case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of
24.157 + (_, 6) => xxx
24.158 +| _ => error "calcul - 2 3 CHANGED";
24.159 +
24.160 +(* (calcul "Rings.divide_class.divide" (t1, t2)
24.161 +ERROR: calcul not impl.for op_ Rings.divide_class.divide*)
24.162 +
24.163 +case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of
24.164 + (_, 9) => xxx
24.165 +| _ => error "calcul - 2 3 CHANGED";
24.166 +
24.167
24.168 "----------- get_pair with 3 args --------------------------------";
24.169 "----------- get_pair with 3 args --------------------------------";
24.170 @@ -307,7 +348,7 @@
24.171 );
24.172 val SOME (str, simpl) = get_pair thy op_ ef arg;
24.173 if str =
24.174 -"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2 = True"
24.175 +"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
24.176 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
24.177
24.178
24.179 @@ -316,49 +357,50 @@
24.180 "----------- calculate (2 * x is_const) -----------------";
24.181 val t = TermC.str2term "2 * x is_const";
24.182 val SOME (str, t') = eval_const "" "" t @{theory Test};
24.183 -UnparseC.term t';
24.184 -"(2 * x is_const) = False";
24.185 +if UnparseC.term t' = "(2 * x is_const) = False" then ()
24.186 +else error "eval_const 2 * x is_const CHANGED";
24.187
24.188 val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
24.189 -UnparseC.term t';
24.190 -"HOL.False";
24.191 +if UnparseC.term t' = "False" then ()
24.192 +else error "rewrite_set_ 2 * x is_const CHANGED";
24.193
24.194 "----------- fun get_pair: examples ------------------------------------------------------------";
24.195 "----------- fun get_pair: examples ------------------------------------------------------------";
24.196 "----------- fun get_pair: examples ------------------------------------------------------------";
24.197 val thy = @{theory};
24.198 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
24.199 +if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
24.200
24.201 -val t = (Thm.term_of o the o (TermC.parse thy)) "3 + 4";
24.202 +val t = @{term "3 + 4 :: real"};
24.203 val SOME (str, term) = get_pair thy isa_str eval_fn t;
24.204 -if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
24.205 -then () else error "get_pair 3 + 4 changed";
24.206 +(*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
24.207 +(*+*)then () else error "get_pair 3 + 4 changed";
24.208
24.209 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a + 3) + 4";
24.210 +val t = @{term "(a + 3) + 4 :: real"};
24.211 val SOME (str, term) = get_pair thy isa_str eval_fn t;
24.212 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
24.213 then () else error "get_pair (a + 3) + 4 changed";
24.214
24.215 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a + 3) + 4";
24.216 +val t = @{term "(a + 3) + 4 :: real"};
24.217 val SOME (str, term) = get_pair thy isa_str eval_fn t;
24.218 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
24.219 then () else error "get_pair (a + 3) + 4 changed";
24.220
24.221 -val t = (Thm.term_of o the o (TermC.parse thy)) "x = 5 * (3 + (4 + a))";
24.222 +val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
24.223 val SOME (str, term) = get_pair thy isa_str eval_fn t;
24.224 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
24.225 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
24.226
24.227 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
24.228
24.229 -val t = (Thm.term_of o the o (TermC.parse thy)) "-4 / -2";
24.230 +val t = @{term "-4 / -2 :: real"};
24.231 val SOME (str, term) = get_pair thy isa_str eval_fn t;
24.232 -if str = "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2"
24.233 +if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
24.234 then () else error "get_pair -4 / -2 changed";
24.235
24.236 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
24.237
24.238 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 \<up> 3";
24.239 +val t = @{term "2 \<up> 3 :: real"};
24.240 val SOME (str, term) = get_pair thy isa_str eval_fn t;
24.241 if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
24.242 then () else error "get_pair 2 \<up> 3 changed";
24.243 @@ -368,18 +410,17 @@
24.244 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
24.245 (*--------------------------------------------------------------------vvvvvvvvvv*)
24.246 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
24.247 -val SOME t = parseNEW @{context} "9 is_const";
24.248 +val t = @{term "9 is_const"};
24.249 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
24.250 if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
24.251 then () else error "adhoc_thm 9 is_const changed";
24.252
24.253 -
24.254 case assoc_calc thy "Orderings.ord_class.less" of
24.255 "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
24.256 -(*--------------------------------------------------------------------vvvvvvvvvv*)
24.257 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
24.258 +if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
24.259
24.260 -val SOME t = parseNEW @{context} "4 < 4";
24.261 +val t = @{term "4 < (4 :: real)"};
24.262 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
24.263 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
24.264 then () else error "adhoc_thm 4 < 4 changed";
24.265 @@ -388,35 +429,30 @@
24.266 case adhoc_thm thy (isa_str, eval_fn) t of
24.267 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
24.268
24.269 -
24.270 -(*--------------------------------------------------------------------vvvvvvvvvv*)
24.271 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
24.272 -val SOME t = parseNEW @{context} "1 + 2";
24.273 +val SOME t = parseNEW @{context} "1 + (2::real)";
24.274 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
24.275 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
24.276 then () else error "adhoc_thm 1 + 2 changed";
24.277
24.278 -(*--------------------------------------------------------------------vvvvvvvvvv*)
24.279 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
24.280 -val SOME t = parseNEW @{context} "6 / -8";
24.281 +val t = @{term "6 / -8 :: real"};
24.282 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
24.283 -if str = "#divide_e6_-8" andalso ThmC_Def.string_of_thm thm = "6 / -8 = -3 / 4"
24.284 -then () else error "adhoc_thm 1 + 2 changed";
24.285 -
24.286 +if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
24.287 +then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
24.288
24.289 case assoc_calc thy "Prog_Expr.ident" of
24.290 "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
24.291 -(*--------------------------------------------------------------------vvvvvvvvvv*)
24.292 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
24.293
24.294 -val SOME t = parseNEW @{context} "3 =!= 3";
24.295 +val t = @{term "3 =!= (3 :: real)"};
24.296 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
24.297 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
24.298 then () else error "adhoc_thm (3 =!= 3) changed";
24.299
24.300 -val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
24.301 +val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
24.302 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
24.303 -if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
24.304 +if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
24.305 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
24.306
24.307 "----------- fun power -------------------------------------------------------------------------";
25.1 --- a/test/Tools/isac/ProgLang/listC.sml Fri May 07 18:12:51 2021 +0200
25.2 +++ b/test/Tools/isac/ProgLang/listC.sml Tue Jun 01 15:41:23 2021 +0200
25.3 @@ -7,6 +7,7 @@
25.4 "-----------------------------------------------------------------------------";
25.5 "table of contents -----------------------------------------------------------";
25.6 "-----------------------------------------------------------------------------";
25.7 +"----------- correct list_erls -----------------------------------------------------------------";
25.8 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
25.9 "--------------------- NTH ---------------------------------------------------";
25.10 "--------------------- Length ------------------------------------------------";
25.11 @@ -14,6 +15,10 @@
25.12 "-----------------------------------------------------------------------------";
25.13 "-----------------------------------------------------------------------------";
25.14
25.15 +"----------- correct list_erls -----------------------------------------------------------------";
25.16 +"----------- correct list_erls -----------------------------------------------------------------";
25.17 +"----------- correct list_erls -----------------------------------------------------------------";
25.18 +
25.19 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
25.20 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
25.21 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
25.22 @@ -50,14 +55,18 @@
25.23 else error "NTH 1 [a,b,c,d,e] = a ..changed";
25.24
25.25 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
25.26 -val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
25.27 - (Const ("List.list.Cons", _) $ Free ("b", _) $
25.28 - (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
25.29 -TermC.atomty t;
25.30 +case TermC.str2term "NTH 3 [a,b,c,d,e]" of
25.31 + Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
25.32 + (Const ("List.list.Cons", _) $ Free ("a", _) $
25.33 + (Const ("List.list.Cons", _) $ Free ("b", _) $
25.34 + (Const ("List.list.Cons", _) $ Free ("c", _) $
25.35 + (Const ("List.list.Cons", _) $ Free ("d", _) $
25.36 + (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
25.37 +| _ => error "ListC.NTH changed";
25.38 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
25.39 TermC.atomty thm;
25.40 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
25.41 -if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then ()
25.42 +if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then ()
25.43 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
25.44
25.45 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
25.46 @@ -95,6 +104,7 @@
25.47
25.48 val t = TermC.str2term "Length [1, 1, 1]";
25.49 val t = eval_prog_expr thy prog_expr t;
25.50 -case t of Free ("3", _) => ()
25.51 +case t of
25.52 + Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => ()
25.53 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";
25.54
26.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Fri May 07 18:12:51 2021 +0200
26.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Tue Jun 01 15:41:23 2021 +0200
26.3 @@ -7,6 +7,8 @@
26.4 "-----------------------------------------------------------------------------------------------";
26.5 "table of contents -----------------------------------------------------------------------------";
26.6 "-----------------------------------------------------------------------------------------------";
26.7 +"-------- fun eval_cancel ----------------------------------------------------------------------";
26.8 +"-------- fun eval_equ -------------------------------------------------------------------------";
26.9 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
26.10 "-------- occurs_in ----------------------------------------------------------------------------";
26.11 "-------- fun eval_occurs_in -------------------------------------------------------------------";
26.12 @@ -14,7 +16,7 @@
26.13 "-------- fun eval_sameFunId -------------------------------------------------------------------";
26.14 "-------- fun eval_filter_sameFunId ------------------------------------------------------------";
26.15 "-------- fun eval_boollist2sum ----------------------------------------------------------------";
26.16 -"-------- fun eval_binop -----------------------------------------------------------------------";
26.17 +"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
26.18 "-------- fun matchsub -------------------------------------------------------------------------";
26.19 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
26.20 "-----------------------------------------------------------------------------------------------";
26.21 @@ -22,6 +24,68 @@
26.22 "-----------------------------------------------------------------------------------------------";
26.23
26.24
26.25 +"-------- fun eval_cancel ----------------------------------------------------------------------";
26.26 +"-------- fun eval_cancel ----------------------------------------------------------------------";
26.27 +"-------- fun eval_cancel ----------------------------------------------------------------------";
26.28 +val t = @{term "3 / 2 :: real"};
26.29 +val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t ""
26.30 +
26.31 +val t = @{term "6 / 4 :: real"};
26.32 +case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
26.33 + SOME ("cancel_6_4", t') =>
26.34 + if UnparseC.term t' = "6 / 4 = 3 / 2" then ()
26.35 + else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1"
26.36 +| _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2";
26.37 +
26.38 +val t = @{term "- 6 / 4 :: real"};
26.39 +case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
26.40 + SOME ("cancel_~6_4", t') =>
26.41 + if UnparseC.term t' = "- 6 / 4 = - 3 / 2" then ()
26.42 + else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1"
26.43 +| _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2";
26.44 +
26.45 +val t = @{term "6 / - 4 :: real"};
26.46 +case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
26.47 + SOME ("cancel_6_~4", t') =>
26.48 + if UnparseC.term t' = "6 / - 4 = - 3 / 2" then ()
26.49 + else error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 1"
26.50 +| _ => error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 2";
26.51 +
26.52 +val t = @{term "- 6 /- 4 :: real"};
26.53 +case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
26.54 + SOME ("cancel_~6_~4", t') =>
26.55 + if UnparseC.term t' = "- 6 / - 4 = 3 / 2" then ()
26.56 + else error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 1"
26.57 +| _ => error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 2";
26.58 +
26.59 +val t = @{term "- (6 / 4) :: real"};
26.60 +val NONE = eval_cancel "adhoc_thm_cancel" "Rings.divide_class.divide" t "";
26.61 +
26.62 +
26.63 +"-------- fun eval_equ -------------------------------------------------------------------------";
26.64 +"-------- fun eval_equ -------------------------------------------------------------------------";
26.65 +"-------- fun eval_equ -------------------------------------------------------------------------";
26.66 +eval_equ: string -> string -> term -> 'a -> (string * term) option;
26.67 +
26.68 +case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (2::real)"} "" of
26.69 +SOME
26.70 + ("#less_1_2",
26.71 + Const ("HOL.Trueprop", _) $
26.72 + (Const ("HOL.eq", _) $
26.73 + (Const ("Orderings.ord_class.less", _) $ Const ("Groups.one_class.one", _) $
26.74 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) $
26.75 + Const ("HOL.True", _))) => ()
26.76 +| _ => error "eval_equ 1 < 2 CHANGED";
26.77 +
26.78 +case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (1::real)"} "" of
26.79 +SOME
26.80 + ("#less_1_1",
26.81 + Const ("HOL.Trueprop", _) $
26.82 + (Const ("HOL.eq", _) $ (Const ("Orderings.ord_class.less", _) $ Const ("Groups.one_class.one", _) $ Const ("Groups.one_class.one", _)) $
26.83 + Const ("HOL.False", _))) => ()
26.84 +| _ => error "eval_equ 1 < 1 CHANGED";
26.85 +
26.86 +
26.87 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
26.88 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
26.89 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
26.90 @@ -48,12 +112,7 @@
26.91 "-------- occurs_in ----------------------------------------------------------------------------";
26.92 "-------- occurs_in ----------------------------------------------------------------------------";
26.93 "-------- occurs_in ----------------------------------------------------------------------------";
26.94 -(*=========================================================================*)
26.95 -fun str2t str = (Thm.term_of o the o (TermC.parse thy)) str;
26.96 -fun term2s t = UnparseC.term_in_thy thy t;
26.97 -(*=========================================================================*)
26.98 -
26.99 -val t = str2t "x";
26.100 +val t = @{term "x::real"};
26.101 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
26.102
26.103 val t = TermC.str2term "x occurs_in x";
26.104 @@ -62,19 +121,19 @@
26.105 else error "x occurs_in x = True ..changed";
26.106
26.107 "------- some_occur_in";
26.108 -some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");
26.109 -val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \
26.110 - \-1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
26.111 +if some_occur_in [@{term "c::real"}, @{term "c_2::real"}] @{term "a + b + c::real"} then ()
26.112 +else error "";
26.113 +
26.114 +val t = @{term "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};
26.115 +val SOME (str, t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
26.116 +if UnparseC.term t' =
26.117 + "some_of [c, c_2, c_3,\n c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 =\nTrue" then ()
26.118 +else error "atools.sml: some_occur_in true";
26.119 +
26.120 +val t = @{term "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};
26.121 val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
26.122 if UnparseC.term t' =
26.123 - "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 =\nTrue" then ()
26.124 -else error "atools.sml: some_occur_in true";
26.125 -
26.126 -val t = str2t "some_of [c_3, c_4] occur_in \
26.127 - \-1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
26.128 -val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
26.129 -if UnparseC.term t' =
26.130 - "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then ()
26.131 + "some_of [c_3, c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then ()
26.132 else error "atools.sml: some_occur_in false";
26.133
26.134
26.135 @@ -174,35 +233,34 @@
26.136 "---------fun eval_sameFunId -------------------------------------------------------------------";
26.137 "---------fun eval_sameFunId -------------------------------------------------------------------";
26.138 "---------fun eval_sameFunId -------------------------------------------------------------------";
26.139 -val t = str2t "M_b L"; TermC.atomty t;
26.140 -val t as f1 $ _ = str2t "M_b L";
26.141 -val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2t "M_b x = c + L*x";
26.142 +val t = @{term "M_b L"}; TermC.atomty t;
26.143 +val t as f1 $ _ = @{term "M_b L"};
26.144 +val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
26.145 f1 = f2 (*true*);
26.146 val (p as Const ("Prog_Expr.sameFunId",_) $
26.147 (f1 $ _) $
26.148 (Const ("HOL.eq", _) $ (f2 $ _) $ _)) =
26.149 - str2t "sameFunId (M_b L) (M_b x = c + L*x)";
26.150 + @{term "sameFunId (M_b L) (M_b x = c + L*x)"};
26.151 f1 = f2 (*true*);
26.152 eval_sameFunId "" "Prog_Expr.sameFunId"
26.153 - (str2t "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
26.154 + (@{term "sameFunId (M_b L) (M_b x = c + L*x)"})""(*true*);
26.155 eval_sameFunId "" "Prog_Expr.sameFunId"
26.156 - (str2t "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
26.157 + (@{term "sameFunId (M_b L) ( y' x = c + L*x)"})""(*false*);
26.158 eval_sameFunId "" "Prog_Expr.sameFunId"
26.159 - (str2t "sameFunId (M_b L) ( y x = c + L*x)")""(*false*);
26.160 + (@{term "sameFunId (M_b L) ( y x = c + L*x)"})""(*false*);
26.161 eval_sameFunId "" "Prog_Expr.sameFunId"
26.162 - (str2t "sameFunId ( y L) (M_b x = c + L*x)")""(*false*);
26.163 + (@{term "sameFunId ( y L) (M_b x = c + L*x)"})""(*false*);
26.164 eval_sameFunId "" "Prog_Expr.sameFunId"
26.165 - (str2t "sameFunId ( y L) ( y x = c + L*x)")""(*true*);
26.166 + (@{term "sameFunId ( y L) ( y x = c + L*x)"})""(*true*);
26.167
26.168
26.169 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
26.170 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
26.171 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
26.172 -val flhs as (fid $ _) = str2t "y' L";
26.173 -val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
26.174 +val flhs as (fid $ _) = @{term "y' L"};
26.175 +val fs = @{term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
26.176 val (p as Const ("Prog_Expr.filter_sameFunId",_) $ (fid $ _) $ fs) =
26.177 - str2t "filter_sameFunId (y' L) \
26.178 - \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
26.179 + @{term "filter_sameFunId (y' L) [M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
26.180 val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";
26.181 if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
26.182 else error "atools.slm diff.behav. in filter_sameFunId";
26.183 @@ -214,18 +272,27 @@
26.184 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
26.185 | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
26.186 "----------- \<up> redefined due to overwritten identifier -----------";
26.187 -val u_ = str2t "[]";
26.188 -val u_ = str2t "[b1 = k - 2*q]";
26.189 -val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
26.190 +val u_ = @{term "[]"};
26.191 +val u_ = @{term "[b1 = k - 2*q]"};
26.192 +val u_ = @{term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
26.193 val ut_ = isalist2list u_;
26.194 val sum_ = map lhs ut_;
26.195 val t = list2sum sum_;
26.196 UnparseC.term t;
26.197
26.198 -val t = str2t "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
26.199 -
26.200 -val p as Const ("Prog_Expr.boollist2sum", _) $ (Const ("List.list.Cons", _) $ _ $ _) = t;
26.201 -
26.202 +val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
26.203 +case t of
26.204 +Const ("Prog_Expr.boollist2sum", _) $
26.205 + (Const ("List.list.Cons", _) $
26.206 + (Const ("HOL.eq", _) $ Free ("b1", _) $ _ ) $
26.207 + (Const ("List.list.Cons", _) $
26.208 + (Const ("HOL.eq", _) $ Free ("b2", _) $ _ ) $
26.209 + (Const ("List.list.Cons", _) $
26.210 + (Const ("HOL.eq", _) $ Free ("b3", _) $ _ ) $
26.211 + (Const ("List.list.Cons", _) $
26.212 + (Const ("HOL.eq", _) $ Free ("b4", _) $ _ ) $
26.213 + Const ("List.list.Nil", _))))) => ()
26.214 +| _ => error "boollist2sum CHANGED";
26.215 val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
26.216 if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
26.217 else error "atools.sml diff.behav. in eval_boollist2sum";
26.218 @@ -233,32 +300,31 @@
26.219 Rewrite.trace_on := false;
26.220 val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
26.221 [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
26.222 -val t = str2t
26.223 - "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
26.224 -case rewrite_set_ thy false srls_ t of SOME _ => ()
26.225 +val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
26.226 +case rewrite_set_ @{theory} false srls_ t of SOME _ => ()
26.227 | _ => error "atools.sml diff.rewrite boollist2sum";
26.228 Rewrite.trace_on := false;
26.229
26.230
26.231 -"---------fun eval_binop -----------------------------------------------------------------------";
26.232 -"---------fun eval_binop -----------------------------------------------------------------------";
26.233 -"---------fun eval_binop -----------------------------------------------------------------------";
26.234 +"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
26.235 +"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
26.236 +"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
26.237 val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
26.238 val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
26.239 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;
26.240 ;
26.241 "~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
26.242 (thy, op_, ef, t);
26.243 -op_ = op0 = true;
26.244 -ef op_ t thy
26.245 -;
26.246 -"~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string),
26.247 - (t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)
26.248 -val (SOME n1, SOME n2) = (numeral t1, numeral t2)
26.249 - val (_, _, Trange) = TermC.dest_binop_typ t0;
26.250 - val res = calcul op0 n1 n2;
26.251 - val rhs = term_of_float Trange res;
26.252 - val prop = HOLogic.Trueprop $ (mk_equality (t, rhs));
26.253 +op_ = op0 = true;val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
26.254 +val t = (Thm.term_of o the o (TermC.parse thy)) "2 * 3";
26.255 +
26.256 + ef op_ t thy;
26.257 +"~~~~~ fun eval_binop , args:"; val ((thmid : string), (op_: string),
26.258 + (t as (Const (op0, _) $ t1 $ t2)), _) =
26.259 + ("#mult_", op_, t, thy); (* binary . n1.n2 *)
26.260 + (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
26.261 + val res = Eval.calcul op0 (t1, t2);
26.262 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
26.263 val SOME (thmid, tm) = SOME ("#: " ^ UnparseC.term prop, prop)
26.264 ;
26.265 if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
26.266 @@ -291,5 +357,5 @@
26.267 if UnparseC.term (or2list t) = "[x = 3]" then ()
26.268 else error "or2list changed";
26.269 val t = (TermC.str2term "x=3 | x=-3 | x=0");
26.270 -if UnparseC.term (or2list t) = "[x = 3, x = -3, x = 0]" then ()
26.271 +if UnparseC.term (or2list t) = "[x = 3, x = - 3, x = 0]" then ()
26.272 else error "HOL.eq ? HOL.disj ? changed";
27.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri May 07 18:12:51 2021 +0200
27.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Jun 01 15:41:23 2021 +0200
27.3 @@ -50,35 +50,37 @@
27.4 and find out, which ML_file or *.thy causes an error (might be ONLY one).
27.5 Also backup files (#* ) recognised by jEdit cause this trouble *)
27.6 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
27.7 - "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
27.8 +(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*)
27.9 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
27.10 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
27.11 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
27.12 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
27.13 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
27.14 -(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
27.15 +(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*)
27.16 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
27.17 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
27.18 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
27.19 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
27.20 ADDTESTS/------------------------------------------- see end of tests *)
27.21 -(*/--- these work directly from Pure, but create problems here ..
27.22 +(*/~~~ these work directly from Pure, but create problems here ..
27.23 "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
27.24 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
27.25 "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
27.26 "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
27.27 "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
27.28 - \--- .. these work independently, but create problems here *)
27.29 + \~~~ .. these work independently, but create problems here *)
27.30 (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
27.31 (**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
27.32 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
27.33 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
27.34 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
27.35 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
27.36 +(** )
27.37 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
27.38 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
27.39 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
27.40 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
27.41 +( **)
27.42
27.43 begin
27.44
27.45 @@ -185,19 +187,20 @@
27.46 ML_file "BaseDefinitions/calcelems.sml"
27.47 ML_file "BaseDefinitions/termC.sml"
27.48 ML_file "BaseDefinitions/substitution.sml"
27.49 - ML_file "BaseDefinitions/contextC.sml"
27.50 +(** )ML_file "BaseDefinitions/contextC.sml"( *loops with eliminate ThmC.numerals_to_Free*)
27.51 ML_file "BaseDefinitions/environment.sml"
27.52 - ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
27.53 +(** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
27.54 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
27.55 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
27.56
27.57 + ML_file "ProgLang/calculate.sml"
27.58 ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
27.59 ML_file "ProgLang/listC.sml"
27.60 ML_file "ProgLang/prog_expr.sml"
27.61 ML_file "ProgLang/program.sml"
27.62 ML_file "ProgLang/prog_tac.sml"
27.63 ML_file "ProgLang/tactical.sml"
27.64 - ML_file "ProgLang/auto_prog.sml"
27.65 +(** )ML_file "ProgLang/auto_prog.sml"( *loops with eliminate ThmC.numerals_to_Free*)
27.66 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
27.67 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
27.68
27.69 @@ -227,6 +230,15 @@
27.70 subsection \<open>further functionality alongside batch build sequence\<close>
27.71 ML_file "MathEngBasic/thmC.sml"
27.72 ML_file "MathEngBasic/rewrite.sml"
27.73 +ML \<open>
27.74 +\<close> ML \<open>
27.75 +\<close> ML \<open>
27.76 +\<close> ML \<open>
27.77 +\<close> ML \<open>
27.78 +\<close> ML \<open>
27.79 +\<close> ML \<open>
27.80 +\<close> ML \<open>
27.81 +\<close>
27.82 ML_file "MathEngBasic/tactic.sml"
27.83 ML_file "MathEngBasic/ctree.sml"
27.84 ML_file "MathEngBasic/calculation.sml"
27.85 @@ -253,12 +265,14 @@
27.86 ML_file "Interpret/lucas-interpreter.sml"
27.87 ML_file "Interpret/step-solve.sml"
27.88
27.89 - ML_file "MathEngine/me-misc.sml"
27.90 +ML_file "MathEngine/me-misc.sml"
27.91 ML_file "MathEngine/fetch-tactics.sml"
27.92 - ML_file "MathEngine/solve.sml"
27.93 +(** )ML_file "MathEngine/solve.sml"( *loops with eliminate ThmC.numerals_to_Free*)
27.94 ML_file "MathEngine/step.sml"
27.95 +(** )
27.96 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
27.97 - ML_file "MathEngine/messages.sml"
27.98 + ( *loops with eliminate ThmC.numerals_to_Free*)
27.99 +ML_file "MathEngine/messages.sml"
27.100 ML_file "MathEngine/states.sml"
27.101
27.102 ML_file "BridgeLibisabelle/thy-present.sml"
27.103 @@ -266,7 +280,7 @@
27.104 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
27.105 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
27.106 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
27.107 - ML_file "BridgeLibisabelle/interface.sml"
27.108 +(** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free*)
27.109 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
27.110 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
27.111
27.112 @@ -304,8 +318,8 @@
27.113 ML_file "Knowledge/biegelinie-1.sml"
27.114 (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
27.115 (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
27.116 - ML_file "Knowledge/biegelinie-4.sml"
27.117 - ML_file "Knowledge/algein.sml"
27.118 +(** )ML_file "Knowledge/biegelinie-4.sml"( *loops with eliminate ThmC.numerals_to_Free*)
27.119 +(** )ML_file "Knowledge/algein.sml"( *loops with eliminate ThmC.numerals_to_Free*)
27.120 ML_file "Knowledge/diophanteq.sml"
27.121 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
27.122 ML_file "Knowledge/inssort.sml"
28.1 --- a/test/Tools/isac/Test_Some.thy Fri May 07 18:12:51 2021 +0200
28.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jun 01 15:41:23 2021 +0200
28.3 @@ -48,7 +48,6 @@
28.4 open Rewrite_Ord
28.5 open UnparseC
28.6 \<close>
28.7 -ML_file "BridgeJEdit/parseC.sml"
28.8
28.9 section \<open>code for copy & paste ===============================================================\<close>
28.10 ML \<open>
28.11 @@ -57,7 +56,10 @@
28.12 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
28.13 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
28.14 "xx"
28.15 -^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
28.16 +^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
28.17 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
28.18 +\<close> ML \<open>
28.19 +\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
28.20 (*/------------------- step into XXXXX -----------------------------------------------------\*)
28.21 (*-------------------- stop step into XXXXX -------------------------------------------------*)
28.22 (*\------------------- step into XXXXX -----------------------------------------------------/*)
28.23 @@ -98,6 +100,8 @@
28.24 \<close> ML \<open>
28.25 \<close>
28.26
28.27 +ML_file "ProgLang/listC.sml"
28.28 +
28.29 section \<open>===================================================================================\<close>
28.30 ML \<open>
28.31 \<close> ML \<open>
28.32 @@ -105,6 +109,1317 @@
28.33 \<close> ML \<open>
28.34 \<close>
28.35
28.36 +section \<open>============== check test/../ "Knowledge/poly.sml" ===============================\<close>
28.37 +ML \<open>
28.38 +\<close> ML \<open>
28.39 +(* testexamples for Poly, polynomials
28.40 + author: Matthias Goldgruber 2003
28.41 + (c) due to copyright terms
28.42 +
28.43 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
28.44 + 10 20 30 40 50 60 70 80
28.45 +LEGEND:
28.46 +WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
28.47 + examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
28.48 +*)
28.49 +
28.50 +"--------------------------------------------------------";
28.51 +"--------------------------------------------------------";
28.52 +"table of contents --------------------------------------";
28.53 +"--------------------------------------------------------";
28.54 +"----------- fun is_polyexp --------------------------------------------------------------------";
28.55 +"----------- fun has_degree_in -----------------------------------------------------------------";
28.56 +"----------- fun mono_deg_in -------------------------------------------------------------------";
28.57 +"----------- fun mono_deg_in -------------------------------------------------------------------";
28.58 +"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
28.59 +"-------- investigate (new 2002) uniary minus -----------";
28.60 +"-------- check make_polynomial with simple terms -------";
28.61 +"-------- fun is_multUnordered --------------------------";
28.62 +"-------- examples from textbook Schalk I ---------------";
28.63 +"-------- check pbl 'polynomial simplification' --------";
28.64 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
28.65 +"-------- interSteps for Schalk 299a --------------------";
28.66 +"-------- norm_Poly NOT COMPLETE ------------------------";
28.67 +"-------- ord_make_polynomial ---------------------------";
28.68 +"--------------------------------------------------------";
28.69 +"--------------------------------------------------------";
28.70 +"--------------------------------------------------------";
28.71 +
28.72 +
28.73 +\<close> ML \<open>
28.74 +"----------- fun is_polyexp --------------------------------------------------------------------";
28.75 +"----------- fun is_polyexp --------------------------------------------------------------------";
28.76 +"----------- fun is_polyexp --------------------------------------------------------------------";
28.77 +val thy = @{theory Partial_Fractions};
28.78 +val ctxt = Proof_Context.init_global thy;
28.79 +
28.80 +val t = (the o (parseNEW ctxt)) "x / x";
28.81 +if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
28.82 +
28.83 +val t = (the o (parseNEW ctxt)) "-1 * A * 3";
28.84 +if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
28.85 +
28.86 +val t = (the o (parseNEW ctxt)) "-1 * AA * 3";
28.87 +if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
28.88 +
28.89 +\<close> ML \<open>
28.90 +"----------- fun has_degree_in -----------------------------------------------------------------";
28.91 +"----------- fun has_degree_in -----------------------------------------------------------------";
28.92 +"----------- fun has_degree_in -----------------------------------------------------------------";
28.93 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.94 +val t = (Thm.term_of o the o (TermC.parse thy)) "1";
28.95 +if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
28.96 +
28.97 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.98 +val t = (Thm.term_of o the o (TermC.parse thy)) "1";
28.99 +if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
28.100 +
28.101 +(*----------*)
28.102 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.103 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
28.104 +if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
28.105 +
28.106 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.107 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
28.108 +if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
28.109 +
28.110 +(*----------*)
28.111 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.112 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
28.113 +if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
28.114 +
28.115 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.116 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
28.117 +if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
28.118 +
28.119 +(*----------*)
28.120 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.121 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
28.122 +if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
28.123 +
28.124 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.125 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
28.126 +if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
28.127 +
28.128 +(*----------*)
28.129 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.130 +val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
28.131 +if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
28.132 +
28.133 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.134 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
28.135 +if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
28.136 +
28.137 +(*----------*)
28.138 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.139 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
28.140 +if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
28.141 +
28.142 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.143 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
28.144 +if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
28.145 +
28.146 +(*----------*)
28.147 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.148 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
28.149 +if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
28.150 +
28.151 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.152 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
28.153 +if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
28.154 +
28.155 +(*----------*)
28.156 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.157 +val t = (Thm.term_of o the o (TermC.parse thy)) "x";
28.158 +if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
28.159 +
28.160 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.161 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.162 +if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
28.163 +
28.164 +(*----------*)
28.165 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.166 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
28.167 +if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
28.168 +
28.169 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.170 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
28.171 +if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
28.172 +
28.173 +\<close> ML \<open>
28.174 +"----------- fun mono_deg_in -------------------------------------------------------------------";
28.175 +"----------- fun mono_deg_in -------------------------------------------------------------------";
28.176 +"----------- fun mono_deg_in -------------------------------------------------------------------";
28.177 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
28.178 +
28.179 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
28.180 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
28.181 +
28.182 +val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
28.183 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
28.184 +
28.185 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
28.186 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
28.187 +
28.188 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
28.189 +if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
28.190 +
28.191 +val t = (Thm.term_of o the o (TermC.parse thy)) "x";
28.192 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
28.193 +
28.194 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
28.195 +if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
28.196 +
28.197 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
28.198 +if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
28.199 +
28.200 +(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
28.201 +val thy = @{theory Partial_Fractions}
28.202 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.203 +
28.204 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
28.205 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
28.206 +
28.207 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
28.208 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
28.209 +
28.210 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
28.211 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
28.212 +
28.213 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
28.214 +if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
28.215 +
28.216 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
28.217 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
28.218 +
28.219 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
28.220 +if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
28.221 +
28.222 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
28.223 +if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
28.224 +
28.225 +\<close> ML \<open>
28.226 +"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
28.227 +"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
28.228 +"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
28.229 +val thy = @{theory Partial_Fractions}
28.230 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
28.231 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
28.232 +
28.233 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
28.234 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
28.235 +
28.236 +\<close> ML \<open>
28.237 +"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
28.238 +"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
28.239 +"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
28.240 +val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
28.241 +val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
28.242 +if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
28.243 + andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
28.244 +then () else error "eval_is_expanded_in x ..changed";
28.245 +
28.246 +\<close> ML \<open>
28.247 +val thy = @{theory Partial_Fractions}
28.248 +val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
28.249 +val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
28.250 +if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
28.251 + andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
28.252 +then () else error "eval_is_expanded_in AA ..changed";
28.253 +
28.254 +
28.255 +\<close> ML \<open>
28.256 +val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";
28.257 +val SOME (id, t') = eval_is_poly_in 0 0 t 0;
28.258 +if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
28.259 + andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
28.260 +then () else error "is_poly_in x ..changed";
28.261 +
28.262 +val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
28.263 +val SOME (id, t') = eval_is_poly_in 0 0 t 0;
28.264 +if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
28.265 + andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
28.266 +then () else error "is_poly_in AA ..changed";
28.267 +
28.268 +
28.269 +val thy = @{theory Partial_Fractions}
28.270 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
28.271 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
28.272 +
28.273 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
28.274 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
28.275 +
28.276 +\<close> ML \<open>
28.277 +"-------- investigate (new 2002) uniary minus -----------";
28.278 +"-------- investigate (new 2002) uniary minus -----------";
28.279 +"-------- investigate (new 2002) uniary minus -----------";
28.280 +(*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)
28.281 +val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
28.282 +TermC.atomty t;
28.283 +(*
28.284 +*** Const (HOL.Trueprop, bool => prop)
28.285 +*** . Const (HOL.eq, real => real => bool)
28.286 +*** . . Const (Groups.minus_class.minus, real => real => real)
28.287 +*** . . . Const (Groups.zero_class.zero, real)
28.288 +*** . . . Var ((x, 0), real)
28.289 +*** . . Const (Groups.uminus_class.uminus, real => real)
28.290 +*** . . . Var ((x, 0), real)
28.291 +*)
28.292 +case t of
28.293 + Const ("HOL.Trueprop", _) $
28.294 + (Const ("HOL.eq", _) $
28.295 + (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $
28.296 + Var (("x", 0), _)) $
28.297 + (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
28.298 +| _ => error "internal representation of \"0 - ?x = - ?x\" changed";
28.299 +
28.300 +\<close> ML \<open>
28.301 +(*----------------------------------- vvvvv -------------------------------------------*)
28.302 +val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
28.303 +TermC.atomty t;
28.304 +(*
28.305 +***
28.306 +*** Free (-1, real)
28.307 +***
28.308 +*)
28.309 +\<close> ML \<open>
28.310 +case t of
28.311 + Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()
28.312 +| _ => error "internal representation of \"- 1\" changed";
28.313 +
28.314 +\<close> ML \<open>
28.315 +"======= these external values all have the same internal representation";
28.316 +(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
28.317 +(*----------------------------------- vvvvv -------------------------------------------*)
28.318 +val t = (Thm.term_of o the o (TermC.parse thy)) "-x";
28.319 +TermC.atomty t;
28.320 +(**** -------------
28.321 +*** Free ( -x, real)*)
28.322 +case t of
28.323 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
28.324 +| _ => error "internal representation of \"-x\" changed";
28.325 +\<close> ML \<open>
28.326 +(*----------------------------------- vvvvv -------------------------------------------*)
28.327 +val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
28.328 +TermC.atomty t;
28.329 +(**** -------------
28.330 +*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
28.331 +case t of
28.332 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
28.333 +| _ => error "internal representation of \"- x\" changed";
28.334 +\<close> ML \<open>
28.335 +(*----------------------------------- vvvvvv ------------------------------------------*)
28.336 +val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
28.337 +TermC.atomty t;
28.338 +(**** -------------
28.339 +*** Free ( -x, real)*)
28.340 +case t of
28.341 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
28.342 +| _ => error "internal representation of \"-(x)\" changed";
28.343 +
28.344 +\<close> ML \<open> (*\\---------------------- original test code --------------------------------------//*)
28.345 +\<close> ML \<open>
28.346 +\<close> ML \<open> (* \<longrightarrow> Poly.thy*)
28.347 +\<close> ML \<open> (* \<longrightarrow> Poly.thy*)
28.348 +\<close> ML \<open>
28.349 +if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
28.350 +else error "lexicographic order CHANGED";
28.351 +\<close> ML \<open>
28.352 +@{term 123}
28.353 +\<close> ML \<open>
28.354 +\<close> ML \<open>
28.355 +\<close> ML \<open> (* \<longrightarrow> Poly.thy*)
28.356 +\<close> ML \<open>
28.357 +"----------- fun sort_varList ------------------------------------------------------------------";
28.358 +"----------- fun sort_varList ------------------------------------------------------------------";
28.359 +"----------- fun sort_varList ------------------------------------------------------------------";
28.360 +\<close> ML \<open>
28.361 + sort_varList [@{term "a"}, @{term "3"}];
28.362 +\<close> ML \<open>
28.363 +"~~~~~ val sort_varList , args:"; val (t) = [@{term "a"}, @{term "3"}];
28.364 +\<close> ML \<open>
28.365 +sort_varList: term list -> term list;
28.366 +\<close> ML \<open>
28.367 +\<close> ML \<open>
28.368 +\<close> ML \<open>
28.369 +\<close> ML \<open>
28.370 +\<close> ML \<open>
28.371 +\<close> ML \<open> (* \<longrightarrow> Poly.thy*)
28.372 +\<close> ML \<open>
28.373 +"----------- fun sort_variables ----------------------------------------------------------------";
28.374 +"----------- fun sort_variables ----------------------------------------------------------------";
28.375 +"----------- fun sort_variables ----------------------------------------------------------------";
28.376 +\<close> ML \<open>
28.377 +sort_variables: term -> term;
28.378 +\<close> ML \<open>
28.379 + val t' = sort_variables @{term "3 * b + a * 2"};
28.380 +\<close> ML \<open>
28.381 +UnparseC.term t' = "(3::'a) * b + (2::'a) * a"
28.382 +\<close> ML \<open>
28.383 +"~~~~~ fun sort_variables , args:"; val (t) = (@{term "3 * b + a * 2"});
28.384 +\<close> ML \<open>
28.385 + val ll = map monom2list (poly2list t);
28.386 +\<close> ML \<open>
28.387 +(*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
28.388 +(*+*)val [
28.389 +(*+*) [Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) ,(*!*) Free ("b", _)],
28.390 +(*+*) [Free ("a", _) ,(*!*) Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _))]
28.391 +(*+*) ] = map monom2list (poly2list t);
28.392 +\<close> ML \<open>
28.393 + val lls = map sort_varList ll;
28.394 +\<close> ML \<open>
28.395 +(*+*)case map sort_varList ll of
28.396 +(*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
28.397 +(*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
28.398 +(*+*) ] => ()
28.399 +(*+*)| _ => error "map sort_varList CHANGED";
28.400 +\<close> ML \<open>
28.401 + val T = type_of t;
28.402 + val ls = map (create_monom T) lls;
28.403 +\<close> ML \<open>
28.404 +(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
28.405 +(*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
28.406 +\<close> ML \<open>
28.407 +(*+*)case map (create_monom T) lls of
28.408 +(*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
28.409 +(*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
28.410 +(*+*) ] => ()
28.411 +(*+*)| _ => error "map (create_monom T) CHANGED";
28.412 +\<close> ML \<open>
28.413 + val xxx = (*in*) create_polynom T ls (*end*);
28.414 +\<close> ML \<open>
28.415 +(*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
28.416 +(*+*)else error "create_polynom CHANGED";
28.417 +(* done by rewriting> 2 * a + 3 * b ? *)
28.418 +\<close> ML \<open>
28.419 +\<close> ML \<open>
28.420 +\<close> ML \<open>
28.421 +\<close> ML \<open>
28.422 +\<close> ML \<open>
28.423 +\<close> ML \<open>
28.424 +\<close> ML \<open>
28.425 +\<close> ML \<open>
28.426 +\<close> ML \<open>
28.427 +\<close> ML \<open>
28.428 +\<close> ML \<open>
28.429 +
28.430 +\<close> ML \<open> (*//---------------------- original test code --------------------------------------\\*)
28.431 +"-------- check make_polynomial with simple terms -------";
28.432 +"-------- check make_polynomial with simple terms -------";
28.433 +"-------- check make_polynomial with simple terms -------";
28.434 +"----- check 1 ---";
28.435 +val t = TermC.str2term "2*3*a";
28.436 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
28.437 +\<close> ML \<open>
28.438 +UnparseC.term t = "a * 6" (*<<<<<<<<<<<<<<<<<<<----------------------------TODOO correct*)
28.439 +\<close> ML \<open>
28.440 +if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
28.441 +
28.442 +\<close> ML \<open>
28.443 +"----- check 2 ---";
28.444 +val t = TermC.str2term "2*a + 3*a";
28.445 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
28.446 +if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
28.447 +
28.448 +\<close> ML \<open>
28.449 +"----- check 3 ---";
28.450 +val t = TermC.str2term "2*a + 3*a + 3*a";
28.451 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
28.452 +if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
28.453 +
28.454 +\<close> ML \<open>
28.455 +Rewrite.trace_on := true;
28.456 +\<close> ML \<open> (*loops THIS IS THE SIMPLEST EXAMPLE*)
28.457 +"----- check 4 ---";
28.458 +val t = TermC.str2term "3*a - 2*a";
28.459 +\<close> text \<open> (*loops THIS IS THE SIMPLEST EXAMPLE*)
28.460 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
28.461 +\<close> text \<open>
28.462 +if UnparseC.term t = "a" then () else error "check make_polynomial 4";
28.463 +\<close> ML \<open>
28.464 +Rewrite.trace_on := false;
28.465 +\<close> ML \<open>
28.466 +
28.467 +\<close> text \<open> (*loops*)
28.468 +"----- check 5 ---";
28.469 +val t = TermC.str2term "4*(3*a - 2*a)";
28.470 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
28.471 +if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
28.472 +
28.473 +\<close> text \<open> (*loops*)
28.474 +"----- check 6 ---";
28.475 +val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
28.476 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
28.477 +if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
28.478 +
28.479 +\<close> ML \<open>
28.480 +\<close> ML \<open>
28.481 +"-------- fun is_multUnordered --------------------------";
28.482 +"-------- fun is_multUnordered --------------------------";
28.483 +"-------- fun is_multUnordered --------------------------";
28.484 +\<close> ML \<open>
28.485 +val thy = @{theory "Isac_Knowledge"};
28.486 +"===== works for a simple example, see rewrite.sml -- fun app_rev ===";
28.487 +val t = TermC.str2term "x \<up> 2 * x";
28.488 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
28.489 +\<close> ML \<open>
28.490 +if UnparseC.term t' = "x * x \<up> 2" then ()
28.491 +else error "poly.sml Poly.is_multUnordered doesn't work";
28.492 +
28.493 +\<close> ML \<open>
28.494 +(* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
28.495 +### rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +
28.496 + (-48 * x \<up> 4 + 8))
28.497 +###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
28.498 +####### try calc: Poly.is_multUnordered'
28.499 +======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
28.500 +*)
28.501 +val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))";
28.502 +
28.503 +\<close> ML \<open>
28.504 +"----- is_multUnordered ---";
28.505 +val tsort = sort_variables t;
28.506 +UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n-1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n-1 * (-1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";
28.507 +is_polyexp t;
28.508 +tsort = t;
28.509 +is_polyexp t andalso not (t = sort_variables t);
28.510 +\<close> text \<open> (*false*)
28.511 +if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
28.512 +
28.513 +\<close> ML \<open>
28.514 +"----- eval_is_multUnordered ---";
28.515 +val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))) is_multUnordered";
28.516 +case eval_is_multUnordered "testid" "" tm thy of
28.517 + SOME (_, Const ("HOL.Trueprop", _) $
28.518 + (Const ("HOL.eq", _) $
28.519 + (Const ("Poly.is_multUnordered", _) $ _) $
28.520 + Const ("HOL.True", _))) => ()
28.521 + | _ => error "poly.sml diff. eval_is_multUnordered";
28.522 +
28.523 +\<close> text \<open> (*NONE*)
28.524 +"----- rewrite_set_ STILL DIDN'T WORK";
28.525 +val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
28.526 +UnparseC.term t;
28.527 +
28.528 +\<close> ML \<open>
28.529 +"-------- examples from textbook Schalk I ---------------";
28.530 +"-------- examples from textbook Schalk I ---------------";
28.531 +"-------- examples from textbook Schalk I ---------------";
28.532 +"-----SPB Schalk I p.63 No.267b ---";
28.533 +(*associate poly* )
28.534 +val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
28.535 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.536 +if (UnparseC.term t) = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 + -8 * x \<up> 9"
28.537 +then () else error "poly.sml: diff.behav. in make_polynomial 1";
28.538 +
28.539 +"-----SPB Schalk I p.63 No.275b ---";
28.540 +val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
28.541 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.542 +if (UnparseC.term t) = ("3 * x \<up> 4 + -2 * x \<up> 3 * y + -5 * x \<up> 2 * y \<up> 2 + " ^
28.543 + "4 * x * y \<up> 3 +\n-2 * y \<up> 4")
28.544 +then () else error "poly.sml: diff.behav. in make_polynomial 2";
28.545 +
28.546 +"-----SPB Schalk I p.63 No.279b ---";
28.547 +val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";
28.548 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.549 +if (UnparseC.term t) =
28.550 + ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x \<up> 2 +\n" ^
28.551 + "-1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n-1 * a * x \<up> 3 +\n" ^
28.552 + "-1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n-1 * b * x \<up> 3 +\n" ^
28.553 + "c * d * x \<up> 2 +\n-1 * c * x \<up> 3 +\n-1 * d * x \<up> 3 +\nx \<up> 4")
28.554 +then () else error "poly.sml: diff.behav. in make_polynomial 3";
28.555 +( *associate poly*)
28.556 +
28.557 +\<close> text \<open> (*loops*)
28.558 +"-----SPB Schalk I p.63 No.291 ---";
28.559 +val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
28.560 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.561 +if (UnparseC.term t) = "50 + -770 * x + 4520 * x \<up> 2 + -16320 * x \<up> 3 + -26880 * x \<up> 4"
28.562 +then () else error "poly.sml: diff.behav. in make_polynomial 4";
28.563 +
28.564 +\<close> ML \<open>
28.565 +(*associate poly* )
28.566 +"-----SPB Schalk I p.64 No.295c ---";
28.567 +val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
28.568 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.569 +if (UnparseC.term t) = ("169 * a \<up> 8 * b \<up> 18 * c \<up> 2 + -312 * a \<up> 7 * b \<up> 15 * c \<up> 10" ^
28.570 + " +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18")
28.571 +then ()else error "poly.sml: diff.behav. in make_polynomial 5";
28.572 +( *associate poly*)
28.573 +
28.574 +\<close> text \<open> (*loops*)
28.575 +"-----SPB Schalk I p.64 No.299a ---";
28.576 +val t = TermC.str2term "(x - y)*(x + y)";
28.577 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.578 +if (UnparseC.term t) = "x \<up> 2 + -1 * y \<up> 2"
28.579 +then () else error "poly.sml: diff.behav. in make_polynomial 6";
28.580 +
28.581 +\<close> text \<open> (*loops*)
28.582 +"-----SPB Schalk I p.64 No.300c ---";
28.583 +val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
28.584 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.585 +if (UnparseC.term t) = "-1 + 9 * x \<up> 4 * y \<up> 2"
28.586 +then () else error "poly.sml: diff.behav. in make_polynomial 7";
28.587 +
28.588 +\<close> text \<open> (*loops*)
28.589 +"-----SPB Schalk I p.64 No.302 ---";
28.590 +val t = TermC.str2term
28.591 + "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
28.592 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
28.593 +if UnparseC.term t = "0"
28.594 +then () else error "poly.sml: diff.behav. in make_polynomial 8";
28.595 +(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
28.596 +
28.597 +\<close> text \<open> (*loops*)
28.598 +"-----SPB Schalk I p.64 No.306a ---";
28.599 +val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
28.600 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.601 +if (UnparseC.term t) = "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8" then ()
28.602 +else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * -2 * x \<up> 4 = -2 * x \<up> 4";
28.603 +
28.604 +\<close> text \<open> (*loops*)
28.605 +(*WN071729 when reducing "rls reduce_012_" for Schaerding,
28.606 +the above resulted in the term below ... but reduces from then correctly*)
28.607 +val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
28.608 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.609 +if (UnparseC.term t) = "1 + -2 * x \<up> 4 + x \<up> 8"
28.610 +then () else error "poly.sml: diff.behav. in make_polynomial 9b";
28.611 +
28.612 +\<close> text \<open> (*loops*)
28.613 +"-----SPB Schalk I p.64 No.296a ---";
28.614 +val t = TermC.str2term "(x - a) \<up> 3";
28.615 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.616 +if (UnparseC.term t) = "-1 * a \<up> 3 + 3 * a \<up> 2 * x + -3 * a * x \<up> 2 + x \<up> 3"
28.617 +then () else error "poly.sml: diff.behav. in make_polynomial 10";
28.618 +
28.619 +\<close> text \<open> (*loops*)
28.620 +"-----SPB Schalk I p.64 No.296c ---";
28.621 +val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
28.622 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.623 +if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"
28.624 +then () else error "poly.sml: diff.behav. in make_polynomial 11";
28.625 +
28.626 +\<close> text \<open> (*loops*)
28.627 +"-----SPB Schalk I p.62 No.242c ---";
28.628 +val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
28.629 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.630 +if (UnparseC.term t) = "1"
28.631 +then () else error "poly.sml: diff.behav. in make_polynomial 12";
28.632 +
28.633 +\<close> text \<open> (*loops*)
28.634 +"-----SPB Schalk I p.60 No.209a ---";
28.635 +val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
28.636 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.637 +if UnparseC.term t = "a \<up> 7"
28.638 +then () else error "poly.sml: diff.behav. in make_polynomial 13";
28.639 +
28.640 +\<close> text \<open> (*loops*)
28.641 +"-----SPB Schalk I p.60 No.209d ---";
28.642 +val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
28.643 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.644 +if UnparseC.term t = "d \<up> 3"
28.645 +then () else error "poly.sml: diff.behav. in make_polynomial 14";
28.646 +
28.647 +\<close> text \<open> (*loops*)
28.648 +(*---------------------------------------------------------------------*)
28.649 +(*---------------- ?RL?Bsple bei denen es Probleme gibt----------------*)
28.650 +(*---------------------------------------------------------------------*)
28.651 +"-----Schalk I p.64 No.303 ---";
28.652 +val t = TermC.str2term "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
28.653 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.654 +if UnparseC.term t = "1280 * b \<up> 4"
28.655 +then () else error "poly.sml: diff.behav. in make_polynomial 14b";
28.656 +(* Richtig - aber Binomische Formel wurde nicht verwendet! *)
28.657 +
28.658 +(*--------------------------------------------------------------------*)
28.659 +(*----------------------- Eigene Beispiele ---------------------------*)
28.660 +(*--------------------------------------------------------------------*)
28.661 +\<close> text \<open> (*loops*)
28.662 +"-----SPO ---";
28.663 +val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
28.664 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.665 +if UnparseC.term t = "1" then ()
28.666 +else error "poly.sml: diff.behav. in make_polynomial 15";
28.667 +\<close> ML \<open>
28.668 +"-----SPO ---";
28.669 +val t = TermC.str2term "a + a + a";
28.670 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.671 +if UnparseC.term t = "3 * a" then ()
28.672 +else error "poly.sml: diff.behav. in make_polynomial 16";
28.673 +\<close> ML \<open>
28.674 +"-----SPO ---";
28.675 +val t = TermC.str2term "a + b + b + b";
28.676 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.677 +if UnparseC.term t = "a + 3 * b" then ()
28.678 +else error "poly.sml: diff.behav. in make_polynomial 17";
28.679 +\<close> text \<open> (*loops*)
28.680 +"-----SPO ---";
28.681 +val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
28.682 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.683 +if UnparseC.term t = "a \<up> 2" then ()
28.684 +else error "poly.sml: diff.behav. in make_polynomial 18";
28.685 +\<close> text \<open> (*loops*)
28.686 +"-----SPO ---";
28.687 +val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
28.688 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.689 +if (UnparseC.term t) = "1" then ()
28.690 +else error "poly.sml: diff.behav. in make_polynomial 19";
28.691 +\<close> text \<open> (*loops*)
28.692 +"-----SPO ---";
28.693 +val t = TermC.str2term "b + a - b";
28.694 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.695 +if (UnparseC.term t) = "a" then ()
28.696 +else error "poly.sml: diff.behav. in make_polynomial 20";
28.697 +\<close> ML \<open>
28.698 +"-----SPO ---";
28.699 +val t = TermC.str2term "b * a * a";
28.700 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.701 +if UnparseC.term t = "a \<up> 2 * b" then ()
28.702 +else error "poly.sml: diff.behav. in make_polynomial 21";
28.703 +\<close> ML \<open>
28.704 +"-----SPO ---";
28.705 +val t = TermC.str2term "(a \<up> 2) \<up> 3";
28.706 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.707 +if UnparseC.term t = "a \<up> 6" then ()
28.708 +else error "poly.sml: diff.behav. in make_polynomial 22";
28.709 +"-----SPO ---";
28.710 +val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
28.711 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
28.712 +if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
28.713 +else error "poly.sml: diff.behav. in make_polynomial 23";
28.714 +\<close> text \<open> (*loops*)
28.715 +"-----SPO ---";
28.716 +val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
28.717 +val SOME (t,_) = rewrite_set_ @ {theory} false make_polynomial t; UnparseC.term t;
28.718 +if (UnparseC.term t) = "a \<up> 4" then ()
28.719 +else error "poly.sml: diff.behav. in make_polynomial 24";
28.720 +"-----SPO ---";
28.721 +val t = TermC.str2term "a * b * b \<up> (-1) + a";
28.722 +\<close> text \<open>
28.723 +val SOME (t,_) = rewrite_set_ @ {theory} false make_polynomial t; UnparseC.term t;
28.724 +\<close> text \<open>
28.725 +UnparseC.term t
28.726 +\<close> text \<open>
28.727 +if UnparseC.term t = "2 * a" then ()
28.728 +else error "poly.sml: diff.behav. in make_polynomial 25";
28.729 +\<close> ML \<open>
28.730 +"-----SPO ---";
28.731 +val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
28.732 +\<close> ML \<open>
28.733 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
28.734 +\<close> ML \<open>
28.735 +(*+++*)UnparseC.term t
28.736 +\<close> ML \<open>
28.737 +if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
28.738 +then () else error "poly.sml: diff.behav. in make_polynomial 26";
28.739 +
28.740 +\<close> ML \<open>
28.741 +(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
28.742 +"-----SPO ---";
28.743 +val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
28.744 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
28.745 +if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
28.746 +then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
28.747 +
28.748 +\<close> ML \<open>
28.749 +val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
28.750 +\<close> ML \<open>
28.751 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
28.752 +\<close> ML \<open>
28.753 +if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
28.754 +then () else error "poly.sml: diff.behav. in make_polynomial 28";
28.755 +
28.756 +\<close> ML \<open>
28.757 +"-------- check pbl 'polynomial simplification' --------";
28.758 +"-------- check pbl 'polynomial simplification' --------";
28.759 +"-------- check pbl 'polynomial simplification' --------";
28.760 +val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
28.761 +"-----0 ---";
28.762 +\<close> ML \<open>
28.763 +case Refine.refine fmz ["polynomial", "simplification"] of
28.764 + [M_Match.Matches (["polynomial", "simplification"], _)] => ()
28.765 + | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
28.766 +\<close> ML \<open>
28.767 +(*...if there is an error, then ...*)
28.768 +
28.769 +"-----1 ---";
28.770 +(*default_print_depth 7;*)
28.771 +val pbt = Problem.from_store ["polynomial", "simplification"];
28.772 +(*default_print_depth 3;*)
28.773 +(*if there is ...
28.774 +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
28.775 +... then Rewrite.trace_on:*)
28.776 +
28.777 +"-----2 ---";
28.778 +Rewrite.trace_on := false;
28.779 +M_Match.match_pbl fmz pbt;
28.780 +Rewrite.trace_on := false;
28.781 +(*... if there is no rewrite, then there is something wrong with prls*)
28.782 +
28.783 +"-----3 ---";
28.784 +(*default_print_depth 7;*)
28.785 +val prls = (#prls o Problem.from_store) ["polynomial", "simplification"];
28.786 +(*default_print_depth 3;*)
28.787 +val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
28.788 +val SOME (t',_) = rewrite_set_ thy false prls t;
28.789 +if t' = @{term True} then ()
28.790 +else error "poly.sml: diff.behav. in check pbl 'polynomial..";
28.791 +(*... if this works, but --1-- does still NOT work, check types:*)
28.792 +
28.793 +"-----4 ---";
28.794 +(*show_types:=true;*)
28.795 +(*
28.796 +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
28.797 +val wh = [False "(t_::real => real) (is_polyexp::real)"]
28.798 +...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
28.799 +val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
28.800 +(*show_types:=false;*)
28.801 +
28.802 +
28.803 +\<close> ML \<open>
28.804 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
28.805 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
28.806 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
28.807 +val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
28.808 +val (dI',pI',mI') =
28.809 + ("Poly",["polynomial", "simplification"],
28.810 + ["simplification", "for_polynomials"]);
28.811 +val p = e_pos'; val c = [];
28.812 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
28.813 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)
28.814 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
28.815 +
28.816 +(*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
28.817 +(*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"
28.818 +(*+*)then () else error "No.267b: I_Model.T CHANGED";
28.819 +( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
28.820 +
28.821 +\<close> ML \<open>
28.822 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
28.823 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
28.824 +\<close> ML \<open>
28.825 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
28.826 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
28.827 +\<close> text \<open> (*loops*)
28.828 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
28.829 +
28.830 +\<close> text \<open>
28.831 +(*+++*)f (*= PpcKF (Problem [],.. *)
28.832 +\<close> text \<open>
28.833 +(*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
28.834 +(*+*)then () else error "";
28.835 +
28.836 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
28.837 +
28.838 +\<close> text \<open>
28.839 +(*+*)if f2str f = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n-8 * x \<up> 9"
28.840 +(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";
28.841 +
28.842 +(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
28.843 +
28.844 +
28.845 +
28.846 +\<close> ML \<open>
28.847 +"-------- interSteps for Schalk 299a --------------------";
28.848 +"-------- interSteps for Schalk 299a --------------------";
28.849 +"-------- interSteps for Schalk 299a --------------------";
28.850 +reset_states ();
28.851 +CalcTree
28.852 +[(["Term ((x - y)*(x + (y::real)))", "normalform N"],
28.853 + ("Poly",["polynomial", "simplification"],
28.854 + ["simplification", "for_polynomials"]))];
28.855 +Iterator 1;
28.856 +moveActiveRoot 1;
28.857 +\<close> text \<open> (*loops*)
28.858 +autoCalculate 1 CompleteCalc;
28.859 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
28.860 +
28.861 +\<close> text \<open>
28.862 +interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
28.863 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
28.864 +if existpt' ([1,1], Frm) pt then ()
28.865 +else error "poly.sml: interSteps doesnt work again 1";
28.866 +
28.867 +interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
28.868 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
28.869 +(*============ inhibit exn WN120316 ==============================================
28.870 +if existpt' ([1,1,1], Frm) pt then ()
28.871 +else error "poly.sml: interSteps doesnt work again 2";
28.872 +============ inhibit exn WN120316 ==============================================*)
28.873 +
28.874 +\<close> text \<open> (*loops*)
28.875 +"-------- norm_Poly NOT COMPLETE ------------------------";
28.876 +"-------- norm_Poly NOT COMPLETE ------------------------";
28.877 +"-------- norm_Poly NOT COMPLETE ------------------------";
28.878 +val thy = @ {theory AlgEin};
28.879 +
28.880 +val SOME (f',_) = rewrite_set_ thy false norm_Poly
28.881 +(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
28.882 +if UnparseC.term f' = "L = senkrecht + oben + 2 * 2 * k + 2 * -4 * q"
28.883 +then ((*norm_Poly NOT COMPLETE -- TODO MG*))
28.884 +else error "norm_Poly changed behavior";
28.885 +
28.886 +\<close> ML \<open>
28.887 +"-------- ord_make_polynomial ---------------------------";
28.888 +"-------- ord_make_polynomial ---------------------------";
28.889 +"-------- ord_make_polynomial ---------------------------";
28.890 +val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
28.891 +val t2 = TermC.str2term "3 * a + 3 * b + 2 * b";
28.892 +
28.893 +\<close> ML \<open>
28.894 +if ord_make_polynomial true thy [] (t1, t2) then ()
28.895 +else error "poly.sml: diff.behav. in ord_make_polynomial";
28.896 +
28.897 +\<close> ML \<open>
28.898 +(*WN071202: \<up> why then is there no rewriting ...*)
28.899 +val term = TermC.str2term "2*b + (3*a + 3*b)";
28.900 +\<close> ML \<open>
28.901 +(*+++*)val SOME (t', []) = rewrite_set_ (@{theory "Isac_Knowledge"}) false order_add_mult term
28.902 +\<close> ML \<open>
28.903 +(*+++*)UnparseC.term t' = "a * 3 + (b * 2 + b * 3)";
28.904 +\<close> text \<open>
28.905 +val NONE = rewrite_set_ (@ {theory "Isac_Knowledge"}) false order_add_mult term;
28.906 +
28.907 +(*or why is there no rewriting this way...*)
28.908 +val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
28.909 +val t2 = TermC.str2term "3 * a + (2 * b + 3 * b)";
28.910 +
28.911 +\<close> ML \<open>
28.912 +\<close> ML \<open>
28.913 +\<close>
28.914 +
28.915 +
28.916 +section \<open>===================================================================================\<close>
28.917 +ML \<open>
28.918 +\<close> ML \<open>
28.919 +\<close> ML \<open>
28.920 +\<close> ML \<open>
28.921 +\<close>
28.922 +
28.923 +section \<open>============== check test/../ "MathEngBasic/rewrite.sml" ==========================\<close>
28.924 +ML \<open>
28.925 +\<close> ML \<open>
28.926 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
28.927 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
28.928 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
28.929 +val thy = @{theory "Isac_Knowledge"};
28.930 +val t = @{term "a + b * x = (0 ::real)"};
28.931 +val pat = TermC.parse_patt thy "?l = (?r ::real)";
28.932 +val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
28.933 +val precond = TermC.parse_patt thy "(?l::real) is_expanded";
28.934 +
28.935 +val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
28.936 +val preinst = Envir.subst_term inst precond;
28.937 +UnparseC.term preinst;
28.938 +
28.939 +"===== Rational.thy: cancel ===";
28.940 +(* pat matched with the current term gives an environment
28.941 + (or not: hen the Rrls not applied);
28.942 + if pre1 and pre2 evaluate to @{term True} in this environment,
28.943 + then the Rrls is applied. *)
28.944 +val t = TermC.str2term "(a + b) / c ::real";
28.945 +val pat = TermC.parse_patt thy "?r / ?s ::real";
28.946 +val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
28.947 +val prepat = [(pres, pat)];
28.948 +val erls = rational_erls;
28.949 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
28.950 +
28.951 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
28.952 +val asms = map (Envir.subst_term subst) pres;
28.953 +if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
28.954 +then () else error "rewrite.sml: prepat cancel subst";
28.955 +\<close> ML \<open>
28.956 +(*+*)val ([], false) = eval__true thy 0 asms [] erls
28.957 +\<close> ML \<open>
28.958 +if ([], true) = eval__true thy 0 asms [] erls
28.959 +then () else error "rewrite.sml: prepat cancel eval__true";
28.960 +
28.961 +"===== Rational.thy: add_fractions_p ===";
28.962 +(* if each pat* TermC.matches with the current term, the Rrls is applied
28.963 + (there are no preconditions to be checked, they are @{term True}) *)
28.964 +val t = TermC.str2term "a / b + 1 / 2";
28.965 +val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
28.966 +val pres = [@{term True}];
28.967 +val prepat = [(pres, pat)];
28.968 +val erls = rational_erls;
28.969 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
28.970 +
28.971 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
28.972 +\<close> ML \<open>
28.973 +(*+*)val ([], false) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
28.974 +\<close> ML \<open>
28.975 +if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
28.976 +then () else error "rewrite.sml: prepat add_fractions_p";
28.977 +
28.978 +"===== Poly.thy: order_mult_ ===";
28.979 + (* ?p matched with the current term gives an environment,
28.980 + which evaluates (the instantiated) "p is_multUnordered" to true*)
28.981 +val t = TermC.str2term "x \<up> 2 * x";
28.982 +val pat = TermC.parse_patt thy "?p :: real"
28.983 +val pres = [TermC.parse_patt thy "?p is_multUnordered"];
28.984 +val prepat = [(pres, pat)];
28.985 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
28.986 + [Eval ("Poly.is_multUnordered",
28.987 + eval_is_multUnordered "")];
28.988 +
28.989 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
28.990 +val asms = map (Envir.subst_term subst) pres;
28.991 +\<close> ML \<open>
28.992 +(*+*)UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
28.993 +\<close> ML \<open>
28.994 +if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
28.995 +then () else error "rewrite.sml: prepat order_mult_ subst";
28.996 +\<close> ML \<open>
28.997 +(*+*)val ([], false) = eval__true thy 0 asms [] erls
28.998 +\<close> ML \<open>
28.999 +if ([], true) = eval__true thy 0 asms [] erls
28.1000 +then () else error "rewrite.sml: prepat order_mult_ eval__true";
28.1001 +
28.1002 +
28.1003 +\<close> ML \<open>
28.1004 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
28.1005 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
28.1006 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
28.1007 +val t = TermC.str2term "x \<up> 2 * x";
28.1008 +
28.1009 +\<close> ML \<open>
28.1010 +(*+*)is_multUnordered t = false
28.1011 +\<close> ML \<open>
28.1012 +if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
28.1013 +\<close> ML \<open>
28.1014 +val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
28.1015 +\<close> ML \<open>
28.1016 +
28.1017 + eval_is_multUnordered "testid" "" tm thy;
28.1018 +case eval_is_multUnordered "testid" "" tm thy of
28.1019 + SOME
28.1020 + ("testidx \<up> 2 * x_",
28.1021 + Const ("HOL.Trueprop", _) $
28.1022 + (Const ("HOL.eq", _) $
28.1023 + (Const ("Poly.is_multUnordered", _) $
28.1024 + (Const ("Groups.times_class.times", _) $
28.1025 + (Const ("Transcendental.powr", _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
28.1026 + Const ("HOL.False", _))) => ()
28.1027 +(* ^^^^^^ compare ---vvv *)
28.1028 +| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
28.1029 +\<close> ML \<open>
28.1030 +case eval_is_multUnordered "testid" "" tm thy of
28.1031 + SOME (_, Const ("HOL.Trueprop", _) $
28.1032 + (Const ("HOL.eq", _) $
28.1033 + (Const ("Poly.is_multUnordered", _) $ _) $
28.1034 + Const ("HOL.True", _))) => ()
28.1035 + | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
28.1036 +
28.1037 +tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
28.1038 +\<close> ML \<open>
28.1039 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
28.1040 +\<close> ML \<open>
28.1041 +tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
28.1042 +\<close> ML \<open>
28.1043 +UnparseC.term t'
28.1044 +\<close> ML \<open>
28.1045 +if UnparseC.term t' = "x * x \<up> 2" then ()
28.1046 +else error "rewrite.sml Poly.is_multUnordered doesn't work";
28.1047 +
28.1048 +(* for achieving the previous result, the following code was taken apart *)
28.1049 +"----- rewrite__set_ ---";
28.1050 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
28.1051 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
28.1052 +"----- app_rev ---";
28.1053 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
28.1054 + fun chk_prepat thy erls [] t = true
28.1055 + | chk_prepat thy erls prepat t =
28.1056 + let fun chk (pres, pat) =
28.1057 + (let val subst: Type.tyenv * Envir.tenv =
28.1058 + Pattern.match thy (pat, t)
28.1059 + (Vartab.empty, Vartab.empty)
28.1060 + in snd (eval__true thy (i+1)
28.1061 + (map (Envir.subst_term subst) pres)
28.1062 + [] erls)
28.1063 + end)
28.1064 + handle Pattern.MATCH => false
28.1065 + fun scan_ f [] = false (*scan_ NEVER called by []*)
28.1066 + | scan_ f (pp::pps) = if f pp then true
28.1067 + else scan_ f pps;
28.1068 + in scan_ chk prepat end;
28.1069 +
28.1070 + (*.apply the normal_form of a rev-set.*)
28.1071 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
28.1072 + if chk_prepat thy erls prepat t
28.1073 + then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
28.1074 + normal_form t)
28.1075 + else NONE;
28.1076 +(*fixme val NONE = app_rev' thy rrls t;*)
28.1077 +"----- app_rev' ---";
28.1078 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
28.1079 +(*fixme false*) chk_prepat thy erls prepat t;
28.1080 +"----- chk_prepat ---";
28.1081 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
28.1082 + fun chk (pres, pat) =
28.1083 + (let val subst: Type.tyenv * Envir.tenv =
28.1084 + Pattern.match thy (pat, t)
28.1085 + (Vartab.empty, Vartab.empty)
28.1086 + in snd (eval__true thy (i+1)
28.1087 + (map (Envir.subst_term subst) pres)
28.1088 + [] erls)
28.1089 + end)
28.1090 + handle Pattern.MATCH => false;
28.1091 + fun scan_ _ [] = false (*scan_ NEVER called by []*)
28.1092 + | scan_ f (pp::pps) = if f pp then true
28.1093 + else scan_ f pps;
28.1094 +tracing "=== poly.sml: scan_ chk prepat begin";
28.1095 +scan_ chk prepat;
28.1096 +tracing "=== poly.sml: scan_ chk prepat end";
28.1097 +
28.1098 +"----- chk ---";
28.1099 +(*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
28.1100 +val [(pres, pat)] = prepat;
28.1101 + val subst: Type.tyenv * Envir.tenv =
28.1102 + Pattern.match thy (pat, t)
28.1103 + (Vartab.empty, Vartab.empty);
28.1104 +
28.1105 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
28.1106 +"----- eval__true ---";
28.1107 +val asms = (map (Envir.subst_term subst) pres);
28.1108 +if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
28.1109 +else error "rewrite.sml: diff. is_multUnordered, asms";
28.1110 +val (thy, i, asms, bdv, rls) =
28.1111 + (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
28.1112 + [] : (term * term) list, erls);
28.1113 +case eval__true thy i asms bdv rls of
28.1114 + ([], true) => ()
28.1115 + | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
28.1116 +
28.1117 +\<close> ML \<open>
28.1118 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
28.1119 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
28.1120 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
28.1121 +val thm = ThmC.numerals_to_Free @{thm div_by_1};
28.1122 +val prop = Thm.prop_of thm;
28.1123 +TermC.atomty prop; (*Type 'a*)
28.1124 +val t = TermC.str2term "(2*x)/1"; (*Type real*)
28.1125 +
28.1126 +val (thy, ro, er, inst) =
28.1127 + (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
28.1128 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
28.1129 +
28.1130 +\<close> ML \<open> (*loops*)
28.1131 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
28.1132 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
28.1133 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
28.1134 +val thy = @{theory RatEq};
28.1135 +val ctxt = Proof_Context.init_global thy;
28.1136 +val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
28.1137 +val rls = assoc_rls "RatEq_eliminate"
28.1138 +
28.1139 +val SOME (t''''', asm''''') =
28.1140 + rewrite_set_ thy true rls t;
28.1141 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
28.1142 + rewrite__set_ thy 1 bool [] rls term;
28.1143 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
28.1144 + = (thy, 1, bool, []:(term * term) list, rls, term);
28.1145 +
28.1146 +(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
28.1147 + datatype switch = Applicable.Yes | Noap;
28.1148 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
28.1149 + | rew_once ruls asm ct Applicable.Yes [] =
28.1150 + (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
28.1151 + | Rule_Set.Sequence _ => (ct, asm)
28.1152 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
28.1153 + | rew_once ruls asm ct apno (rul :: thms) =
28.1154 + case rul of
28.1155 + Rule.Thm (thmid, thm) =>
28.1156 + (trace1 i (" try thm: " ^ thmid);
28.1157 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
28.1158 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
28.1159 + NONE => rew_once ruls asm ct apno thms
28.1160 + | SOME (ct', asm') =>
28.1161 + (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
28.1162 + rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
28.1163 + (* once again try the same rule, e.g. associativity against "()"*)
28.1164 + | Rule.Eval (cc as (op_, _)) =>
28.1165 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
28.1166 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
28.1167 + in case Eval.adhoc_thm thy cc ct of
28.1168 + NONE => rew_once ruls asm ct apno thms
28.1169 + | SOME (_, thm') =>
28.1170 + let
28.1171 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
28.1172 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
28.1173 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
28.1174 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
28.1175 + val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
28.1176 + in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
28.1177 + end
28.1178 + | Rule.Cal1 (cc as (op_, _)) =>
28.1179 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
28.1180 + val ct = TermC.uminus_to_string ct
28.1181 + in case Eval.adhoc_thm1_ thy cc ct of
28.1182 + NONE => (ct, asm)
28.1183 + | SOME (_, thm') =>
28.1184 + let
28.1185 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
28.1186 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
28.1187 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
28.1188 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
28.1189 + val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
28.1190 + in the pairopt end
28.1191 + end
28.1192 + | Rule.Rls_ rls' =>
28.1193 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
28.1194 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
28.1195 + | NONE => rew_once ruls asm ct apno thms)
28.1196 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
28.1197 + val ruls = (#rules o Rule.Rule_Set.rep) rls;
28.1198 +(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
28.1199 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
28.1200 +"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
28.1201 + = (ruls, []:term list, ct, Noap, ruls);
28.1202 + val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
28.1203 +
28.1204 + val SOME (ct', asm') = (*case*)
28.1205 + rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
28.1206 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
28.1207 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
28.1208 + = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
28.1209 + ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
28.1210 +
28.1211 + val (t', asms, _ (*lrd*), rew) =
28.1212 + rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
28.1213 + (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
28.1214 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
28.1215 + = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
28.1216 + (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
28.1217 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
28.1218 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
28.1219 +;
28.1220 +(*+*)if UnparseC.term r' =
28.1221 +(*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
28.1222 +(*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
28.1223 +(*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
28.1224 +(*+*) " 1 / x) =\n" ^
28.1225 +(*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
28.1226 +(*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
28.1227 +(*+*)then () else error "instantiated rule CHANGED";
28.1228 +
28.1229 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
28.1230 +;
28.1231 +(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
28.1232 +(*+*)then () else error "stored assumptions CHANGED";
28.1233 +
28.1234 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
28.1235 +;
28.1236 +(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
28.1237 +(*+*)then () else error "rewritten term (an equality) CHANGED";
28.1238 +
28.1239 + val (simpl_p', nofalse) =
28.1240 + eval__true thy (i + 1) p' bdv rls;
28.1241 +"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
28.1242 + (*if*) asms = [@{term True}] orelse asms = [] (*else*);
28.1243 +
28.1244 +(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
28.1245 +(*+*)then () else error "asms before chk CHANGED";
28.1246 +
28.1247 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
28.1248 + | chk indets (a :: asms) =
28.1249 + (case rewrite__set_ thy (i + 1) false bdv rls a of
28.1250 + NONE => (chk (indets @ [a]) asms)
28.1251 + | SOME (t, a') =>
28.1252 + if t = @{term True} then (chk (indets @ a') asms)
28.1253 + else if t = @{term False} then ([], false)
28.1254 + (*asm false .. thm not applied \<up> ; continue until False vvv*)
28.1255 + else chk (indets @ [t] @ a') asms);
28.1256 +
28.1257 + val (xxx, true) =
28.1258 + chk [] asms; (*return from eval__true*);
28.1259 +"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
28.1260 +
28.1261 +(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
28.1262 +(*+*)(*val rules =
28.1263 +(*+*) [Eval ("Rings.divide_class.divide", fn),
28.1264 +(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
28.1265 +(*+*) :
28.1266 +(*+*) Eval ("HOL.eq", fn),
28.1267 +(*+*) Thm ("not_true", "(\<not> True) = False"),
28.1268 +(*+*) Thm ("not_false", "(\<not> False) = True"),
28.1269 +(*+*) :
28.1270 +(*+*) Eval ("Transcendental.powr", fn),
28.1271 +(*+*) Eval ("RatEq.is_ratequation_in", fn)]:
28.1272 +(*+*) rule list*)
28.1273 +(*+*)chk: term list -> term list -> term list * bool
28.1274 +
28.1275 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
28.1276 +
28.1277 +(*+*)Rewrite.trace_on := true;
28.1278 +
28.1279 + (*this was False; vvvv--- means: indeterminate*)
28.1280 + val (* SOME (t, a') *)NONE = (*case*)
28.1281 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
28.1282 +
28.1283 +(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
28.1284 +(*
28.1285 + :
28.1286 + #### rls: rateq_erls on: x \<noteq> 0
28.1287 + :
28.1288 + ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
28.1289 + ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
28.1290 + ##### try calc: HOL.eq'
28.1291 + ##### try thm: not_true
28.1292 + ##### try thm: not_false
28.1293 + ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
28.1294 + and True, False are NOT stored ...
28.1295 + :
28.1296 + ### asms accepted: [x \<noteq> 0] stored: []
28.1297 + : *)
28.1298 +Rewrite.trace_on := false;
28.1299 +( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
28.1300 +
28.1301 +\<close> ML \<open>
28.1302 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
28.1303 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
28.1304 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
28.1305 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
28.1306 + (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
28.1307 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
28.1308 + (thy, 1, [], rew_ord, erls, bool, thm, term);
28.1309 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
28.1310 + (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
28.1311 + val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
28.1312 + val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
28.1313 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
28.1314 + val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
28.1315 +;
28.1316 +if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
28.1317 +else error "ARGS FOR Pattern.match CHANGED";
28.1318 +val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
28.1319 +if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
28.1320 + else error "Pattern.match CHANGED";
28.1321 +
28.1322 +\<close> ML \<open>
28.1323 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
28.1324 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
28.1325 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
28.1326 +(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
28.1327 +val thy = @{theory};
28.1328 +val rls = norm_equation;
28.1329 +val term = TermC.str2term "x + 1 = 2";
28.1330 +
28.1331 +(**)val SOME (t, asm) = rewrite_set_ thy false rls term;
28.1332 +(** )##### try thm: "root_ge0"
28.1333 +exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
28.1334 + dest_eq
28.1335 + 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
28.1336 +if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
28.1337 +
28.1338 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
28.1339 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
28.1340 + (thy, 1, bool, []: (term * term) list, rls, term);
28.1341 +(*deleted after error detection*)
28.1342 +
28.1343 +\<close> ML \<open>
28.1344 +\<close> ML \<open>
28.1345 +\<close>
28.1346 +
28.1347 section \<open>===================================================================================\<close>
28.1348 ML \<open>
28.1349 \<close> ML \<open>