--- a/src/HOL/ex/Meson_Test.thy Sun Apr 14 17:37:05 2019 +0200
+++ b/src/HOL/ex/Meson_Test.thy Sun Apr 14 18:13:46 2019 +0200
@@ -304,7 +304,7 @@
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~product(x::'a,x,x)) --> False"
- oops
+ by meson
(*51194 inferences so far. Searching to depth 13. 204.6 secs
Strange! The previous problem also has 51194 inferences at depth 13. They
@@ -314,7 +314,7 @@
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~sum(x::'a,x,x)) --> False"
- oops
+ by meson
(*74799 inferences so far. Searching to depth 13. 290.0 secs*)
lemma BOO005_1:
@@ -322,7 +322,7 @@
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~sum(x::'a,multiplicative_identity,multiplicative_identity)) --> False"
- oops
+ by meson
(*74799 inferences so far. Searching to depth 13. 314.6 secs*)
lemma BOO006_1:
@@ -330,7 +330,7 @@
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~product(x::'a,additive_identity,additive_identity)) --> False"
- oops
+ by meson
(*5 inferences so far. Searching to depth 5. 1.3 secs*)
lemma BOO011_1:
@@ -434,7 +434,7 @@
(defined(a::'a,d)) &
(identity_map(d)) &
(~equal(domain(a),d)) --> False"
- oops
+ by meson
(*1728 inferences so far. Searching to depth 10. 5.8 secs*)
lemma CAT007_1:
@@ -453,7 +453,7 @@
(defined(a::'a,b)) &
(defined(b::'a,c)) &
(~defined(a::'a,compos(b::'a,c))) --> False"
- oops
+ by meson
(*1118 inferences so far. Searching to depth 8. 2.3 secs*)
lemma COL001_2:
@@ -505,7 +505,7 @@
(agreeable(c)) &
(~agreeable(a)) &
(equal(c::'a,compos(a::'a,b))) --> False"
- oops
+ by meson
(*13201 inferences so far. Searching to depth 11. 31.9 secs*)
lemma COL075_2:
@@ -517,7 +517,7 @@
(\<forall>A B. equal(A::'a,B) --> equal(b(A),b(B))) &
(\<forall>C D. equal(C::'a,D) --> equal(c(C),c(D))) &
(\<forall>Y. ~equal(apply(apply(Y::'a,b(Y)),c(Y)),apply(b(Y),b(Y)))) --> False"
- oops
+ by meson
(*33 inferences so far. Searching to depth 7. 0.1 secs*)
lemma COM001_1:
@@ -785,7 +785,7 @@
between equal equidistant &
(equidistant(u::'a,v,w,x)) &
(~equidistant(u::'a,v,x,w)) --> False"
- oops
+ by meson
(*382903 inferences so far. Searching to depth 9. 1022s (17 mins) on griffon*)
lemma GEO027_3:
@@ -895,7 +895,7 @@
(product(INVERSE(a),INVERSE(b),d)) &
(\<forall>A C B. product(INVERSE(A),INVERSE(B),C) --> product(A::'a,C,B)) &
(~product(c::'a,d,identity)) --> False"
- oops
+ by meson
(*2448 inferences so far. Searching to depth 10. 7.2 secs*)
lemma GRP037_3:
@@ -965,7 +965,7 @@
(\<forall>X Y W Z. product(X::'a,W,Y) & product(X::'a,Z,Y) --> equal(W::'a,Z)) &
(\<forall>Y X W Z. product(W::'a,Y,X) & product(Z::'a,Y,X) --> equal(W::'a,Z)) &
(\<forall>Z1 Z2 Y X. product(X::'a,Y,Z1) & product(X::'a,Z1,Z2) --> product(Z2::'a,Y,X)) --> False"
- oops
+ by meson
abbreviation "GRP004_0_ax INVERSE identity multiply equal \<equiv>
(\<forall>X. equal(multiply(identity::'a,X),X)) &
@@ -1034,7 +1034,7 @@
HEN002_0_ax identity Zero Divide equal mless_equal &
HEN002_0_eq mless_equal Divide equal &
(~equal(Divide(a::'a,a),Zero)) --> False"
- oops
+ by meson
(*202177 inferences so far. Searching to depth 14. 451 secs*)
lemma HEN007_2:
@@ -1065,7 +1065,7 @@
(quotient(z::'a,y,zQy)) &
(quotient(z::'a,x,zQx)) &
(~mless_equal(zQy::'a,zQx)) --> False"
- oops
+ by meson
(*60026 inferences so far. Searching to depth 12. 42.2 secs*)
lemma HEN008_4:
@@ -1081,7 +1081,7 @@
(\<forall>Y Z X. mless_equal(X::'a,Y) --> mless_equal(Divide(Z::'a,Y),Divide(Z::'a,X))) &
(mless_equal(a::'a,b)) &
(~mless_equal(Divide(a::'a,c),Divide(b::'a,c))) --> False"
- oops
+ by meson
(*3160 inferences so far. Searching to depth 11. 3.5 secs*)
lemma HEN009_5:
@@ -1109,7 +1109,7 @@
HEN002_0_ax identity Zero Divide equal mless_equal &
HEN002_0_eq mless_equal Divide equal &
(~mless_equal(a::'a,a)) --> False"
- oops
+ by meson
(*1063 inferences so far. Searching to depth 20. 1.0 secs*)
@@ -1233,7 +1233,7 @@
(\<forall>G H I'. equal(G::'a,H) & left(G::'a,I') --> left(H::'a,I')) &
(\<forall>J L K'. equal(J::'a,K') & left(L::'a,J) --> left(L::'a,K')) &
(~left(num3::'a,u)) --> False"
- oops
+ by meson
(*2392 inferences so far. Searching to depth 12. 2.2 secs*)
@@ -1355,7 +1355,7 @@
(\<forall>B A C. equal(add(A::'a,B),add(C::'a,B)) --> equal(A::'a,C)) &
(mless(a::'a,a)) &
(\<forall>A. ~equal(successor(A),num0)) --> False"
- oops
+ by meson
abbreviation "SET004_0_ax not_homomorphism2 not_homomorphism1
homomorphism compatible operation cantor diagonalise subset_relation
@@ -2010,7 +2010,7 @@
(a_truth(says(a::'a,equal_type(b::'a,c)))) &
(ask_1_if_2(c::'a,equal_type(a::'a,b))) &
(\<forall>Answer. ~answer(Answer)) --> False"
- oops
+ by meson
(*621 inferences so far. Searching to depth 18. 0.2 secs*)
@@ -2074,7 +2074,7 @@
(\<forall>Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) &
(\<forall>Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) &
(~product(a::'a,additive_identity,additive_identity)) --> False"
- oops
+ by meson
abbreviation "RNG_other_ax multiply add equal product additive_identity additive_inverse sum \<equiv>
(\<forall>X. sum(X::'a,additive_inverse(X),additive_identity)) &
@@ -2279,7 +2279,7 @@
(product(a::'a,b,additive_identity)) &
(~equal(a::'a,additive_identity)) &
(~equal(b::'a,additive_identity)) --> False"
- oops
+ by meson
(*101319 inferences so far. Searching to depth 14. 76.0 secs*)
lemma ROB010_1:
@@ -2292,7 +2292,7 @@
(\<forall>G H. equal(G::'a,H) --> equal(negate(G),negate(H))) &
(equal(negate(add(a::'a,negate(b))),c)) &
(~equal(negate(add(c::'a,negate(add(b::'a,a)))),a)) --> False"
- oops
+ by meson
(*6933 inferences so far. Searching to depth 12. 5.1 secs*)
@@ -2329,7 +2329,7 @@
(positive_integer(k)) &
(\<forall>Vk X Y. equal(negate(add(negate(Y),negate(add(X::'a,negate(Y))))),X) & positive_integer(Vk) --> equal(negate(add(Y::'a,multiply(Vk::'a,add(X::'a,negate(add(X::'a,negate(Y))))))),negate(Y))) &
(~equal(negate(add(e::'a,multiply(k::'a,add(d::'a,negate(add(d::'a,negate(e))))))),negate(e))) --> False"
- oops
+ by meson
(*14077 inferences so far. Searching to depth 11. 32.8 secs*)
lemma ROB021_1:
@@ -2342,7 +2342,7 @@
(\<forall>G H. equal(G::'a,H) --> equal(negate(G),negate(H))) &
(\<forall>X Y. equal(negate(X),negate(Y)) --> equal(X::'a,Y)) &
(~equal(add(negate(add(a::'a,negate(b))),negate(add(negate(a),negate(b)))),b)) --> False"
- oops
+ by meson
(*35532 inferences so far. Searching to depth 19. 54.3 secs*)
lemma SET005_1:
@@ -2362,7 +2362,7 @@
(intersection(b::'a,c,bIc)) &
(intersection(a::'a,bIc,aIbIc)) &
(~intersection(aIb::'a,c,aIbIc)) --> False"
- oops
+ by meson
(*6450 inferences so far. Searching to depth 14. 4.2 secs*)
@@ -2895,6 +2895,6 @@
(\<forall>X U Y. subset_collections(X::'a,Y) & element_of_collection(U::'a,X) --> element_of_collection(U::'a,Y)) &
(subset_collections(g::'a,top_of_basis(f))) &
(~element_of_collection(union_of_members(g),top_of_basis(f))) --> False"
- oops
+ by meson
end