Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/HOL/HOL-eg.txt
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 6580 ff2c3ffd38ee
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2 
     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!
wneuper/isa