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

src/HOL/ex/Guess.thy

author | bulwahn |

Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) | |

changeset 45231 | d85a2fdc586c |

parent 41460 | ea56b98aee83 |

child 58889 | 5b7a9633cfa8 |

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

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

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