src/HOL/ex/Guess.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61343 5b5656a63bd6
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*
     2     Author:     Makarius
     3 *)
     4 
     5 section \<open>Proof by guessing\<close>
     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