105

1 
(* Deriving an inference rule *)


2 


3 
Pretty.setmargin 72; (*existing macros just allow this margin*)


4 
print_depth 0;


5 


6 

14148

7 
val [major,minor] = goal IFOL.thy

105

8 
"[ P&Q; [ P; Q ] ==> R ] ==> R";


9 
prth minor;


10 
by (resolve_tac [minor] 1);


11 
prth major;


12 
prth (major RS conjunct1);


13 
by (resolve_tac [major RS conjunct1] 1);


14 
prth (major RS conjunct2);


15 
by (resolve_tac [major RS conjunct2] 1);


16 
prth (topthm());


17 
val conjE = prth(result());


18 


19 


20 
 val [major,minor] = goal Int_Rule.thy


21 
= "[ P&Q; [ P; Q ] ==> R ] ==> R";


22 
Level 0


23 
R


24 
1. R


25 
val major = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm


26 
val minor = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm


27 
 prth minor;


28 
[ P; Q ] ==> R [[ P; Q ] ==> R]


29 
 by (resolve_tac [minor] 1);


30 
Level 1


31 
R


32 
1. P


33 
2. Q


34 
 prth major;


35 
P & Q [P & Q]


36 
 prth (major RS conjunct1);


37 
P [P & Q]


38 
 by (resolve_tac [major RS conjunct1] 1);


39 
Level 2


40 
R


41 
1. Q


42 
 prth (major RS conjunct2);


43 
Q [P & Q]


44 
 by (resolve_tac [major RS conjunct2] 1);


45 
Level 3


46 
R


47 
No subgoals!


48 
 prth (topthm());


49 
R [P & Q, P & Q, [ P; Q ] ==> R]


50 
 val conjE = prth(result());


51 
[ ?P & ?Q; [ ?P; ?Q ] ==> ?R ] ==> ?R


52 
val conjE = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm


53 


54 


55 
(*** Derived rules involving definitions ***)


56 


57 
(** notI **)


58 


59 
val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";


60 
prth not_def;


61 
by (rewrite_goals_tac [not_def]);


62 
by (resolve_tac [impI] 1);


63 
by (resolve_tac prems 1);


64 
by (assume_tac 1);


65 
val notI = prth(result());


66 


67 
val prems = goalw Int_Rule.thy [not_def]


68 
"(P ==> False) ==> ~P";


69 


70 


71 
 prth not_def;


72 
~?P == ?P > False


73 
 val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";


74 
Level 0


75 
~P


76 
1. ~P


77 
 by (rewrite_goals_tac [not_def]);


78 
Level 1


79 
~P


80 
1. P > False


81 
 by (resolve_tac [impI] 1);


82 
Level 2


83 
~P


84 
1. P ==> False


85 
 by (resolve_tac prems 1);


86 
Level 3


87 
~P


88 
1. P ==> P


89 
 by (assume_tac 1);


90 
Level 4


91 
~P


92 
No subgoals!


93 
 val notI = prth(result());


94 
(?P ==> False) ==> ~?P


95 
val notI = # : thm


96 


97 
 val prems = goalw Int_Rule.thy [not_def]


98 
= "(P ==> False) ==> ~P";


99 
Level 0


100 
~P


101 
1. P > False


102 


103 


104 
(** notE **)


105 


106 
val [major,minor] = goal Int_Rule.thy "[ ~P; P ] ==> R";


107 
by (resolve_tac [FalseE] 1);


108 
by (resolve_tac [mp] 1);


109 
prth (rewrite_rule [not_def] major);


110 
by (resolve_tac [it] 1);


111 
by (resolve_tac [minor] 1);


112 
val notE = prth(result());


113 


114 
val [major,minor] = goalw Int_Rule.thy [not_def]


115 
"[ ~P; P ] ==> R";


116 
prth (minor RS (major RS mp RS FalseE));


117 
by (resolve_tac [it] 1);


118 


119 


120 
val prems = goalw Int_Rule.thy [not_def]


121 
"[ ~P; P ] ==> R";


122 
prths prems;


123 
by (resolve_tac [FalseE] 1);


124 
by (resolve_tac [mp] 1);


125 
by (resolve_tac prems 1);


126 
by (resolve_tac prems 1);


127 
val notE = prth(result());


128 


129 


130 
 val [major,minor] = goal Int_Rule.thy "[ ~P; P ] ==> R";


131 
Level 0


132 
R


133 
1. R


134 
val major = # : thm


135 
val minor = # : thm


136 
 by (resolve_tac [FalseE] 1);


137 
Level 1


138 
R


139 
1. False


140 
 by (resolve_tac [mp] 1);


141 
Level 2


142 
R


143 
1. ?P1 > False


144 
2. ?P1


145 
 prth (rewrite_rule [not_def] major);


146 
P > False [~P]


147 
 by (resolve_tac [it] 1);


148 
Level 3


149 
R


150 
1. P


151 
 by (resolve_tac [minor] 1);


152 
Level 4


153 
R


154 
No subgoals!


155 
 val notE = prth(result());


156 
[ ~?P; ?P ] ==> ?R


157 
val notE = # : thm


158 
 val [major,minor] = goalw Int_Rule.thy [not_def]


159 
= "[ ~P; P ] ==> R";


160 
Level 0


161 
R


162 
1. R


163 
val major = # : thm


164 
val minor = # : thm


165 
 prth (minor RS (major RS mp RS FalseE));


166 
?P [P, ~P]


167 
 by (resolve_tac [it] 1);


168 
Level 1


169 
R


170 
No subgoals!


171 


172 


173 


174 


175 
 goal Int_Rule.thy "[ ~P; P ] ==> R";


176 
Level 0


177 
R


178 
1. R


179 
 prths (map (rewrite_rule [not_def]) it);


180 
P > False [~P]


181 


182 
P [P]


183 


184 
 val prems = goalw Int_Rule.thy [not_def]


185 
= "[ ~P; P ] ==> R";


186 
Level 0


187 
R


188 
1. R


189 
val prems = # : thm list


190 
 prths prems;


191 
P > False [~P]


192 


193 
P [P]


194 


195 
 by (resolve_tac [mp RS FalseE] 1);


196 
Level 1


197 
R


198 
1. ?P1 > False


199 
2. ?P1


200 
 by (resolve_tac prems 1);


201 
Level 2


202 
R


203 
1. P


204 
 by (resolve_tac prems 1);


205 
Level 3


206 
R


207 
No subgoals!


208 
 val notE = prth(result());


209 
[ ~?P; ?P ] ==> ?R


210 
val notE = # : thm
