src/HOL/ex/Guess.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 41460 ea56b98aee83
child 58889 5b7a9633cfa8
permissions -rw-r--r--
introduce order topology
     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