--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Holcfb.ML Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,152 @@
+(* Title: HOLCF/holcfb.ML
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Lemmas for Holcfb.thy
+*)
+
+open Holcfb;
+
+(* ------------------------------------------------------------------------ *)
+(* <::nat=>nat=>bool is well-founded *)
+(* ------------------------------------------------------------------------ *)
+
+val well_founded_nat = prove_goal Nat.thy
+ "!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
+ (fn prems =>
+ [
+ (res_inst_tac [("n","x")] less_induct 1),
+ (strip_tac 1),
+ (res_inst_tac [("Q","? k.k<n & P(k)")] (excluded_middle RS disjE) 1),
+ (etac exE 2),
+ (etac conjE 2),
+ (rtac mp 2),
+ (etac allE 2),
+ (etac impE 2),
+ (atac 2),
+ (etac spec 2),
+ (atac 2),
+ (res_inst_tac [("x","n")] exI 1),
+ (rtac conjI 1),
+ (atac 1),
+ (strip_tac 1),
+ (rtac leI 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* Lemmas for selecting the least element in a nonempty set *)
+(* ------------------------------------------------------------------------ *)
+
+val theleast = prove_goalw Holcfb.thy [theleast_def]
+"P(x) ==> P(theleast(P)) & (!x.P(x)--> theleast(P) <= x)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac (well_founded_nat RS spec RS mp RS exE) 1),
+ (atac 1),
+ (rtac selectI 1),
+ (atac 1)
+ ]);
+
+val theleast1= theleast RS conjunct1;
+(* ?P1(?x1) ==> ?P1(theleast(?P1)) *)
+
+val theleast2 = prove_goal Holcfb.thy "P(x) ==> theleast(P) <= x"
+ (fn prems =>
+ [
+ (rtac (theleast RS conjunct2 RS spec RS mp) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1)
+ ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* Some lemmas in HOL.thy *)
+(* ------------------------------------------------------------------------ *)
+
+
+val de_morgan1 = prove_goal HOL.thy "(~a & ~b)=(~(a | b))"
+(fn prems =>
+ [
+ (rtac iffI 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val de_morgan2 = prove_goal HOL.thy "(~a | ~b)=(~(a & b))"
+(fn prems =>
+ [
+ (rtac iffI 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
+val notall2ex = prove_goal HOL.thy "(~ (!x.P(x))) = (? x.~P(x))"
+(fn prems =>
+ [
+ (rtac iffI 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val notex2all = prove_goal HOL.thy "(~ (? x.P(x))) = (!x.~P(x))"
+(fn prems =>
+ [
+ (rtac iffI 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
+val selectI2 = prove_goal HOL.thy "(? x. P(x)) ==> P(@ x.P(x))"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac exE 1),
+ (etac selectI 1)
+ ]);
+
+val selectE = prove_goal HOL.thy "P(@ x.P(x)) ==> (? x. P(x))"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac exI 1)
+ ]);
+
+val select_eq_Ex = prove_goal HOL.thy "(P(@ x.P(x))) = (? x. P(x))"
+(fn prems =>
+ [
+ (rtac (iff RS mp RS mp) 1),
+ (strip_tac 1),
+ (etac selectE 1),
+ (strip_tac 1),
+ (etac selectI2 1)
+ ]);
+
+
+val notnotI = prove_goal HOL.thy "P ==> ~~P"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
+val classical2 = prove_goal HOL.thy "[|Q ==> R; ~Q ==> R|]==>R"
+ (fn prems =>
+ [
+ (rtac disjE 1),
+ (rtac excluded_middle 1),
+ (eresolve_tac prems 1),
+ (eresolve_tac prems 1)
+ ]);
+
+
+
+val classical3 = (notE RS notI);
+(* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
+