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
 wenzelm@20005 ` 1` ```(* ``` wenzelm@20005 ` 2` ``` Author: Makarius ``` wenzelm@20005 ` 3` ```*) ``` wenzelm@20005 ` 4` wenzelm@20005 ` 5` ```header {* Proof by guessing *} ``` wenzelm@20005 ` 6` wenzelm@20005 ` 7` ```theory Guess ``` wenzelm@20005 ` 8` ```imports Main ``` wenzelm@20005 ` 9` ```begin ``` wenzelm@20005 ` 10` wenzelm@20005 ` 11` ```lemma True ``` wenzelm@20005 ` 12` ```proof ``` wenzelm@20005 ` 13` wenzelm@20005 ` 14` ``` have 1: "\x. x = x" by simp ``` wenzelm@20005 ` 15` wenzelm@20005 ` 16` ``` from 1 guess .. ``` wenzelm@20005 ` 17` ``` from 1 guess x .. ``` wenzelm@20005 ` 18` ``` from 1 guess x :: 'a .. ``` wenzelm@20005 ` 19` ``` from 1 guess x :: nat .. ``` wenzelm@20005 ` 20` wenzelm@20005 ` 21` ``` have 2: "\x y. x = x & y = y" by simp ``` wenzelm@20005 ` 22` ``` from 2 guess apply - apply (erule exE conjE)+ done ``` wenzelm@20005 ` 23` ``` from 2 guess x apply - apply (erule exE conjE)+ done ``` wenzelm@20005 ` 24` ``` from 2 guess x y apply - apply (erule exE conjE)+ done ``` wenzelm@20005 ` 25` ``` from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done ``` wenzelm@20005 ` 26` ``` from 2 guess x y :: nat apply - apply (erule exE conjE)+ done ``` wenzelm@20005 ` 27` wenzelm@20005 ` 28` ```qed ``` wenzelm@20005 ` 29` wenzelm@20005 ` 30` ```end ```