summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Guess.thy

author | wenzelm |

Tue Jul 04 19:49:56 2006 +0200 (2006-07-04) | |

changeset 20005 | 3fd6d57b16de |

child 41460 | ea56b98aee83 |

permissions | -rw-r--r-- |

Proof by guessing.

1 (*

2 ID: $Id$

3 Author: Makarius

4 *)

6 header {* Proof by guessing *}

8 theory Guess

9 imports Main

10 begin

12 lemma True

13 proof

15 have 1: "\<exists>x. x = x" by simp

17 from 1 guess ..

18 from 1 guess x ..

19 from 1 guess x :: 'a ..

20 from 1 guess x :: nat ..

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

29 qed

31 end