src/HOL/ex/Guess.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 41460 ea56b98aee83
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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