src/HOL/ex/Guess.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 20005 3fd6d57b16de
child 41460 ea56b98aee83
permissions -rw-r--r--
added lemmas
     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