Building Pre_Polynomial_Factorization ...
Building Sqrt_Babylonian ...
Running AODV ...
Running Hermite ...
Running Impossible_Geometry ...
Running Perfect-Number-Thm ...
Perfect-Number-Thm FAILED
(see also
/mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Perfect-Number-Thm)
val it = (): unit
Loading theory "Primes" (required by "Perfect" via "Sigma" via "PerfectBasics")
Loading theory "Infinite_Set" (required by "Perfect" via "Sigma")
### theory "Infinite_Set"
### 2.227s elapsed time, 6.440s cpu time, 1.968s GC time
### theory "Primes"
### 2.278s elapsed time, 6.752s cpu time, 2.000s GC time
Loading theory "Exponent" (required by "Perfect" via "Sigma" via
"PerfectBasics")
### theory "Exponent"
### 0.329s elapsed time, 1.756s cpu time, 0.148s GC time
Loading theory "PerfectBasics" (required by "Perfect" via "Sigma")
### theory "PerfectBasics"
### 0.159s elapsed time, 0.844s cpu time, 0.056s GC time
Loading theory "Sigma" (required by "Perfect")
### theory "Sigma"
### 0.559s elapsed time, 2.836s cpu time, 0.204s GC time
Loading theory "Perfect"
### theory "Perfect"
### 0.161s elapsed time, 0.724s cpu time, 0.076s GC time
*** Undefined fact: "division_decomp_nat" (line 196 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** At command "by" (line 196 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
### Metis: Unused theorems: "Groups.ab_semigroup_add_class.add.commute",
"Groups.ab_semigroup_add_class.add.left_commute"
### Metis: Unused theorems: "Groups.ab_semigroup_add_class.add.commute",
"Groups.ab_semigroup_add_class.add.left_commute"
*** Undefined fact: "coprime_exp_nat" (line 163 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** At command "apply" (line 163 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** Undefined fact: "coprime_exp_nat" (line 203 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** At command "by" (line 203 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
### Ignoring duplicate rewrite rule:
### ?a1 dvd ?y \<Longrightarrow> ?a1 * (?y div ?a1) \<equiv> ?y
*** Undefined fact: "coprime_exp_nat" (line 203 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** At command "by" (line 203 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** Undefined fact: "coprime_exp_nat" (line 163 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** At command "apply" (line 163 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** Undefined fact: "division_decomp_nat" (line 196 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
*** At command "by" (line 196 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
Running QR_Decomposition ...
Impossible_Geometry FAILED
(see also
/mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Impossible_Geometry)
minus_point == minus :: point \<Rightarrow> point \<Rightarrow> point
plus_point == plus :: point \<Rightarrow> point \<Rightarrow> point
instantiation
point :: metric_space
dist_point == dist :: point \<Rightarrow> point \<Rightarrow> real
uniformity_point == uniformity :: (point \<times> point) filter
open_point == open :: point set \<Rightarrow> bool
Proofs for inductive predicate(s) "radical_sqrtp"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Proofs for inductive predicate(s) "constructiblep"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
### theory "Impossible_Geometry"
### 7.730s elapsed time, 17.180s cpu time, 3.876s GC time
### Metis: Unused theorems: "local.a", "local.d"
### Metis: Unused theorems: "local.b", "local.e"
*** Undefined fact: "gcd_exp_int" (line 1285 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** At command "by" (line 1285 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
### Metis: Unused theorems: "local.hypsp_2", "local.hypsp_3"
*** Undefined fact: "gcd_exp_int" (line 1336 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** At command "by" (line 1336 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** Undefined fact: "coprime_exp_int" (line 1365 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** At command "by" (line 1365 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** Undefined fact: "coprime_exp_int" (line 1365 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** At command "by" (line 1365 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** Undefined fact: "gcd_exp_int" (line 1336 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** At command "by" (line 1336 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** Undefined fact: "gcd_exp_int" (line 1285 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
*** At command "by" (line 1285 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
Running Encodability_Process_Calculi ...
Sqrt_Babylonian FAILED
(see also
/mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Sqrt_Babylonian)
val it = (): unit
Loading theory "Sqrt_Babylonian_Auxiliary" (required by "NthRoot_Impl")
### theory "Sqrt_Babylonian_Auxiliary"
### 2.780s elapsed time, 7.608s cpu time, 2.004s GC time
Loading theory "NthRoot_Impl"
locale fixed_root =
fixes p :: "nat"
and pm :: "nat"
assumes "fixed_root p pm"
locale fixed_root =
fixes p :: "nat"
and pm :: "nat"
assumes "fixed_root p pm"
### theory "NthRoot_Impl"
### 2.063s elapsed time, 6.552s cpu time, 1.112s GC time
Loading theory "Sqrt_Babylonian"
locale sqrt_approximation =
fixes \<epsilon> :: "'a"
and n :: "'a"
assumes "sqrt_approximation \<epsilon> n"
### theory "Sqrt_Babylonian"
### 0.812s elapsed time, 4.332s cpu time, 0.184s GC time
### Ignoring duplicate rewrite rule:
### of_int (?z1 ^ ?n1) \<equiv> of_int ?z1 ^ ?n1
*** Undefined fact: "coprime_exp_int" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
*** At command "by" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
(log (real b) (real_of_int (int b ^ ss)) < log (real b) (real_of_int x)) =
(real_of_int (int b ^ ss) < real_of_int x)
"(215912063945802350977 / 152672884556058511392,
1104427674243920646305299201 / 23309009678667569523128057147486993777664,
True)"
:: "rat \<times> rat \<times> bool"
*** Undefined fact: "coprime_exp_int" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
*** At command "by" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
Real_Impl CANCELLED
Running Probabilistic_Noninterference ...
Hermite FAILED
(see also
/mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Hermite)
"\<And>b a c.
b \<noteq> (0::'a) \<Longrightarrow>
(a + c * b) div b = c + a div b"
and
"div_mult_mult1":
"\<And>c a b.
c \<noteq> (0::'a) \<Longrightarrow> c * a div (c * b) = a div b"
class semiring_div = div + algebraic_semidom +
assumes "mod_div_equality": "\<And>a b. a div b * b + a mod b = a"
and "div_by_0": "\<And>a. a div (0::'a) = (0::'a)"
and "div_0": "\<And>a. (0::'a) div a = (0::'a)"
and
"div_mult_self1":
"\<And>b a c.
b \<noteq> (0::'a) \<Longrightarrow>
(a + c * b) div b = c + a div b"
and
"div_mult_mult1":
"\<And>c a b.
c \<noteq> (0::'a) \<Longrightarrow> c * a div (c * b) = a div b"
### theory "Hermite"
### 10.324s elapsed time, 29.832s cpu time, 4.196s GC time
Loading theory "Hermite_IArrays"
### theory "Hermite_IArrays"
### 1.745s elapsed time, 6.540s cpu time, 1.052s GC time
"IArray [IArray [1, 44, 57], IArray [0, 108, 52], IArray [0, 0, 63]]"
:: "int iarray iarray"
"[[1, 44, 57], [0, 108, 52], [0, 0, 63]]"
:: "int list list"
"IArray [IArray [1, 44, 57], IArray [0, 108, 52], IArray [0, 0, 63]]"
:: "int iarray iarray"
"[[[:1:], [:- (44 / 89), 31 / 89, - (68 / 89), 137 / 89, 40 / 89:]],
[0, [:- (2 / 5), 4 / 5, 4, 22 / 5, 24 / 5, 1:]]]"
:: "real poly list list"
"IArray
[IArray [[:1:], [:- (44 / 89), 31 / 89, - (68 / 89), 137 / 89, 40 / 89:]],
IArray [0, [:- (2 / 5), 4 / 5, 4, 22 / 5, 24 / 5, 1:]]]"
:: "real poly iarray iarray"
*** Undefined fact: "gcd_poly.simps" (line 37 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Hermite/Hermite.thy")
*** At command "by" (line 36 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Hermite/Hermite.thy")
Pre_Polynomial_Factorization FAILED
(see also
/mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Pre_Polynomial_Factorization)
registered mat in class set_impl
use dlist as set_impl for type vec
registered vec in class set_impl
use None as trivial implementation of cenum for type mat
registered mat in class cenum
use None as trivial implementation of cenum for type vec
registered vec in class cenum
### theory "Matrix_IArray_Impl"
### 5.297s elapsed time, 16.428s cpu time, 2.408s GC time
### theory "Gauss_Jordan"
### 6.924s elapsed time, 20.880s cpu time, 5.188s GC time
Loading theory "Gauss_Jordan_IArray_Impl"
### theory "Gauss_Jordan_IArray_Impl"
### 3.884s elapsed time, 15.888s cpu time, 3.660s GC time
### Rule already declared as introduction (intro)
### \<lbrakk>\<And>i j.
### \<lbrakk>i < dim\<^sub>r ?B; j < dim\<^sub>c ?B\<rbrakk>
### \<Longrightarrow> ?A $$ (i, j) = ?B $$ (i, j);
### dim\<^sub>r ?A = dim\<^sub>r ?B; dim\<^sub>c ?A = dim\<^sub>c ?B\<rbrakk>
### \<Longrightarrow> ?A = ?B
### Rule already declared as introduction (intro)
### \<lbrakk>\<And>i j.
### \<lbrakk>i < dim\<^sub>r ?B; j < dim\<^sub>c ?B\<rbrakk>
### \<Longrightarrow> ?A $$ (i, j) = ?B $$ (i, j);
### dim\<^sub>r ?A = dim\<^sub>r ?B; dim\<^sub>c ?A = dim\<^sub>c ?B\<rbrakk>
### \<Longrightarrow> ?A = ?B
### Rule already declared as introduction (intro)
### \<lbrakk>\<And>i j.
### \<lbrakk>i < dim\<^sub>r ?B; j < dim\<^sub>c ?B\<rbrakk>
### \<Longrightarrow> ?A $$ (i, j) = ?B $$ (i, j);
### dim\<^sub>r ?A = dim\<^sub>r ?B; dim\<^sub>c ?A = dim\<^sub>c ?B\<rbrakk>
### \<Longrightarrow> ?A = ?B
"\<zero>\<^sub>v
6 |\<^sub>v 1 \<mapsto> (2::'a) |\<^sub>v 2 \<mapsto> (3::'a)"
:: "'a vec"
(log (real b) (real_of_int (int b ^ ss)) < log (real b) (real_of_int x)) =
(real_of_int (int b ^ ss) < real_of_int x)
"\<zero>\<^sub>m 6
4 |\<^sub>m (1, 3) \<mapsto> (2::'a) |\<^sub>m (2, 1) \<mapsto> (3::'a)"
:: "'a mat"
"(215912063945802350977 / 152672884556058511392,
1104427674243920646305299201 / 23309009678667569523128057147486993777664,
True)"
:: "rat \<times> rat \<times> bool"
*** Undefined fact: "coprime_exp_int" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
*** At command "by" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
Polynomial_Factorization CANCELLED
Pre_Algebraic_Numbers CANCELLED
Algebraic_Numbers CANCELLED
QR_Decomposition FAILED
(see also
/mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/QR_Decomposition)
\<And>b. b \<in> ?C - ?B \<Longrightarrow> ?h b = (0::?'a);
setsum ?g ?C = setsum ?h ?C\<rbrakk>
\<Longrightarrow> setsum ?g ?A = setsum ?h ?B
"None"
:: "(real list \<times> real list set) option"
"Some ([4, - 3, 0], {[1, - 1, 1]})"
:: "(real list \<times> real list set) option"
"Some
([63 / 5, 57 / 5, 0, 0], {[2, 2, 1, 0], [- (26 / 5), - (24 / 5), 0, 1]})"
:: "(real list \<times> real list set) option"
"{False, True}"
:: "bool set"
"{False, True}"
:: "bool set"
\<lbrakk>finite {p. 0 \<le> p \<and> nat 0 < f p};
\<And>p.
\<lbrakk>0 \<le> p; nat 0 < f p\<rbrakk>
\<Longrightarrow> prime (nat p)\<rbrakk>
\<Longrightarrow> prime_factors
(\<Prod>x\<in>{p. 0 \<le> p \<and> nat 0 < f p}.
x ^ f x) =
{p. 0 \<le> p \<and> nat 0 < f p}
"{a\<^sub>1, a\<^sub>2}"
:: "Enum.finite_2 set"
"op *s"
:: "'a \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec"
"op *\<^sub>R"
:: "real \<Rightarrow> 'a \<Rightarrow> 'a"
(log (real b) (real_of_int (int b ^ ss)) < log (real b) (real_of_int x)) =
(real_of_int (int b ^ ss) < real_of_int x)
"{a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}"
:: "Enum.finite_5 set"
"{a\<^sub>1, a\<^sub>2}"
:: "Enum.finite_2 set"
"{[- 10, 5, 1, 0]}"
:: "real list set"
"{[- (1 / 4), - 1, - (3 / 4), 1]}"
:: "real list set"
*** Undefined fact: "coprime_exp_int" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
*** At command "by" (line 1007 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
Unfinished session(s): Algebraic_Numbers, Hermite, Impossible_Geometry,
Perfect-Number-Thm, Polynomial_Factorization, Pre_Algebraic_Numbers,
Pre_Polynomial_Factorization, QR_Decomposition, Real_Impl, Sqrt_Babylonian
