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