src/HOL/ex/Guess.thy
author wenzelm
Tue Jul 04 19:49:56 2006 +0200 (2006-07-04)
changeset 20005 3fd6d57b16de
child 41460 ea56b98aee83
permissions -rw-r--r--
Proof by guessing.
     1 (*
     2     ID:         $Id$
     3     Author:     Makarius
     4 *)
     5 
     6 header {* Proof by guessing *}
     7 
     8 theory Guess
     9 imports Main
    10 begin
    11 
    12 lemma True
    13 proof
    14 
    15   have 1: "\<exists>x. x = x" by simp
    16 
    17   from 1 guess ..
    18   from 1 guess x ..
    19   from 1 guess x :: 'a ..
    20   from 1 guess x :: nat ..
    21 
    22   have 2: "\<exists>x y. x = x & y = y" by simp
    23   from 2 guess apply - apply (erule exE conjE)+ done
    24   from 2 guess x apply - apply (erule exE conjE)+ done
    25   from 2 guess x y apply - apply (erule exE conjE)+ done
    26   from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
    27   from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
    28 
    29 qed
    30 
    31 end