author | Walther Neuper <neuper@ist.tugraz.at> |
Thu, 12 Aug 2010 15:03:34 +0200 | |
branch | isac-from-Isabelle2009-2 |
changeset 37913 | 20e3616b2d9c |
parent 6580 | ff2c3ffd38ee |
permissions | -rw-r--r-- |
wenzelm@6580 | 1 |
(**** HOL examples -- process using Doc/tout HOL-eg.txt ****) |
wenzelm@6580 | 2 |
|
wenzelm@6580 | 3 |
Pretty.setmargin 72; (*existing macros just allow this margin*) |
wenzelm@6580 | 4 |
print_depth 0; |
wenzelm@6580 | 5 |
|
wenzelm@6580 | 6 |
|
wenzelm@6580 | 7 |
(*** Conjunction rules ***) |
wenzelm@6580 | 8 |
|
wenzelm@6580 | 9 |
val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q"; |
wenzelm@6580 | 10 |
by (resolve_tac [and_def RS ssubst] 1); |
wenzelm@6580 | 11 |
by (resolve_tac [allI] 1); |
wenzelm@6580 | 12 |
by (resolve_tac [impI] 1); |
wenzelm@6580 | 13 |
by (eresolve_tac [mp RS mp] 1); |
wenzelm@6580 | 14 |
by (REPEAT (resolve_tac prems 1)); |
wenzelm@6580 | 15 |
val conjI = result(); |
wenzelm@6580 | 16 |
|
wenzelm@6580 | 17 |
val prems = goal HOL_Rule.thy "[| P & Q |] ==> P"; |
wenzelm@6580 | 18 |
prths (prems RL [and_def RS subst]); |
wenzelm@6580 | 19 |
prths (prems RL [and_def RS subst] RL [spec] RL [mp]); |
wenzelm@6580 | 20 |
by (resolve_tac it 1); |
wenzelm@6580 | 21 |
by (REPEAT (ares_tac [impI] 1)); |
wenzelm@6580 | 22 |
val conjunct1 = result(); |
wenzelm@6580 | 23 |
|
wenzelm@6580 | 24 |
|
wenzelm@6580 | 25 |
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
wenzelm@6580 | 26 |
|
wenzelm@6580 | 27 |
goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; |
wenzelm@6580 | 28 |
by (resolve_tac [notI] 1); |
wenzelm@6580 | 29 |
by (eresolve_tac [rangeE] 1); |
wenzelm@6580 | 30 |
by (eresolve_tac [equalityCE] 1); |
wenzelm@6580 | 31 |
by (dresolve_tac [CollectD] 1); |
wenzelm@6580 | 32 |
by (contr_tac 1); |
wenzelm@6580 | 33 |
by (swap_res_tac [CollectI] 1); |
wenzelm@6580 | 34 |
by (assume_tac 1); |
wenzelm@6580 | 35 |
|
wenzelm@6580 | 36 |
choplev 0; |
wenzelm@6580 | 37 |
by (best_tac (set_cs addSEs [equalityCE]) 1); |
wenzelm@6580 | 38 |
|
wenzelm@6580 | 39 |
|
wenzelm@6580 | 40 |
goal Set.thy "! f:: 'a=>'a set. ! x. ~ f(x) = ?S(f)"; |
wenzelm@6580 | 41 |
by (REPEAT (resolve_tac [allI,notI] 1)); |
wenzelm@6580 | 42 |
by (eresolve_tac [equalityCE] 1); |
wenzelm@6580 | 43 |
by (dresolve_tac [CollectD] 1); |
wenzelm@6580 | 44 |
by (contr_tac 1); |
wenzelm@6580 | 45 |
by (swap_res_tac [CollectI] 1); |
wenzelm@6580 | 46 |
by (assume_tac 1); |
wenzelm@6580 | 47 |
|
wenzelm@6580 | 48 |
choplev 0; |
wenzelm@6580 | 49 |
by (best_tac (set_cs addSEs [equalityCE]) 1); |
wenzelm@6580 | 50 |
|
wenzelm@6580 | 51 |
|
wenzelm@6580 | 52 |
goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? a. f(a) = S)"; |
wenzelm@6580 | 53 |
by (best_tac (set_cs addSEs [equalityCE]) 1); |
wenzelm@6580 | 54 |
|
wenzelm@6580 | 55 |
|
wenzelm@6580 | 56 |
|
wenzelm@6580 | 57 |
|
wenzelm@6580 | 58 |
> val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q"; |
wenzelm@6580 | 59 |
Level 0 |
wenzelm@6580 | 60 |
P & Q |
wenzelm@6580 | 61 |
1. P & Q |
wenzelm@6580 | 62 |
> by (resolve_tac [and_def RS ssubst] 1); |
wenzelm@6580 | 63 |
Level 1 |
wenzelm@6580 | 64 |
P & Q |
wenzelm@6580 | 65 |
1. ! R. (P --> Q --> R) --> R |
wenzelm@6580 | 66 |
> by (resolve_tac [allI] 1); |
wenzelm@6580 | 67 |
Level 2 |
wenzelm@6580 | 68 |
P & Q |
wenzelm@6580 | 69 |
1. !!R. (P --> Q --> R) --> R |
wenzelm@6580 | 70 |
> by (resolve_tac [impI] 1); |
wenzelm@6580 | 71 |
Level 3 |
wenzelm@6580 | 72 |
P & Q |
wenzelm@6580 | 73 |
1. !!R. P --> Q --> R ==> R |
wenzelm@6580 | 74 |
> by (eresolve_tac [mp RS mp] 1); |
wenzelm@6580 | 75 |
Level 4 |
wenzelm@6580 | 76 |
P & Q |
wenzelm@6580 | 77 |
1. !!R. P |
wenzelm@6580 | 78 |
2. !!R. Q |
wenzelm@6580 | 79 |
> by (REPEAT (resolve_tac prems 1)); |
wenzelm@6580 | 80 |
Level 5 |
wenzelm@6580 | 81 |
P & Q |
wenzelm@6580 | 82 |
No subgoals! |
wenzelm@6580 | 83 |
|
wenzelm@6580 | 84 |
|
wenzelm@6580 | 85 |
|
wenzelm@6580 | 86 |
> val prems = goal HOL_Rule.thy "[| P & Q |] ==> P"; |
wenzelm@6580 | 87 |
Level 0 |
wenzelm@6580 | 88 |
P |
wenzelm@6580 | 89 |
1. P |
wenzelm@6580 | 90 |
> prths (prems RL [and_def RS subst]); |
wenzelm@6580 | 91 |
! R. (P --> Q --> R) --> R [P & Q] |
wenzelm@6580 | 92 |
P & Q [P & Q] |
wenzelm@6580 | 93 |
|
wenzelm@6580 | 94 |
> prths (prems RL [and_def RS subst] RL [spec] RL [mp]); |
wenzelm@6580 | 95 |
P --> Q --> ?Q ==> ?Q [P & Q] |
wenzelm@6580 | 96 |
|
wenzelm@6580 | 97 |
> by (resolve_tac it 1); |
wenzelm@6580 | 98 |
Level 1 |
wenzelm@6580 | 99 |
P |
wenzelm@6580 | 100 |
1. P --> Q --> P |
wenzelm@6580 | 101 |
> by (REPEAT (ares_tac [impI] 1)); |
wenzelm@6580 | 102 |
Level 2 |
wenzelm@6580 | 103 |
P |
wenzelm@6580 | 104 |
No subgoals! |
wenzelm@6580 | 105 |
|
wenzelm@6580 | 106 |
|
wenzelm@6580 | 107 |
|
wenzelm@6580 | 108 |
|
wenzelm@6580 | 109 |
> goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; |
wenzelm@6580 | 110 |
Level 0 |
wenzelm@6580 | 111 |
~?S : range(f) |
wenzelm@6580 | 112 |
1. ~?S : range(f) |
wenzelm@6580 | 113 |
> by (resolve_tac [notI] 1); |
wenzelm@6580 | 114 |
Level 1 |
wenzelm@6580 | 115 |
~?S : range(f) |
wenzelm@6580 | 116 |
1. ?S : range(f) ==> False |
wenzelm@6580 | 117 |
> by (eresolve_tac [rangeE] 1); |
wenzelm@6580 | 118 |
Level 2 |
wenzelm@6580 | 119 |
~?S : range(f) |
wenzelm@6580 | 120 |
1. !!x. ?S = f(x) ==> False |
wenzelm@6580 | 121 |
> by (eresolve_tac [equalityCE] 1); |
wenzelm@6580 | 122 |
Level 3 |
wenzelm@6580 | 123 |
~?S : range(f) |
wenzelm@6580 | 124 |
1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False |
wenzelm@6580 | 125 |
2. !!x. [| ~?c3(x) : ?S; ~?c3(x) : f(x) |] ==> False |
wenzelm@6580 | 126 |
> by (dresolve_tac [CollectD] 1); |
wenzelm@6580 | 127 |
Level 4 |
wenzelm@6580 | 128 |
~{x. ?P7(x)} : range(f) |
wenzelm@6580 | 129 |
1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False |
wenzelm@6580 | 130 |
2. !!x. [| ~?c3(x) : {x. ?P7(x)}; ~?c3(x) : f(x) |] ==> False |
wenzelm@6580 | 131 |
> by (contr_tac 1); |
wenzelm@6580 | 132 |
Level 5 |
wenzelm@6580 | 133 |
~{x. ~x : f(x)} : range(f) |
wenzelm@6580 | 134 |
1. !!x. [| ~x : {x. ~x : f(x)}; ~x : f(x) |] ==> False |
wenzelm@6580 | 135 |
> by (swap_res_tac [CollectI] 1); |
wenzelm@6580 | 136 |
Level 6 |
wenzelm@6580 | 137 |
~{x. ~x : f(x)} : range(f) |
wenzelm@6580 | 138 |
1. !!x. [| ~x : f(x); ~False |] ==> ~x : f(x) |
wenzelm@6580 | 139 |
> by (assume_tac 1); |
wenzelm@6580 | 140 |
Level 7 |
wenzelm@6580 | 141 |
~{x. ~x : f(x)} : range(f) |
wenzelm@6580 | 142 |
No subgoals! |
wenzelm@6580 | 143 |
|
wenzelm@6580 | 144 |
> choplev 0; |
wenzelm@6580 | 145 |
Level 0 |
wenzelm@6580 | 146 |
~?S : range(f) |
wenzelm@6580 | 147 |
1. ~?S : range(f) |
wenzelm@6580 | 148 |
> by (best_tac (set_cs addSEs [equalityCE]) 1); |
wenzelm@6580 | 149 |
Level 1 |
wenzelm@6580 | 150 |
~{x. ~x : f(x)} : range(f) |
wenzelm@6580 | 151 |
No subgoals! |