doc-src/HOL/HOL-eg.txt
author wenzelm
Sat Apr 30 20:48:29 2011 +0200 (2011-04-30)
changeset 42506 876887b07e8d
parent 6580 ff2c3ffd38ee
permissions -rw-r--r--
more robust error handling (NB: Source.source requires total scanner or recover);
tuned;
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!