summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 04 Jul 2006 19:49:56 +0200 | |

changeset 20005 | 3fd6d57b16de |

parent 20004 | e6d3f2b031e6 |

child 20006 | 0f507e799938 |

Proof by guessing.

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Guess.thy Tue Jul 04 19:49:56 2006 +0200 @@ -0,0 +1,31 @@ +(* + ID: $Id$ + Author: Makarius +*) + +header {* Proof by guessing *} + +theory Guess +imports Main +begin + +lemma True +proof + + have 1: "\<exists>x. x = x" by simp + + from 1 guess .. + from 1 guess x .. + from 1 guess x :: 'a .. + from 1 guess x :: nat .. + + have 2: "\<exists>x y. x = x & y = y" by simp + from 2 guess apply - apply (erule exE conjE)+ done + from 2 guess x apply - apply (erule exE conjE)+ done + from 2 guess x y apply - apply (erule exE conjE)+ done + from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done + from 2 guess x y :: nat apply - apply (erule exE conjE)+ done + +qed + +end