9869

1 
(* Title: HOL/meson_lemmas.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Lemmas for Meson.


7 
*)


8 


9 
(* "Axiom" of Choice, proved using the description operator *)


10 


11 
Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";

9970

12 
by (fast_tac (claset() addEs [someI]) 1);

9869

13 
qed "choice";


14 


15 


16 
(* Generation of contrapositives *)


17 


18 
(*Inserts negated disjunct after removing the negation; P is a literal*)


19 
val [major,minor] = Goal "~PQ ==> ((~P==>P) ==> Q)";


20 
by (rtac (major RS disjE) 1);


21 
by (rtac notE 1);


22 
by (etac minor 2);


23 
by (ALLGOALS assume_tac);


24 
qed "make_neg_rule";


25 


26 
(*For Plaisted's "Postive refinement" of the MESON procedure*)


27 
Goal "~PQ ==> (P ==> Q)";


28 
by (Blast_tac 1);


29 
qed "make_refined_neg_rule";


30 


31 
(*P should be a literal*)


32 
val [major,minor] = Goal "PQ ==> ((P==>~P) ==> Q)";


33 
by (rtac (major RS disjE) 1);


34 
by (rtac notE 1);


35 
by (etac minor 1);


36 
by (ALLGOALS assume_tac);


37 
qed "make_pos_rule";


38 


39 


40 
(* Generation of a goal clause  put away the final literal *)


41 


42 
val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";


43 
by (rtac notE 1);


44 
by (rtac minor 2);


45 
by (ALLGOALS (rtac major));


46 
qed "make_neg_goal";


47 


48 
val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";


49 
by (rtac notE 1);


50 
by (rtac minor 1);


51 
by (ALLGOALS (rtac major));


52 
qed "make_pos_goal";


53 


54 


55 
(* Lemmas for forward proof (like congruence rules) *)


56 


57 
(*NOTE: could handle conjunctions (faster?) by


58 
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)


59 
val major::prems = Goal


60 
"[ P'&Q'; P' ==> P; Q' ==> Q ] ==> P&Q";


61 
by (rtac (major RS conjE) 1);


62 
by (rtac conjI 1);


63 
by (ALLGOALS (eresolve_tac prems));


64 
qed "conj_forward";


65 


66 
val major::prems = Goal


67 
"[ P'Q'; P' ==> P; Q' ==> Q ] ==> PQ";


68 
by (rtac (major RS disjE) 1);


69 
by (ALLGOALS (dresolve_tac prems));


70 
by (ALLGOALS (eresolve_tac [disjI1,disjI2]));


71 
qed "disj_forward";


72 


73 
(*Version for removal of duplicate literals*)


74 
val major::prems = Goal


75 
"[ P'Q'; P' ==> P; [ Q'; P==>False ] ==> Q ] ==> PQ";


76 
by (cut_facts_tac [major] 1);


77 
by (blast_tac (claset() addIs prems) 1);


78 
qed "disj_forward2";


79 


80 
val major::prems = Goal


81 
"[ ALL x. P'(x); !!x. P'(x) ==> P(x) ] ==> ALL x. P(x)";


82 
by (rtac allI 1);


83 
by (resolve_tac prems 1);


84 
by (rtac (major RS spec) 1);


85 
qed "all_forward";


86 


87 
val major::prems = Goal


88 
"[ EX x. P'(x); !!x. P'(x) ==> P(x) ] ==> EX x. P(x)";


89 
by (rtac (major RS exE) 1);


90 
by (rtac exI 1);


91 
by (eresolve_tac prems 1);


92 
qed "ex_forward";
