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
```