src/HOL/ex/Guess.thy
author bulwahn
Fri Jan 07 14:46:28 2011 +0100 (2011-01-07)
changeset 41460 ea56b98aee83
parent 20005 3fd6d57b16de
child 58889 5b7a9633cfa8
permissions -rw-r--r--
removing obselete Id comments from HOL/ex theories
     1 (*
     2     Author:     Makarius
     3 *)
     4 
     5 header {* Proof by guessing *}
     6 
     7 theory Guess
     8 imports Main
     9 begin
    10 
    11 lemma True
    12 proof
    13 
    14   have 1: "\<exists>x. x = x" by simp
    15 
    16   from 1 guess ..
    17   from 1 guess x ..
    18   from 1 guess x :: 'a ..
    19   from 1 guess x :: nat ..
    20 
    21   have 2: "\<exists>x y. x = x & y = y" by simp
    22   from 2 guess apply - apply (erule exE conjE)+ done
    23   from 2 guess x apply - apply (erule exE conjE)+ done
    24   from 2 guess x y apply - apply (erule exE conjE)+ done
    25   from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
    26   from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
    27 
    28 qed
    29 
    30 end