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

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

added lemmas

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