src/HOL/ex/Guess.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 20005 3fd6d57b16de child 41460 ea56b98aee83 permissions -rw-r--r--
```     1 (*
```
```     2     ID:         \$Id\$
```
```     3     Author:     Makarius
```
```     4 *)
```
```     5
```
```     6 header {* Proof by guessing *}
```
```     7
```
```     8 theory Guess
```
```     9 imports Main
```
```    10 begin
```
```    11
```
```    12 lemma True
```
```    13 proof
```
```    14
```
```    15   have 1: "\<exists>x. x = x" by simp
```
```    16
```
```    17   from 1 guess ..
```
```    18   from 1 guess x ..
```
```    19   from 1 guess x :: 'a ..
```
```    20   from 1 guess x :: nat ..
```
```    21
```
```    22   have 2: "\<exists>x y. x = x & y = y" by simp
```
```    23   from 2 guess apply - apply (erule exE conjE)+ done
```
```    24   from 2 guess x apply - apply (erule exE conjE)+ done
```
```    25   from 2 guess x y apply - apply (erule exE conjE)+ done
```
```    26   from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
```
```    27   from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
```
```    28
```
```    29 qed
```
```    30
```
```    31 end
```