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