src/HOL/ex/Guess.thy
changeset 20005 3fd6d57b16de
child 41460 ea56b98aee83
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Guess.thy	Tue Jul 04 19:49:56 2006 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +(*
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +*)
     1.8 +
     1.9 +header {* Proof by guessing *}
    1.10 +
    1.11 +theory Guess
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +lemma True
    1.16 +proof
    1.17 +
    1.18 +  have 1: "\<exists>x. x = x" by simp
    1.19 +
    1.20 +  from 1 guess ..
    1.21 +  from 1 guess x ..
    1.22 +  from 1 guess x :: 'a ..
    1.23 +  from 1 guess x :: nat ..
    1.24 +
    1.25 +  have 2: "\<exists>x y. x = x & y = y" by simp
    1.26 +  from 2 guess apply - apply (erule exE conjE)+ done
    1.27 +  from 2 guess x apply - apply (erule exE conjE)+ done
    1.28 +  from 2 guess x y apply - apply (erule exE conjE)+ done
    1.29 +  from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
    1.30 +  from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
    1.31 +
    1.32 +qed
    1.33 +
    1.34 +end