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