--- a/src/HOL/HOL.ML Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/HOL.ML Wed Apr 17 17:59:58 1996 +0200
@@ -11,6 +11,7 @@
(** Equality **)
+section "=";
qed_goal "sym" HOL.thy "s=t ==> t=s"
(fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
@@ -34,7 +35,9 @@
(rtac sym 1),
(REPEAT (resolve_tac prems 1)) ]);
+
(** Congruence rules for meta-application **)
+section "Congruence";
(*similar to AP_THM in Gordon's HOL*)
qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
@@ -49,7 +52,9 @@
(fn [prem1,prem2] =>
[rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
+
(** Equality of booleans -- iff **)
+section "iff";
qed_goal "iffI" HOL.thy
"[| P ==> Q; Q ==> P |] ==> P=Q"
@@ -65,7 +70,9 @@
"[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
(fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
+
(** True **)
+section "True";
qed_goalw "TrueI" HOL.thy [True_def] "True"
(fn _ => [rtac refl 1]);
@@ -76,7 +83,9 @@
qed_goal "eqTrueE" HOL.thy "P=True ==> P"
(fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
+
(** Universal quantifier **)
+section "!";
qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
(fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
@@ -96,6 +105,7 @@
(** False ** Depends upon spec; it is impossible to do propositional logic
before quantifiers! **)
+section "False";
qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
(fn [major] => [rtac (major RS spec) 1]);
@@ -105,6 +115,7 @@
(** Negation **)
+section "~";
qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
(fn prems=> [rtac impI 1, eresolve_tac prems 1]);
@@ -112,7 +123,9 @@
qed_goalw "notE" HOL.thy [not_def] "[| ~P; P |] ==> R"
(fn prems => [rtac (prems MRS mp RS FalseE) 1]);
+
(** Implication **)
+section "-->";
qed_goal "impE" HOL.thy "[| P-->Q; P; Q ==> R |] ==> R"
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
@@ -135,6 +148,7 @@
(** Existential quantifier **)
+section "?";
qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
(fn prems => [rtac selectI 1, resolve_tac prems 1]);
@@ -145,6 +159,7 @@
(** Conjunction **)
+section "&";
qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
(fn prems =>
@@ -163,7 +178,9 @@
[cut_facts_tac prems 1, resolve_tac prems 1,
etac conjunct1 1, etac conjunct2 1]);
+
(** Disjunction *)
+section "|";
qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
(fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
@@ -176,7 +193,9 @@
[rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
+
(** CCONTR -- classical logic **)
+section "classical logic";
qed_goalw "classical" HOL.thy [not_def] "(~P ==> P) ==> P"
(fn [prem] =>
@@ -191,11 +210,23 @@
(fn [major]=>
[ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
+qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
+ rtac classical 1,
+ dtac p2 1,
+ etac notE 1,
+ rtac p1 1]);
+
+qed_goal "swap2" HOL.thy "[| P; Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
+ rtac notI 1,
+ dtac p2 1,
+ etac notE 1,
+ rtac p1 1]);
(** Unique existence **)
+section "?!";
qed_goalw "ex1I" HOL.thy [Ex1_def]
- "[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
+ "[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
(fn prems =>
[REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
@@ -206,6 +237,7 @@
(** Select: Hilbert's Epsilon-operator **)
+section "@";
(*Easier to apply than selectI: conclusion has only one occurrence of P*)
qed_goal "selectI2" HOL.thy
@@ -219,8 +251,15 @@
(fn prems => [ rtac selectI2 1,
REPEAT (ares_tac prems 1) ]);
+qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (fn prems => [
+ rtac iffI 1,
+ etac exI 1,
+ etac exE 1,
+ etac selectI 1]);
+
(** Classical intro rules for disjunction and existential quantifiers *)
+section "classical intro rules";
qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
(fn prems=>
@@ -263,6 +302,7 @@
fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+
(** Standard abbreviations **)
fun stac th = rtac(th RS ssubst);
@@ -303,9 +343,13 @@
end;
+
+
(*** Load simpdata.ML to be able to initialize HOL's simpset ***)
+
(** Applying HypsubstFun to generate hyp_subst_tac **)
+section "Classical Reasoner";
structure Hypsubst_Data =
struct
@@ -343,6 +387,9 @@
val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
addSEs [exE,ex1E] addEs [allE];
+
+section "Simplifier";
+
use "simpdata.ML";
simpset := HOL_ss;