104

1 
(**** HOL examples  process using Doc/tout HOLeg.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!
