src/HOL/simpdata.ML
changeset 2031 03a843f0f447
parent 2022 9d47e2962edd
child 2036 62ff902eeffc
     1.1 --- a/src/HOL/simpdata.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4  (*** Addition of rules to simpsets and clasets simultaneously ***)
     1.5  
     1.6  (*Takes UNCONDITIONAL theorems of the form A<->B to 
     1.7 -	the Safe Intr     rule B==>A and 
     1.8 -	the Safe Destruct rule A==>B.
     1.9 +        the Safe Intr     rule B==>A and 
    1.10 +        the Safe Destruct rule A==>B.
    1.11    Also ~A goes to the Safe Elim rule A ==> ?R
    1.12    Failing other cases, A is added as a Safe Intr rule*)
    1.13  local
    1.14 @@ -42,31 +42,31 @@
    1.15  
    1.16    fun addIff th = 
    1.17        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
    1.18 -		(Const("not",_) $ A) =>
    1.19 -		    AddSEs [zero_var_indexes (th RS notE)]
    1.20 -	      | (con $ _ $ _) =>
    1.21 -		    if con=iff_const
    1.22 -		    then (AddSIs [zero_var_indexes (th RS iffD2)];  
    1.23 -			  AddSDs [zero_var_indexes (th RS iffD1)])
    1.24 -		    else  AddSIs [th]
    1.25 -	      | _ => AddSIs [th];
    1.26 +                (Const("not",_) $ A) =>
    1.27 +                    AddSEs [zero_var_indexes (th RS notE)]
    1.28 +              | (con $ _ $ _) =>
    1.29 +                    if con=iff_const
    1.30 +                    then (AddSIs [zero_var_indexes (th RS iffD2)];  
    1.31 +                          AddSDs [zero_var_indexes (th RS iffD1)])
    1.32 +                    else  AddSIs [th]
    1.33 +              | _ => AddSIs [th];
    1.34         Addsimps [th])
    1.35        handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    1.36 -			 string_of_thm th)
    1.37 +                         string_of_thm th)
    1.38  
    1.39    fun delIff th = 
    1.40        (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of
    1.41 -		(Const("not",_) $ A) =>
    1.42 -		    Delrules [zero_var_indexes (th RS notE)]
    1.43 -	      | (con $ _ $ _) =>
    1.44 -		    if con=iff_const
    1.45 -		    then Delrules [zero_var_indexes (th RS iffD2),
    1.46 -				   zero_var_indexes (th RS iffD1)]
    1.47 -		    else Delrules [th]
    1.48 -	      | _ => Delrules [th];
    1.49 +                (Const("not",_) $ A) =>
    1.50 +                    Delrules [zero_var_indexes (th RS notE)]
    1.51 +              | (con $ _ $ _) =>
    1.52 +                    if con=iff_const
    1.53 +                    then Delrules [zero_var_indexes (th RS iffD2),
    1.54 +                                   zero_var_indexes (th RS iffD1)]
    1.55 +                    else Delrules [th]
    1.56 +              | _ => Delrules [th];
    1.57         Delsimps [th])
    1.58        handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.59 -			  string_of_thm th)
    1.60 +                          string_of_thm th)
    1.61  in
    1.62  val AddIffs = seq addIff
    1.63  val DelIffs = seq delIff
    1.64 @@ -85,19 +85,19 @@
    1.65  
    1.66    fun atomize pairs =
    1.67      let fun atoms th =
    1.68 -	  (case concl_of th of
    1.69 -	     Const("Trueprop",_) $ p =>
    1.70 -	       (case head_of p of
    1.71 -		  Const(a,_) =>
    1.72 -		    (case assoc(pairs,a) of
    1.73 -		       Some(rls) => flat (map atoms ([th] RL rls))
    1.74 -		     | None => [th])
    1.75 -		| _ => [th])
    1.76 -	   | _ => [th])
    1.77 +          (case concl_of th of
    1.78 +             Const("Trueprop",_) $ p =>
    1.79 +               (case head_of p of
    1.80 +                  Const(a,_) =>
    1.81 +                    (case assoc(pairs,a) of
    1.82 +                       Some(rls) => flat (map atoms ([th] RL rls))
    1.83 +                     | None => [th])
    1.84 +                | _ => [th])
    1.85 +           | _ => [th])
    1.86      in atoms end;
    1.87  
    1.88    fun mk_meta_eq r = case concl_of r of
    1.89 -	  Const("==",_)$_$_ => r
    1.90 +          Const("==",_)$_$_ => r
    1.91        |   _$(Const("op =",_)$_$_) => r RS eq_reflection
    1.92        |   _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
    1.93        |   _ => r RS P_imp_P_eq_True;
    1.94 @@ -153,8 +153,8 @@
    1.95  val expand_if = prove_goal HOL.thy
    1.96      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
    1.97   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
    1.98 -         rtac (if_P RS ssubst) 2,
    1.99 -         rtac (if_not_P RS ssubst) 1,
   1.100 +         stac if_P 2,
   1.101 +         stac if_not_P 1,
   1.102           REPEAT(fast_tac HOL_cs 1) ]);
   1.103  
   1.104  val if_bool_eq = prove_goal HOL.thy
   1.105 @@ -183,21 +183,21 @@
   1.106  
   1.107  (*Miniscoping: pushing in existential quantifiers*)
   1.108  val ex_simps = map prover 
   1.109 -		["(EX x. P x & Q)   = ((EX x.P x) & Q)",
   1.110 -		 "(EX x. P & Q x)   = (P & (EX x.Q x))",
   1.111 -		 "(EX x. P x | Q)   = ((EX x.P x) | Q)",
   1.112 -		 "(EX x. P | Q x)   = (P | (EX x.Q x))",
   1.113 -		 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
   1.114 -		 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
   1.115 +                ["(EX x. P x & Q)   = ((EX x.P x) & Q)",
   1.116 +                 "(EX x. P & Q x)   = (P & (EX x.Q x))",
   1.117 +                 "(EX x. P x | Q)   = ((EX x.P x) | Q)",
   1.118 +                 "(EX x. P | Q x)   = (P | (EX x.Q x))",
   1.119 +                 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
   1.120 +                 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
   1.121  
   1.122  (*Miniscoping: pushing in universal quantifiers*)
   1.123  val all_simps = map prover
   1.124 -		["(ALL x. P x & Q)   = ((ALL x.P x) & Q)",
   1.125 -		 "(ALL x. P & Q x)   = (P & (ALL x.Q x))",
   1.126 -		 "(ALL x. P x | Q)   = ((ALL x.P x) | Q)",
   1.127 -		 "(ALL x. P | Q x)   = (P | (ALL x.Q x))",
   1.128 -		 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
   1.129 -		 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
   1.130 +                ["(ALL x. P x & Q)   = ((ALL x.P x) & Q)",
   1.131 +                 "(ALL x. P & Q x)   = (P & (ALL x.Q x))",
   1.132 +                 "(ALL x. P x | Q)   = ((ALL x.P x) | Q)",
   1.133 +                 "(ALL x. P | Q x)   = (P | (ALL x.Q x))",
   1.134 +                 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
   1.135 +                 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
   1.136  
   1.137  val HOL_ss = empty_ss
   1.138        setmksimps (mksimps mksimps_pairs)
   1.139 @@ -205,7 +205,7 @@
   1.140                               ORELSE' etac FalseE)
   1.141        setsubgoaler asm_simp_tac
   1.142        addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
   1.143 -		 cases_simp]
   1.144 +                 cases_simp]
   1.145          @ ex_simps @ all_simps @ simp_thms)
   1.146        addcongs [imp_cong];
   1.147  
   1.148 @@ -245,13 +245,13 @@
   1.149  val conj_cong = 
   1.150    let val th = prove_goal HOL.thy 
   1.151                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   1.152 -		(fn _=> [fast_tac HOL_cs 1])
   1.153 +                (fn _=> [fast_tac HOL_cs 1])
   1.154    in  standard (impI RSN (2, th RS mp RS mp))  end;
   1.155  
   1.156  val rev_conj_cong =
   1.157    let val th = prove_goal HOL.thy 
   1.158                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   1.159 -		(fn _=> [fast_tac HOL_cs 1])
   1.160 +                (fn _=> [fast_tac HOL_cs 1])
   1.161    in  standard (impI RSN (2, th RS mp RS mp))  end;
   1.162  
   1.163  (* '|' congruence rule: not included by default! *)
   1.164 @@ -259,7 +259,7 @@
   1.165  val disj_cong = 
   1.166    let val th = prove_goal HOL.thy 
   1.167                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   1.168 -		(fn _=> [fast_tac HOL_cs 1])
   1.169 +                (fn _=> [fast_tac HOL_cs 1])
   1.170    in  standard (impI RSN (2, th RS mp RS mp))  end;
   1.171  
   1.172  (** 'if' congruence rules: neither included by default! *)