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