src/HOL/HOL.ML
changeset 1660 8cb42cd97579
parent 1657 a7a6c3fb3cdd
child 1668 8ead1fe65aad
     1.1 --- a/src/HOL/HOL.ML	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  
     1.5  
     1.6  (** Equality **)
     1.7 +section "=";
     1.8  
     1.9  qed_goal "sym" HOL.thy "s=t ==> t=s"
    1.10   (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
    1.11 @@ -34,7 +35,9 @@
    1.12      (rtac sym 1),
    1.13      (REPEAT (resolve_tac prems 1)) ]);
    1.14  
    1.15 +
    1.16  (** Congruence rules for meta-application **)
    1.17 +section "Congruence";
    1.18  
    1.19  (*similar to AP_THM in Gordon's HOL*)
    1.20  qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
    1.21 @@ -49,7 +52,9 @@
    1.22   (fn [prem1,prem2] =>
    1.23     [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
    1.24  
    1.25 +
    1.26  (** Equality of booleans -- iff **)
    1.27 +section "iff";
    1.28  
    1.29  qed_goal "iffI" HOL.thy
    1.30     "[| P ==> Q;  Q ==> P |] ==> P=Q"
    1.31 @@ -65,7 +70,9 @@
    1.32      "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
    1.33   (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
    1.34  
    1.35 +
    1.36  (** True **)
    1.37 +section "True";
    1.38  
    1.39  qed_goalw "TrueI" HOL.thy [True_def] "True"
    1.40    (fn _ => [rtac refl 1]);
    1.41 @@ -76,7 +83,9 @@
    1.42  qed_goal "eqTrueE" HOL.thy "P=True ==> P" 
    1.43   (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
    1.44  
    1.45 +
    1.46  (** Universal quantifier **)
    1.47 +section "!";
    1.48  
    1.49  qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
    1.50   (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
    1.51 @@ -96,6 +105,7 @@
    1.52  
    1.53  (** False ** Depends upon spec; it is impossible to do propositional logic
    1.54               before quantifiers! **)
    1.55 +section "False";
    1.56  
    1.57  qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
    1.58   (fn [major] => [rtac (major RS spec) 1]);
    1.59 @@ -105,6 +115,7 @@
    1.60  
    1.61  
    1.62  (** Negation **)
    1.63 +section "~";
    1.64  
    1.65  qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
    1.66   (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
    1.67 @@ -112,7 +123,9 @@
    1.68  qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
    1.69   (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
    1.70  
    1.71 +
    1.72  (** Implication **)
    1.73 +section "-->";
    1.74  
    1.75  qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
    1.76   (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    1.77 @@ -135,6 +148,7 @@
    1.78  
    1.79  
    1.80  (** Existential quantifier **)
    1.81 +section "?";
    1.82  
    1.83  qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
    1.84   (fn prems => [rtac selectI 1, resolve_tac prems 1]);
    1.85 @@ -145,6 +159,7 @@
    1.86  
    1.87  
    1.88  (** Conjunction **)
    1.89 +section "&";
    1.90  
    1.91  qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
    1.92   (fn prems =>
    1.93 @@ -163,7 +178,9 @@
    1.94           [cut_facts_tac prems 1, resolve_tac prems 1,
    1.95            etac conjunct1 1, etac conjunct2 1]);
    1.96  
    1.97 +
    1.98  (** Disjunction *)
    1.99 +section "|";
   1.100  
   1.101  qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
   1.102   (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   1.103 @@ -176,7 +193,9 @@
   1.104          [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
   1.105           rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
   1.106  
   1.107 +
   1.108  (** CCONTR -- classical logic **)
   1.109 +section "classical logic";
   1.110  
   1.111  qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
   1.112   (fn [prem] =>
   1.113 @@ -191,11 +210,23 @@
   1.114   (fn [major]=>
   1.115    [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
   1.116  
   1.117 +qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
   1.118 +	rtac classical 1,
   1.119 +	dtac p2 1,
   1.120 +	etac notE 1,
   1.121 +	rtac p1 1]);
   1.122 +
   1.123 +qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
   1.124 +	rtac notI 1,
   1.125 +	dtac p2 1,
   1.126 +	etac notE 1,
   1.127 +	rtac p1 1]);
   1.128  
   1.129  (** Unique existence **)
   1.130 +section "?!";
   1.131  
   1.132  qed_goalw "ex1I" HOL.thy [Ex1_def]
   1.133 -    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
   1.134 +	    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
   1.135   (fn prems =>
   1.136    [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
   1.137  
   1.138 @@ -206,6 +237,7 @@
   1.139  
   1.140  
   1.141  (** Select: Hilbert's Epsilon-operator **)
   1.142 +section "@";
   1.143  
   1.144  (*Easier to apply than selectI: conclusion has only one occurrence of P*)
   1.145  qed_goal "selectI2" HOL.thy
   1.146 @@ -219,8 +251,15 @@
   1.147   (fn prems => [ rtac selectI2 1, 
   1.148                  REPEAT (ares_tac prems 1) ]);
   1.149  
   1.150 +qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (fn prems => [
   1.151 +        rtac iffI 1,
   1.152 +        etac exI 1,
   1.153 +        etac exE 1,
   1.154 +        etac selectI 1]);
   1.155 +
   1.156  
   1.157  (** Classical intro rules for disjunction and existential quantifiers *)
   1.158 +section "classical intro rules";
   1.159  
   1.160  qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
   1.161   (fn prems=>
   1.162 @@ -263,6 +302,7 @@
   1.163  
   1.164  fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   1.165  
   1.166 +
   1.167  (** Standard abbreviations **)
   1.168  
   1.169  fun stac th = rtac(th RS ssubst);
   1.170 @@ -303,9 +343,13 @@
   1.171  
   1.172  end;
   1.173  
   1.174 +
   1.175 +
   1.176  (*** Load simpdata.ML to be able to initialize HOL's simpset ***)
   1.177  
   1.178 +
   1.179  (** Applying HypsubstFun to generate hyp_subst_tac **)
   1.180 +section "Classical Reasoner";
   1.181  
   1.182  structure Hypsubst_Data =
   1.183    struct
   1.184 @@ -343,6 +387,9 @@
   1.185  val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
   1.186                       addSEs [exE,ex1E] addEs [allE];
   1.187  
   1.188 +
   1.189 +section "Simplifier";
   1.190 +
   1.191  use     "simpdata.ML";
   1.192  simpset := HOL_ss;
   1.193