src/HOL/ex/Refute_Examples.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18789 8a5c6fc3ad27
child 21502 7f3ea2b3bab6
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/ex/Refute_Examples.thy
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2005
     5 *)
     6 
     7 (* See 'HOL/Refute.thy' for help. *)
     8 
     9 header {* Examples for the 'refute' command *}
    10 
    11 theory Refute_Examples imports Main
    12 
    13 begin
    14 
    15 refute_params [satsolver="dpll"]
    16 
    17 lemma "P \<and> Q"
    18   apply (rule conjI)
    19   refute 1  -- {* refutes @{term "P"} *}
    20   refute 2  -- {* refutes @{term "Q"} *}
    21   refute    -- {* equivalent to 'refute 1' *}
    22     -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
    23   refute [maxsize=5]           -- {* we can override parameters ... *}
    24   refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
    25 oops
    26 
    27 section {* Examples and Test Cases *}
    28 
    29 subsection {* Propositional logic *}
    30 
    31 lemma "True"
    32   refute
    33   apply auto
    34 done
    35 
    36 lemma "False"
    37   refute
    38 oops
    39 
    40 lemma "P"
    41   refute
    42 oops
    43 
    44 lemma "~ P"
    45   refute
    46 oops
    47 
    48 lemma "P & Q"
    49   refute
    50 oops
    51 
    52 lemma "P | Q"
    53   refute
    54 oops
    55 
    56 lemma "P \<longrightarrow> Q"
    57   refute
    58 oops
    59 
    60 lemma "(P::bool) = Q"
    61   refute
    62 oops
    63 
    64 lemma "(P | Q) \<longrightarrow> (P & Q)"
    65   refute
    66 oops
    67 
    68 subsection {* Predicate logic *}
    69 
    70 lemma "P x y z"
    71   refute
    72 oops
    73 
    74 lemma "P x y \<longrightarrow> P y x"
    75   refute
    76 oops
    77 
    78 lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
    79   refute
    80 oops
    81 
    82 subsection {* Equality *}
    83 
    84 lemma "P = True"
    85   refute
    86 oops
    87 
    88 lemma "P = False"
    89   refute
    90 oops
    91 
    92 lemma "x = y"
    93   refute
    94 oops
    95 
    96 lemma "f x = g x"
    97   refute
    98 oops
    99 
   100 lemma "(f::'a\<Rightarrow>'b) = g"
   101   refute
   102 oops
   103 
   104 lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
   105   refute
   106 oops
   107 
   108 lemma "distinct [a,b]"
   109   refute
   110   apply simp
   111   refute
   112 oops
   113 
   114 subsection {* First-Order Logic *}
   115 
   116 lemma "\<exists>x. P x"
   117   refute
   118 oops
   119 
   120 lemma "\<forall>x. P x"
   121   refute
   122 oops
   123 
   124 lemma "EX! x. P x"
   125   refute
   126 oops
   127 
   128 lemma "Ex P"
   129   refute
   130 oops
   131 
   132 lemma "All P"
   133   refute
   134 oops
   135 
   136 lemma "Ex1 P"
   137   refute
   138 oops
   139 
   140 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
   141   refute
   142 oops
   143 
   144 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
   145   refute
   146 oops
   147 
   148 lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
   149   refute
   150 oops
   151 
   152 text {* A true statement (also testing names of free and bound variables being identical) *}
   153 
   154 lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
   155   refute [maxsize=4]
   156   apply fast
   157 done
   158 
   159 text {* "A type has at most 4 elements." *}
   160 
   161 lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
   162   refute
   163 oops
   164 
   165 lemma "\<forall>a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
   166   refute  -- {* quantification causes an expansion of the formula; the
   167                 previous version with free variables is refuted much faster *}
   168 oops
   169 
   170 text {* "Every reflexive and symmetric relation is transitive." *}
   171 
   172 lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
   173   refute
   174 oops
   175 
   176 text {* The "Drinker's theorem" ... *}
   177 
   178 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
   179   refute [maxsize=4]
   180   apply (auto simp add: ext)
   181 done
   182 
   183 text {* ... and an incorrect version of it *}
   184 
   185 lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
   186   refute
   187 oops
   188 
   189 text {* "Every function has a fixed point." *}
   190 
   191 lemma "\<exists>x. f x = x"
   192   refute
   193 oops
   194 
   195 text {* "Function composition is commutative." *}
   196 
   197 lemma "f (g x) = g (f x)"
   198   refute
   199 oops
   200 
   201 text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
   202 
   203 lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
   204   refute
   205 oops
   206 
   207 subsection {* Higher-Order Logic *}
   208 
   209 lemma "\<exists>P. P"
   210   refute
   211   apply auto
   212 done
   213 
   214 lemma "\<forall>P. P"
   215   refute
   216 oops
   217 
   218 lemma "EX! P. P"
   219   refute
   220   apply auto
   221 done
   222 
   223 lemma "EX! P. P x"
   224   refute
   225 oops
   226 
   227 lemma "P Q | Q x"
   228   refute
   229 oops
   230 
   231 lemma "P All"
   232   refute
   233 oops
   234 
   235 lemma "P Ex"
   236   refute
   237 oops
   238 
   239 lemma "P Ex1"
   240   refute
   241 oops
   242 
   243 text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
   244 
   245 constdefs
   246   "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   247   "trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
   248   "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   249   "subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
   250   "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   251   "trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
   252 
   253 lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
   254   refute
   255 oops
   256 
   257 text {* "The union of transitive closures is equal to the transitive closure of unions." *}
   258 
   259 lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
   260         \<longrightarrow> trans_closure TP P
   261         \<longrightarrow> trans_closure TR R
   262         \<longrightarrow> (T x y = (TP x y | TR x y))"
   263   refute
   264 oops
   265 
   266 text {* "Every surjective function is invertible." *}
   267 
   268 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
   269   refute
   270 oops
   271 
   272 text {* "Every invertible function is surjective." *}
   273 
   274 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   275   refute
   276 oops
   277 
   278 text {* Every point is a fixed point of some function. *}
   279 
   280 lemma "\<exists>f. f x = x"
   281   refute [maxsize=4]
   282   apply (rule_tac x="\<lambda>x. x" in exI)
   283   apply simp
   284 done
   285 
   286 text {* Axiom of Choice: first an incorrect version ... *}
   287 
   288 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   289   refute
   290 oops
   291 
   292 text {* ... and now two correct ones *}
   293 
   294 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
   295   refute [maxsize=4]
   296   apply (simp add: choice)
   297 done
   298 
   299 lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   300   refute [maxsize=2]
   301   apply auto
   302     apply (simp add: ex1_implies_ex choice)
   303   apply (fast intro: ext)
   304 done
   305 
   306 subsection {* Meta-logic *}
   307 
   308 lemma "!!x. P x"
   309   refute
   310 oops
   311 
   312 lemma "f x == g x"
   313   refute
   314 oops
   315 
   316 lemma "P \<Longrightarrow> Q"
   317   refute
   318 oops
   319 
   320 lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
   321   refute
   322 oops
   323 
   324 subsection {* Schematic variables *}
   325 
   326 lemma "?P"
   327   refute
   328   apply auto
   329 done
   330 
   331 lemma "x = ?y"
   332   refute
   333   apply auto
   334 done
   335 
   336 subsection {* Abstractions *}
   337 
   338 lemma "(\<lambda>x. x) = (\<lambda>x. y)"
   339   refute
   340 oops
   341 
   342 lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
   343   refute
   344 oops
   345 
   346 lemma "(\<lambda>x. x) = (\<lambda>y. y)"
   347   refute
   348   apply simp
   349 done
   350 
   351 subsection {* Sets *}
   352 
   353 lemma "P (A::'a set)"
   354   refute
   355 oops
   356 
   357 lemma "P (A::'a set set)"
   358   refute
   359 oops
   360 
   361 lemma "{x. P x} = {y. P y}"
   362   refute
   363   apply simp
   364 done
   365 
   366 lemma "x : {x. P x}"
   367   refute
   368 oops
   369 
   370 lemma "P op:"
   371   refute
   372 oops
   373 
   374 lemma "P (op: x)"
   375   refute
   376 oops
   377 
   378 lemma "P Collect"
   379   refute
   380 oops
   381 
   382 lemma "A Un B = A Int B"
   383   refute
   384 oops
   385 
   386 lemma "(A Int B) Un C = (A Un C) Int B"
   387   refute
   388 oops
   389 
   390 lemma "Ball A P \<longrightarrow> Bex A P"
   391   refute
   392 oops
   393 
   394 subsection {* arbitrary *}
   395 
   396 lemma "arbitrary"
   397   refute
   398 oops
   399 
   400 lemma "P arbitrary"
   401   refute
   402 oops
   403 
   404 lemma "arbitrary x"
   405   refute
   406 oops
   407 
   408 lemma "arbitrary arbitrary"
   409   refute
   410 oops
   411 
   412 subsection {* The *}
   413 
   414 lemma "The P"
   415   refute
   416 oops
   417 
   418 lemma "P The"
   419   refute
   420 oops
   421 
   422 lemma "P (The P)"
   423   refute
   424 oops
   425 
   426 lemma "(THE x. x=y) = z"
   427   refute
   428 oops
   429 
   430 lemma "Ex P \<longrightarrow> P (The P)"
   431   refute
   432 oops
   433 
   434 subsection {* Eps *}
   435 
   436 lemma "Eps P"
   437   refute
   438 oops
   439 
   440 lemma "P Eps"
   441   refute
   442 oops
   443 
   444 lemma "P (Eps P)"
   445   refute
   446 oops
   447 
   448 lemma "(SOME x. x=y) = z"
   449   refute
   450 oops
   451 
   452 lemma "Ex P \<longrightarrow> P (Eps P)"
   453   refute [maxsize=3]
   454   apply (auto simp add: someI)
   455 done
   456 
   457 (******************************************************************************)
   458 
   459 subsection {* Subtypes (typedef), typedecl *}
   460 
   461 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
   462 
   463 typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)"
   464   by auto
   465 
   466 lemma "(x::'a myTdef) = y"
   467   refute
   468 oops
   469 
   470 typedecl myTdecl
   471 
   472 typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   473   by auto
   474 
   475 lemma "P (f::(myTdecl myTdef) T_bij)"
   476   refute
   477 oops
   478 
   479 (******************************************************************************)
   480 
   481 subsection {* Inductive datatypes *}
   482 
   483 text {* With quick\_and\_dirty set, the datatype package does not generate
   484   certain axioms for recursion operators.  Without these axioms, refute may
   485   find spurious countermodels. *}
   486 
   487 ML {* reset quick_and_dirty; *}
   488 
   489 subsubsection {* unit *}
   490 
   491 lemma "P (x::unit)"
   492   refute
   493 oops
   494 
   495 lemma "\<forall>x::unit. P x"
   496   refute
   497 oops
   498 
   499 lemma "P ()"
   500   refute
   501 oops
   502 
   503 lemma "P (unit_rec u x)"
   504   refute
   505 oops
   506 
   507 lemma "P (case x of () \<Rightarrow> u)"
   508   refute
   509 oops
   510 
   511 subsubsection {* option *}
   512 
   513 lemma "P (x::'a option)"
   514   refute
   515 oops
   516 
   517 lemma "\<forall>x::'a option. P x"
   518   refute
   519 oops
   520 
   521 lemma "P None"
   522   refute
   523 oops
   524 
   525 lemma "P (Some x)"
   526   refute
   527 oops
   528 
   529 lemma "P (option_rec n s x)"
   530   refute
   531 oops
   532 
   533 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
   534   refute
   535 oops
   536 
   537 subsubsection {* * *}
   538 
   539 lemma "P (x::'a*'b)"
   540   refute
   541 oops
   542 
   543 lemma "\<forall>x::'a*'b. P x"
   544   refute
   545 oops
   546 
   547 lemma "P (x,y)"
   548   refute
   549 oops
   550 
   551 lemma "P (fst x)"
   552   refute
   553 oops
   554 
   555 lemma "P (snd x)"
   556   refute
   557 oops
   558 
   559 lemma "P Pair"
   560   refute
   561 oops
   562 
   563 lemma "P (prod_rec p x)"
   564   refute
   565 oops
   566 
   567 lemma "P (case x of Pair a b \<Rightarrow> p a b)"
   568   refute
   569 oops
   570 
   571 subsubsection {* + *}
   572 
   573 lemma "P (x::'a+'b)"
   574   refute
   575 oops
   576 
   577 lemma "\<forall>x::'a+'b. P x"
   578   refute
   579 oops
   580 
   581 lemma "P (Inl x)"
   582   refute
   583 oops
   584 
   585 lemma "P (Inr x)"
   586   refute
   587 oops
   588 
   589 lemma "P Inl"
   590   refute
   591 oops
   592 
   593 lemma "P (sum_rec l r x)"
   594   refute
   595 oops
   596 
   597 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
   598   refute
   599 oops
   600 
   601 subsubsection {* Non-recursive datatypes *}
   602 
   603 datatype T1 = A | B
   604 
   605 lemma "P (x::T1)"
   606   refute
   607 oops
   608 
   609 lemma "\<forall>x::T1. P x"
   610   refute
   611 oops
   612 
   613 lemma "P A"
   614   refute
   615 oops
   616 
   617 lemma "P (T1_rec a b x)"
   618   refute
   619 oops
   620 
   621 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
   622   refute
   623 oops
   624 
   625 datatype 'a T2 = C T1 | D 'a
   626 
   627 lemma "P (x::'a T2)"
   628   refute
   629 oops
   630 
   631 lemma "\<forall>x::'a T2. P x"
   632   refute
   633 oops
   634 
   635 lemma "P D"
   636   refute
   637 oops
   638 
   639 lemma "P (T2_rec c d x)"
   640   refute
   641 oops
   642 
   643 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
   644   refute
   645 oops
   646 
   647 datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
   648 
   649 lemma "P (x::('a,'b) T3)"
   650   refute
   651 oops
   652 
   653 lemma "\<forall>x::('a,'b) T3. P x"
   654   refute
   655 oops
   656 
   657 lemma "P E"
   658   refute
   659 oops
   660 
   661 lemma "P (T3_rec e x)"
   662   refute
   663 oops
   664 
   665 lemma "P (case x of E f \<Rightarrow> e f)"
   666   refute
   667 oops
   668 
   669 subsubsection {* Recursive datatypes *}
   670 
   671 text {* nat *}
   672 
   673 lemma "P (x::nat)"
   674   refute
   675 oops
   676 
   677 lemma "\<forall>x::nat. P x"
   678   refute
   679 oops
   680 
   681 lemma "P (Suc 0)"
   682   refute
   683 oops
   684 
   685 lemma "P Suc"
   686   refute  -- {* @{term "Suc"} is a partial function (regardless of the size
   687                 of the model), hence @{term "P Suc"} is undefined, hence no
   688                 model will be found *}
   689 oops
   690 
   691 lemma "P (nat_rec zero suc x)"
   692   refute
   693 oops
   694 
   695 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
   696   refute
   697 oops
   698 
   699 text {* 'a list *}
   700 
   701 lemma "P (xs::'a list)"
   702   refute
   703 oops
   704 
   705 lemma "\<forall>xs::'a list. P xs"
   706   refute
   707 oops
   708 
   709 lemma "P [x, y]"
   710   refute
   711 oops
   712 
   713 lemma "P (list_rec nil cons xs)"
   714   refute
   715 oops
   716 
   717 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
   718   refute
   719 oops
   720 
   721 lemma "(xs::'a list) = ys"
   722   refute
   723 oops
   724 
   725 lemma "a # xs = b # xs"
   726   refute
   727 oops
   728 
   729 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   730 
   731 lemma "P (x::'a BinTree)"
   732   refute
   733 oops
   734 
   735 lemma "\<forall>x::'a BinTree. P x"
   736   refute
   737 oops
   738 
   739 lemma "P (Node (Leaf x) (Leaf y))"
   740   refute
   741 oops
   742 
   743 lemma "P (BinTree_rec l n x)"
   744   refute
   745 oops
   746 
   747 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
   748   refute
   749 oops
   750 
   751 subsubsection {* Mutually recursive datatypes *}
   752 
   753 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   754      and 'a bexp = Equal "'a aexp" "'a aexp"
   755 
   756 lemma "P (x::'a aexp)"
   757   refute
   758 oops
   759 
   760 lemma "\<forall>x::'a aexp. P x"
   761   refute
   762 oops
   763 
   764 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
   765   refute
   766 oops
   767 
   768 lemma "P (x::'a bexp)"
   769   refute
   770 oops
   771 
   772 lemma "\<forall>x::'a bexp. P x"
   773   refute
   774 oops
   775 
   776 lemma "P (aexp_bexp_rec_1 number ite equal x)"
   777   refute
   778 oops
   779 
   780 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
   781   refute
   782 oops
   783 
   784 lemma "P (aexp_bexp_rec_2 number ite equal x)"
   785   refute
   786 oops
   787 
   788 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
   789   refute
   790 oops
   791 
   792 subsubsection {* Other datatype examples *}
   793 
   794 datatype Trie = TR "Trie list"
   795 
   796 lemma "P (x::Trie)"
   797   refute
   798 oops
   799 
   800 lemma "\<forall>x::Trie. P x"
   801   refute
   802 oops
   803 
   804 lemma "P (TR [TR []])"
   805   refute
   806 oops
   807 
   808 lemma "P (Trie_rec_1 a b c x)"
   809   refute
   810 oops
   811 
   812 lemma "P (Trie_rec_2 a b c x)"
   813   refute
   814 oops
   815 
   816 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
   817 
   818 lemma "P (x::InfTree)"
   819   refute
   820 oops
   821 
   822 lemma "\<forall>x::InfTree. P x"
   823   refute
   824 oops
   825 
   826 lemma "P (Node (\<lambda>n. Leaf))"
   827   refute
   828 oops
   829 
   830 lemma "P (InfTree_rec leaf node x)"
   831   refute
   832 oops
   833 
   834 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
   835 
   836 lemma "P (x::'a lambda)"
   837   refute
   838 oops
   839 
   840 lemma "\<forall>x::'a lambda. P x"
   841   refute
   842 oops
   843 
   844 lemma "P (Lam (\<lambda>a. Var a))"
   845   refute
   846 oops
   847 
   848 lemma "P (lambda_rec v a l x)"
   849   refute
   850 oops
   851 
   852 text {* Taken from "Inductive datatypes in HOL", p.8: *}
   853 
   854 datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
   855 datatype 'c U = E "('c, 'c U) T"
   856 
   857 lemma "P (x::'c U)"
   858   refute
   859 oops
   860 
   861 lemma "\<forall>x::'c U. P x"
   862   refute
   863 oops
   864 
   865 lemma "P (E (C (\<lambda>a. True)))"
   866   refute
   867 oops
   868 
   869 lemma "P (U_rec_1 e f g h i x)"
   870   refute
   871 oops
   872 
   873 lemma "P (U_rec_2 e f g h i x)"
   874   refute
   875 oops
   876 
   877 lemma "P (U_rec_3 e f g h i x)"
   878   refute
   879 oops
   880 
   881 (******************************************************************************)
   882 
   883 subsection {* Records *}
   884 
   885 (*TODO: make use of pair types, rather than typedef, for record types*)
   886 
   887 record ('a, 'b) point =
   888   xpos :: 'a
   889   ypos :: 'b
   890 
   891 lemma "(x::('a, 'b) point) = y"
   892   refute
   893 oops
   894 
   895 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
   896   ext :: 'c
   897 
   898 lemma "(x::('a, 'b, 'c) extpoint) = y"
   899   refute
   900 oops
   901 
   902 (******************************************************************************)
   903 
   904 subsection {* Inductively defined sets *}
   905 
   906 consts
   907   arbitrarySet :: "'a set"
   908 inductive arbitrarySet
   909 intros
   910   "arbitrary : arbitrarySet"
   911 
   912 lemma "x : arbitrarySet"
   913   refute
   914 oops
   915 
   916 consts
   917   evenCard :: "'a set set"
   918 inductive evenCard
   919 intros
   920   "{} : evenCard"
   921   "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
   922 
   923 lemma "S : evenCard"
   924   refute
   925 oops
   926 
   927 consts
   928   even :: "nat set"
   929   odd  :: "nat set"
   930 inductive even odd
   931 intros
   932   "0 : even"
   933   "n : even \<Longrightarrow> Suc n : odd"
   934   "n : odd \<Longrightarrow> Suc n : even"
   935 
   936 lemma "n : odd"
   937   (*refute*)  -- {* unfortunately, this little example already takes too long *}
   938 oops
   939 
   940 (******************************************************************************)
   941 
   942 subsection {* Examples involving special functions *}
   943 
   944 lemma "card x = 0"
   945   refute
   946 oops
   947 
   948 lemma "finite x"
   949   refute  -- {* no finite countermodel exists *}
   950 oops
   951 
   952 lemma "(x::nat) + y = 0"
   953   refute
   954 oops
   955 
   956 lemma "(x::nat) = x + x"
   957   refute
   958 oops
   959 
   960 lemma "(x::nat) - y + y = x"
   961   refute
   962 oops
   963 
   964 lemma "(x::nat) = x * x"
   965   refute
   966 oops
   967 
   968 lemma "(x::nat) < x + y"
   969   refute
   970 oops
   971 
   972 lemma "a @ [] = b @ []"
   973   refute
   974 oops
   975 
   976 lemma "a @ b = b @ a"
   977   refute
   978 oops
   979 
   980 lemma "f (lfp f) = lfp f"
   981   refute
   982 oops
   983 
   984 lemma "f (gfp f) = gfp f"
   985   refute
   986 oops
   987 
   988 lemma "lfp f = gfp f"
   989   refute
   990 oops
   991 
   992 (******************************************************************************)
   993 
   994 subsection {* Axiomatic type classes and overloading *}
   995 
   996 text {* A type class without axioms: *}
   997 
   998 axclass classA
   999 
  1000 lemma "P (x::'a::classA)"
  1001   refute
  1002 oops
  1003 
  1004 text {* The axiom of this type class does not contain any type variables, but is internally converted into one that does: *}
  1005 
  1006 axclass classB
  1007   classB_ax: "P | ~ P"
  1008 
  1009 lemma "P (x::'a::classB)"
  1010   refute
  1011 oops
  1012 
  1013 text {* An axiom with a type variable (denoting types which have at least two elements): *}
  1014 
  1015 axclass classC < type
  1016   classC_ax: "\<exists>x y. x \<noteq> y"
  1017 
  1018 lemma "P (x::'a::classC)"
  1019   refute
  1020 oops
  1021 
  1022 lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
  1023   refute  -- {* no countermodel exists *}
  1024 oops
  1025 
  1026 text {* A type class for which a constant is defined: *}
  1027 
  1028 consts
  1029   classD_const :: "'a \<Rightarrow> 'a"
  1030 
  1031 axclass classD < type
  1032   classD_ax: "classD_const (classD_const x) = classD_const x"
  1033 
  1034 lemma "P (x::'a::classD)"
  1035   refute
  1036 oops
  1037 
  1038 text {* A type class with multiple superclasses: *}
  1039 
  1040 axclass classE < classC, classD
  1041 
  1042 lemma "P (x::'a::classE)"
  1043   refute
  1044 oops
  1045 
  1046 lemma "P (x::'a::{classB, classE})"
  1047   refute
  1048 oops
  1049 
  1050 text {* OFCLASS: *}
  1051 
  1052 lemma "OFCLASS('a::type, type_class)"
  1053   refute  -- {* no countermodel exists *}
  1054   apply intro_classes
  1055 done
  1056 
  1057 lemma "OFCLASS('a::classC, type_class)"
  1058   refute  -- {* no countermodel exists *}
  1059   apply intro_classes
  1060 done
  1061 
  1062 lemma "OFCLASS('a, classB_class)"
  1063   refute  -- {* no countermodel exists *}
  1064   apply intro_classes
  1065   apply simp
  1066 done
  1067 
  1068 lemma "OFCLASS('a::type, classC_class)"
  1069   refute
  1070 oops
  1071 
  1072 text {* Overloading: *}
  1073 
  1074 consts inverse :: "'a \<Rightarrow> 'a"
  1075 
  1076 defs (overloaded)
  1077   inverse_bool: "inverse (b::bool)   == ~ b"
  1078   inverse_set : "inverse (S::'a set) == -S"
  1079   inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
  1080 
  1081 lemma "inverse b"
  1082   refute
  1083 oops
  1084 
  1085 lemma "P (inverse (S::'a set))"
  1086   refute
  1087 oops
  1088 
  1089 lemma "P (inverse (p::'a\<times>'b))"
  1090   refute
  1091 oops
  1092 
  1093 refute_params [satsolver="auto"]
  1094 
  1095 end