src/HOL/simpdata.ML
changeset 7031 972b5f62f476
parent 6968 7f2977e96a5c
child 7127 48e235179ffb
     1.1 --- a/src/HOL/simpdata.ML	Mon Jul 19 15:19:11 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Jul 19 15:24:35 1999 +0200
     1.3 @@ -89,12 +89,14 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
     1.8 -  (fn [prem] => [rewtac prem, rtac refl 1]);
     1.9 +val [prem] = goal HOL.thy "x==y ==> x=y";
    1.10 +by (rewtac prem);
    1.11 +by (rtac refl 1);
    1.12 +qed "meta_eq_to_obj_eq";
    1.13  
    1.14  local
    1.15  
    1.16 -  fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
    1.17 +  fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]);
    1.18  
    1.19  in
    1.20  
    1.21 @@ -156,7 +158,7 @@
    1.22  
    1.23  val imp_cong = impI RSN
    1.24      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    1.25 -        (fn _=> [Blast_tac 1]) RS mp RS mp);
    1.26 +        (fn _=> [(Blast_tac 1)]) RS mp RS mp);
    1.27  
    1.28  (*Miniscoping: pushing in existential quantifiers*)
    1.29  val ex_simps = map prover 
    1.30 @@ -185,7 +187,7 @@
    1.31          (fn prems => [resolve_tac prems 1, etac exI 1]);
    1.32        val lemma2 = prove_goalw HOL.thy [Ex_def]
    1.33          "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
    1.34 -        (fn prems => [REPEAT(resolve_tac prems 1)])
    1.35 +        (fn prems => [(REPEAT(resolve_tac prems 1))])
    1.36    in equal_intr lemma1 lemma2 end;
    1.37  
    1.38  end;
    1.39 @@ -194,11 +196,11 @@
    1.40  
    1.41  val True_implies_equals = prove_goal HOL.thy
    1.42   "(True ==> PROP P) == PROP P"
    1.43 -(K [rtac equal_intr_rule 1, atac 2,
    1.44 +(fn _ => [rtac equal_intr_rule 1, atac 2,
    1.45            METAHYPS (fn prems => resolve_tac prems 1) 1,
    1.46            rtac TrueI 1]);
    1.47  
    1.48 -fun prove nm thm  = qed_goal nm HOL.thy thm (K [Blast_tac 1]);
    1.49 +fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]);
    1.50  
    1.51  prove "conj_commute" "(P&Q) = (Q&P)";
    1.52  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
    1.53 @@ -255,19 +257,19 @@
    1.54  
    1.55  let val th = prove_goal HOL.thy 
    1.56                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
    1.57 -                (fn _=> [Blast_tac 1])
    1.58 +                (fn _=> [(Blast_tac 1)])
    1.59  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    1.60  
    1.61  let val th = prove_goal HOL.thy 
    1.62                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
    1.63 -                (fn _=> [Blast_tac 1])
    1.64 +                (fn _=> [(Blast_tac 1)])
    1.65  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    1.66  
    1.67  (* '|' congruence rule: not included by default! *)
    1.68  
    1.69  let val th = prove_goal HOL.thy 
    1.70                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
    1.71 -                (fn _=> [Blast_tac 1])
    1.72 +                (fn _=> [(Blast_tac 1)])
    1.73  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
    1.74  
    1.75  prove "eq_sym_conv" "(x=y) = (y=x)";
    1.76 @@ -275,48 +277,58 @@
    1.77  
    1.78  (** if-then-else rules **)
    1.79  
    1.80 -qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
    1.81 - (K [Blast_tac 1]);
    1.82 +Goalw [if_def] "(if True then x else y) = x";
    1.83 +by (Blast_tac 1);
    1.84 +qed "if_True";
    1.85  
    1.86 -qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
    1.87 - (K [Blast_tac 1]);
    1.88 +Goalw [if_def] "(if False then x else y) = y";
    1.89 +by (Blast_tac 1);
    1.90 +qed "if_False";
    1.91  
    1.92 -qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
    1.93 - (K [Blast_tac 1]);
    1.94 +Goalw [if_def] "!!P. P ==> (if P then x else y) = x";
    1.95 +by (Blast_tac 1);
    1.96 +qed "if_P";
    1.97  
    1.98 -qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
    1.99 - (K [Blast_tac 1]);
   1.100 +Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y";
   1.101 +by (Blast_tac 1);
   1.102 +qed "if_not_P";
   1.103  
   1.104 -qed_goal "split_if" HOL.thy
   1.105 -    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
   1.106 -	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
   1.107 -         stac if_P 2,
   1.108 -         stac if_not_P 1,
   1.109 -         ALLGOALS (Blast_tac)]);
   1.110 +Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))";
   1.111 +by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1);
   1.112 +by (stac if_P 2);
   1.113 +by (stac if_not_P 1);
   1.114 +by (ALLGOALS (Blast_tac));
   1.115 +qed "split_if";
   1.116 +
   1.117  (* for backwards compatibility: *)
   1.118  val expand_if = split_if;
   1.119  
   1.120 -qed_goal "split_if_asm" HOL.thy
   1.121 -    "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
   1.122 -    (K [stac split_if 1,
   1.123 -	Blast_tac 1]);
   1.124 +Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
   1.125 +by (stac split_if 1);
   1.126 +by (Blast_tac 1);
   1.127 +qed "split_if_asm";
   1.128  
   1.129 -qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   1.130 -  (K [stac split_if 1, Blast_tac 1]);
   1.131 +Goal "(if c then x else x) = x";
   1.132 +by (stac split_if 1);
   1.133 +by (Blast_tac 1);
   1.134 +qed "if_cancel";
   1.135  
   1.136 -qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
   1.137 -  (K [stac split_if 1, Blast_tac 1]);
   1.138 +Goal "(if x = y then y else x) = x";
   1.139 +by (stac split_if 1);
   1.140 +by (Blast_tac 1);
   1.141 +qed "if_eq_cancel";
   1.142  
   1.143  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   1.144 -qed_goal "if_bool_eq_conj" HOL.thy
   1.145 -    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   1.146 -    (K [rtac split_if 1]);
   1.147 +Goal
   1.148 +    "(if P then Q else R) = ((P-->Q) & (~P-->R))";
   1.149 +by (rtac split_if 1);
   1.150 +qed "if_bool_eq_conj";
   1.151  
   1.152  (*And this form is useful for expanding IFs on the LEFT*)
   1.153 -qed_goal "if_bool_eq_disj" HOL.thy
   1.154 -    "(if P then Q else R) = ((P&Q) | (~P&R))"
   1.155 -    (K [stac split_if 1,
   1.156 -	Blast_tac 1]);
   1.157 +Goal "(if P then Q else R) = ((P&Q) | (~P&R))";
   1.158 +by (stac split_if 1);
   1.159 +by (Blast_tac 1);
   1.160 +qed "if_bool_eq_disj";
   1.161  
   1.162  
   1.163  (*** make simplification procedures for quantifier elimination ***)
   1.164 @@ -453,18 +465,18 @@
   1.165  qed "if_cong";
   1.166  
   1.167  (*Prevents simplification of x and y: much faster*)
   1.168 -qed_goal "if_weak_cong" HOL.thy
   1.169 -  "b=c ==> (if b then x else y) = (if c then x else y)"
   1.170 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   1.171 +Goal "b=c ==> (if b then x else y) = (if c then x else y)";
   1.172 +by (etac arg_cong 1);
   1.173 +qed "if_weak_cong";
   1.174  
   1.175  (*Prevents simplification of t: much faster*)
   1.176 -qed_goal "let_weak_cong" HOL.thy
   1.177 -  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
   1.178 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   1.179 +Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))";
   1.180 +by (etac arg_cong 1);
   1.181 +qed "let_weak_cong";
   1.182  
   1.183 -qed_goal "if_distrib" HOL.thy
   1.184 -  "f(if c then x else y) = (if c then f x else f y)" 
   1.185 -  (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
   1.186 +Goal "f(if c then x else y) = (if c then f x else f y)";
   1.187 +by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
   1.188 +qed "if_distrib";
   1.189  
   1.190  
   1.191  (*For expand_case_tac*)