src/HOL/ex/Guess.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 59031 4c3bb56b8ce7
child 61343 5b5656a63bd6
permissions -rw-r--r--
prefer symbols;
     1 (*
     2     Author:     Makarius
     3 *)
     4 
     5 section {* Proof by guessing *}
     6 
     7 theory Guess
     8 imports Main
     9 begin
    10 
    11 notepad
    12 begin
    13   have 1: "\<exists>x. x = x" by simp
    14 
    15   from 1 guess ..
    16   from 1 guess x ..
    17   from 1 guess x :: 'a ..
    18   from 1 guess x :: nat ..
    19 
    20   have 2: "\<exists>x y. x = x \<and> y = y" by simp
    21   from 2 guess apply - apply (erule exE conjE)+ done
    22   from 2 guess x apply - apply (erule exE conjE)+ done
    23   from 2 guess x y apply - apply (erule exE conjE)+ done
    24   from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
    25   from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
    26 end
    27 
    28 end