equal
deleted
inserted
replaced
6 |
6 |
7 theory Guess |
7 theory Guess |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 lemma True |
11 notepad |
12 proof |
12 begin |
13 |
|
14 have 1: "\<exists>x. x = x" by simp |
13 have 1: "\<exists>x. x = x" by simp |
15 |
14 |
16 from 1 guess .. |
15 from 1 guess .. |
17 from 1 guess x .. |
16 from 1 guess x .. |
18 from 1 guess x :: 'a .. |
17 from 1 guess x :: 'a .. |
19 from 1 guess x :: nat .. |
18 from 1 guess x :: nat .. |
20 |
19 |
21 have 2: "\<exists>x y. x = x & y = y" by simp |
20 have 2: "\<exists>x y. x = x \<and> y = y" by simp |
22 from 2 guess apply - apply (erule exE conjE)+ done |
21 from 2 guess apply - apply (erule exE conjE)+ done |
23 from 2 guess x apply - apply (erule exE conjE)+ done |
22 from 2 guess x apply - apply (erule exE conjE)+ done |
24 from 2 guess x y apply - apply (erule exE conjE)+ done |
23 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 |
24 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 |
25 from 2 guess x y :: nat apply - apply (erule exE conjE)+ done |
27 |
26 end |
28 qed |
|
29 |
27 |
30 end |
28 end |