1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/HOL/HOL-eg.txt	Tue May 04 18:03:56 1999 +0200
     1.3 @@ -0,0 +1,151 @@
     1.4 +(**** HOL examples -- process using Doc/tout HOL-eg.txt  ****)
     1.5 +
     1.6 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
     1.7 +print_depth 0;
     1.8 +
     1.9 +
    1.10 +(*** Conjunction rules ***)
    1.11 +
    1.12 +val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q";
    1.13 +by (resolve_tac [and_def RS ssubst] 1);
    1.14 +by (resolve_tac [allI] 1);
    1.15 +by (resolve_tac [impI] 1);
    1.16 +by (eresolve_tac [mp RS mp] 1);
    1.17 +by (REPEAT (resolve_tac prems 1));
    1.18 +val conjI = result();
    1.19 +
    1.20 +val prems = goal HOL_Rule.thy "[| P & Q |] ==> P";
    1.21 +prths (prems RL [and_def RS subst]);
    1.22 +prths (prems RL [and_def RS subst] RL [spec] RL [mp]);
    1.23 +by (resolve_tac it 1);
    1.24 +by (REPEAT (ares_tac [impI] 1));
    1.25 +val conjunct1 = result();
    1.26 +
    1.27 +
    1.28 +(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
    1.29 +
    1.30 +goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
    1.31 +by (resolve_tac [notI] 1);
    1.32 +by (eresolve_tac [rangeE] 1);
    1.33 +by (eresolve_tac [equalityCE] 1);
    1.34 +by (dresolve_tac [CollectD] 1);
    1.35 +by (contr_tac 1);
    1.36 +by (swap_res_tac [CollectI] 1);
    1.37 +by (assume_tac 1);
    1.38 +
    1.39 +choplev 0;
    1.40 +by (best_tac (set_cs addSEs [equalityCE]) 1);
    1.41 +
    1.42 +
    1.43 +goal Set.thy "! f:: 'a=>'a set. ! x. ~ f(x) = ?S(f)";
    1.44 +by (REPEAT (resolve_tac [allI,notI] 1));
    1.45 +by (eresolve_tac [equalityCE] 1);
    1.46 +by (dresolve_tac [CollectD] 1);
    1.47 +by (contr_tac 1);
    1.48 +by (swap_res_tac [CollectI] 1);
    1.49 +by (assume_tac 1);
    1.50 +
    1.51 +choplev 0;
    1.52 +by (best_tac (set_cs addSEs [equalityCE]) 1);
    1.53 +
    1.54 +
    1.55 +goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? a. f(a) = S)";
    1.56 +by (best_tac (set_cs addSEs [equalityCE]) 1);
    1.57 +
    1.58 +
    1.59 +
    1.60 +
    1.61 +> val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q";
    1.62 +Level 0
    1.63 +P & Q
    1.64 + 1. P & Q
    1.65 +> by (resolve_tac [and_def RS ssubst] 1);
    1.66 +Level 1
    1.67 +P & Q
    1.68 + 1. ! R. (P --> Q --> R) --> R
    1.69 +> by (resolve_tac [allI] 1);
    1.70 +Level 2
    1.71 +P & Q
    1.72 + 1. !!R. (P --> Q --> R) --> R
    1.73 +> by (resolve_tac [impI] 1);
    1.74 +Level 3
    1.75 +P & Q
    1.76 + 1. !!R. P --> Q --> R ==> R
    1.77 +> by (eresolve_tac [mp RS mp] 1);
    1.78 +Level 4
    1.79 +P & Q
    1.80 + 1. !!R. P
    1.81 + 2. !!R. Q
    1.82 +> by (REPEAT (resolve_tac prems 1));
    1.83 +Level 5
    1.84 +P & Q
    1.85 +No subgoals!
    1.86 +
    1.87 +
    1.88 +
    1.89 +> val prems = goal HOL_Rule.thy "[| P & Q |] ==> P";
    1.90 +Level 0
    1.91 +P
    1.92 + 1. P
    1.93 +> prths (prems RL [and_def RS subst]);
    1.94 +! R. (P --> Q --> R) --> R  [P & Q]
    1.95 +P & Q  [P & Q]
    1.96 +
    1.97 +> prths (prems RL [and_def RS subst] RL [spec] RL [mp]);
    1.98 +P --> Q --> ?Q ==> ?Q  [P & Q]
    1.99 +
   1.100 +> by (resolve_tac it 1);
   1.101 +Level 1
   1.102 +P
   1.103 + 1. P --> Q --> P
   1.104 +> by (REPEAT (ares_tac [impI] 1));
   1.105 +Level 2
   1.106 +P
   1.107 +No subgoals!
   1.108 +
   1.109 +
   1.110 +
   1.111 +
   1.112 +> goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
   1.113 +Level 0
   1.114 +~?S : range(f)
   1.115 + 1. ~?S : range(f)
   1.116 +> by (resolve_tac [notI] 1);
   1.117 +Level 1
   1.118 +~?S : range(f)
   1.119 + 1. ?S : range(f) ==> False
   1.120 +> by (eresolve_tac [rangeE] 1);
   1.121 +Level 2
   1.122 +~?S : range(f)
   1.123 + 1. !!x. ?S = f(x) ==> False
   1.124 +> by (eresolve_tac [equalityCE] 1);
   1.125 +Level 3
   1.126 +~?S : range(f)
   1.127 + 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False
   1.128 + 2. !!x. [| ~?c3(x) : ?S; ~?c3(x) : f(x) |] ==> False
   1.129 +> by (dresolve_tac [CollectD] 1);
   1.130 +Level 4
   1.131 +~{x. ?P7(x)} : range(f)
   1.132 + 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False
   1.133 + 2. !!x. [| ~?c3(x) : {x. ?P7(x)}; ~?c3(x) : f(x) |] ==> False
   1.134 +> by (contr_tac 1);
   1.135 +Level 5
   1.136 +~{x. ~x : f(x)} : range(f)
   1.137 + 1. !!x. [| ~x : {x. ~x : f(x)}; ~x : f(x) |] ==> False
   1.138 +> by (swap_res_tac [CollectI] 1);
   1.139 +Level 6
   1.140 +~{x. ~x : f(x)} : range(f)
   1.141 + 1. !!x. [| ~x : f(x); ~False |] ==> ~x : f(x)
   1.142 +> by (assume_tac 1);
   1.143 +Level 7
   1.144 +~{x. ~x : f(x)} : range(f)
   1.145 +No subgoals!
   1.146 +
   1.147 +> choplev 0;
   1.148 +Level 0
   1.149 +~?S : range(f)
   1.150 + 1. ~?S : range(f)
   1.151 +> by (best_tac (set_cs addSEs [equalityCE]) 1);
   1.152 +Level 1
   1.153 +~{x. ~x : f(x)} : range(f)
   1.154 +No subgoals!