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!