1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Mon Jul 19 15:34:54 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Mon Jul 19 17:29:35 2021 +0200
1.3 @@ -151,7 +151,7 @@
1.4 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
1.5 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
1.6
1.7 -(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
1.8 +(*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
1.9 val thy = @{theory Partial_Fractions}
1.10 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.11
1.12 @@ -193,27 +193,27 @@
1.13 val ll = map monom2list (poly2list t);
1.14
1.15 (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
1.16 -(*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
1.17 -(*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
1.18 +(*+*)val [ [(Const (\<^const_name>\<open>numeral\<close>, _) $ _), Free ("b", _)],
1.19 +(*+*) [Free ("a", _), (Const (\<^const_name>\<open>numeral\<close>, _) $ _)]
1.20 (*+*) ] = map monom2list (poly2list t);
1.21
1.22 val lls = map sort_varList ll;
1.23
1.24 (*+*)case map sort_varList ll of
1.25 -(*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
1.26 -(*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
1.27 +(*+*) [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("b", _)],
1.28 +(*+*) [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)]
1.29 (*+*) ] => ()
1.30 (*+*)| _ => error "map sort_varList CHANGED";
1.31
1.32 val T = type_of t;
1.33 val ls = map (create_monom T) lls;
1.34
1.35 -(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
1.36 -(*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
1.37 +(*+*)val [Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("b", _),
1.38 +(*+*) Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
1.39
1.40 (*+*)case map (create_monom T) lls of
1.41 -(*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
1.42 -(*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
1.43 +(*+*) [Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("b", _),
1.44 +(*+*) Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("a", _)
1.45 (*+*) ] => ()
1.46 (*+*)| _ => error "map (create_monom T) CHANGED";
1.47
1.48 @@ -232,15 +232,15 @@
1.49 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.50 val ll = map monom2list (poly2list t);
1.51
1.52 -(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
1.53 -(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
1.54 +(*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
1.55 +(*+*) [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*already correct order*)
1.56 (*+*) ] = map monom2list (poly2list t);
1.57
1.58 val lls = map
1.59 sort_varList ll;
1.60
1.61 -(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
1.62 -(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
1.63 +(*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
1.64 +(*+*) [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
1.65 (*+*) ] = map sort_varList ll;
1.66
1.67 map sort_varList ll;
1.68 @@ -362,7 +362,7 @@
1.69 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
1.70 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
1.71 (*if*) (is_nums x) (*else*);
1.72 - val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.73 + val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
1.74 (*case*) x (*of*);
1.75 (*+*)UnparseC.term x = "x \<up> 2";
1.76 (*if*) TermC.is_num t (*then*);
1.77 @@ -370,7 +370,7 @@
1.78 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.79 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.80 (*if*) (is_nums x) (*else*);
1.81 - val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.82 + val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
1.83 (*case*) x (*of*);
1.84 (*+*)UnparseC.term x = "y \<up> 2";
1.85 (*if*) TermC.is_num t (*then*);
1.86 @@ -385,7 +385,7 @@
1.87 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
1.88 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
1.89 (*if*) (is_nums x) (*else*);
1.90 -val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.91 +val (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ t) =
1.92 (*case*) x (*of*);
1.93 (*+*)UnparseC.term x = "x \<up> 3";
1.94 (*if*) TermC.is_num t (*then*);
1.95 @@ -468,10 +468,10 @@
1.96 "----- eval_is_multUnordered ---";
1.97 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";
1.98 case eval_is_multUnordered "testid" "" tm thy of
1.99 - SOME (_, Const ("HOL.Trueprop", _) $
1.100 - (Const ("HOL.eq", _) $
1.101 - (Const ("Poly.is_multUnordered", _) $ _) $
1.102 - Const ("HOL.True", _))) => ()
1.103 + SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
1.104 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
1.105 + (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
1.106 + Const (\<^const_name>\<open>True\<close>, _))) => ()
1.107 | _ => error "poly.sml diff. eval_is_multUnordered";
1.108
1.109 "----- rewrite_set_ STILL DIDN'T WORK";
1.110 @@ -492,9 +492,9 @@
1.111 case eval_is_multUnordered "xxx " "yyy " t thy of
1.112 SOME
1.113 ("xxx 3 * a + - 2 * a_",
1.114 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.115 - Const ("HOL.False", _))) => ()
1.116 -(* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
1.117 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
1.118 + Const (\<^const_name>\<open>False\<close>, _))) => ()
1.119 +(* Const (\<^const_name>\<open>True\<close>, _))) => () <<<<<--------------------------- this is false*)
1.120 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.121
1.122 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
1.123 @@ -507,8 +507,8 @@
1.124 case eval_is_multUnordered "xxx " "yyy " t thy of
1.125 SOME
1.126 ("xxx - 2 * a_",
1.127 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.128 - Const ("HOL.False", _))) => ()
1.129 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
1.130 + Const (\<^const_name>\<open>False\<close>, _))) => ()
1.131 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.132
1.133 "----- is_multUnordered --- (a) is_multUnordered = False";
1.134 @@ -521,8 +521,8 @@
1.135 case eval_is_multUnordered "xxx " "yyy " t thy of
1.136 SOME
1.137 ("xxx a_",
1.138 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.139 - Const ("HOL.False", _))) => ()
1.140 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
1.141 + Const (\<^const_name>\<open>False\<close>, _))) => ()
1.142 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.143
1.144 "----- is_multUnordered --- (- 2) is_multUnordered = False";
1.145 @@ -535,8 +535,8 @@
1.146 case eval_is_multUnordered "xxx " "yyy " t thy of
1.147 SOME
1.148 ("xxx - 2_",
1.149 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.150 - Const ("HOL.False", _))) => ()
1.151 + Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
1.152 + Const (\<^const_name>\<open>False\<close>, _))) => ()
1.153 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.154
1.155
1.156 @@ -642,10 +642,10 @@
1.157 ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
1.158
1.159 (*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
1.160 -"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
1.161 +"~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (t);
1.162 (*if*) TermC.is_num num (*else*);
1.163
1.164 -"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
1.165 +"~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (num);
1.166 (*if*) TermC.is_num num (*else*);
1.167 (*if*) TermC.is_variable num (*then*);
1.168
1.169 @@ -678,7 +678,7 @@
1.170 (*+*)else error "6 * a is_multUnordered = False CHANGED";
1.171
1.172 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
1.173 - (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
1.174 + (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory});
1.175 (*if*) is_multUnordered arg (*else*);
1.176
1.177 "~~~~~ fun is_multUnordered , args:"; val (t) = (arg);