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

src/HOL/ex/Guess.thy

author | haftmann |

Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) | |

changeset 58646 | cd63a4b12a33 |

parent 41460 | ea56b98aee83 |

child 58889 | 5b7a9633cfa8 |

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

specialized specification: avoid trivial instances

1 (*

2 Author: Makarius

3 *)

5 header {* Proof by guessing *}

7 theory Guess

8 imports Main

9 begin

11 lemma True

12 proof

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

16 from 1 guess ..

17 from 1 guess x ..

18 from 1 guess x :: 'a ..

19 from 1 guess x :: nat ..

21 have 2: "\<exists>x y. x = x & y = y" by simp

22 from 2 guess apply - apply (erule exE conjE)+ done

23 from 2 guess x apply - apply (erule exE conjE)+ done

24 from 2 guess x y apply - apply (erule exE conjE)+ done

25 from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done

26 from 2 guess x y :: nat apply - apply (erule exE conjE)+ done

28 qed

30 end