- new theorems imp_cong and swap_prems_eq
authorberghofe
Tue Nov 07 17:48:25 2000 +0100 (2000-11-07)
changeset 10414f7aeff3e9e1e
parent 10413 0e015d9bea4e
child 10415 e6d7b77a0574
- new theorems imp_cong and swap_prems_eq
- new function dest_equals
- exported strip_imp_concl
- removed incr_indexes (now in Thm)
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Nov 07 17:44:48 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Nov 07 17:48:25 2000 +0100
     1.3 @@ -13,8 +13,10 @@
     1.4    val mk_implies        : cterm * cterm -> cterm
     1.5    val list_implies      : cterm list * cterm -> cterm
     1.6    val dest_implies      : cterm -> cterm * cterm
     1.7 +  val dest_equals       : cterm -> cterm * cterm
     1.8    val skip_flexpairs    : cterm -> cterm
     1.9    val strip_imp_prems   : cterm -> cterm list
    1.10 +  val strip_imp_concl   : cterm -> cterm
    1.11    val cprems_of         : thm -> cterm list
    1.12    val read_insts        :
    1.13            Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    1.14 @@ -59,17 +61,8 @@
    1.15    val transitive_thm    : thm
    1.16    val refl_implies      : thm
    1.17    val symmetric_fun     : thm -> thm
    1.18 -  val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.19 -  val rewrite_thm       : bool * bool * bool
    1.20 -                          -> (meta_simpset -> thm -> thm option)
    1.21 -                          -> meta_simpset -> thm -> thm
    1.22 -  val rewrite_cterm     : bool * bool * bool
    1.23 -                          -> (meta_simpset -> thm -> thm option)
    1.24 -                          -> meta_simpset -> cterm -> thm
    1.25 -  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.26 -  val rewrite_goal_rule : bool* bool * bool
    1.27 -                          -> (meta_simpset -> thm -> thm option)
    1.28 -                          -> meta_simpset -> int -> thm -> thm
    1.29 +  val imp_cong          : thm
    1.30 +  val swap_prems_eq     : thm
    1.31    val equal_abs_elim    : cterm  -> thm -> thm
    1.32    val equal_abs_elim_list: cterm list -> thm -> thm
    1.33    val flexpair_abs_elim_list: cterm list -> thm -> thm
    1.34 @@ -82,7 +75,6 @@
    1.35    val equal_intr_rule   : thm
    1.36    val inst              : string -> string -> thm -> thm
    1.37    val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
    1.38 -  val incr_indexes      : int -> thm -> thm
    1.39    val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    1.40  end;
    1.41  
    1.42 @@ -134,6 +126,13 @@
    1.43              in  (#2 (dest_comb ct1), ct2)  end
    1.44        | _ => raise TERM ("dest_implies", [term_of ct]) ;
    1.45  
    1.46 +fun dest_equals ct =
    1.47 +    case term_of ct of
    1.48 +        (Const("==", _) $ _ $ _) =>
    1.49 +            let val (ct1,ct2) = dest_comb ct
    1.50 +            in  (#2 (dest_comb ct1), ct2)  end
    1.51 +      | _ => raise TERM ("dest_equals", [term_of ct]) ;
    1.52 +
    1.53  
    1.54  (*Discard flexflex pairs; return a cterm*)
    1.55  fun skip_flexpairs ct =
    1.56 @@ -482,48 +481,38 @@
    1.57  
    1.58  fun symmetric_fun thm = thm RS symmetric_thm;
    1.59  
    1.60 -(** Below, a "conversion" has type cterm -> thm **)
    1.61 +val imp_cong =
    1.62 +  let
    1.63 +    val ABC = read_prop "PROP A ==> PROP B == PROP C"
    1.64 +    val AB = read_prop "PROP A ==> PROP B"
    1.65 +    val AC = read_prop "PROP A ==> PROP C"
    1.66 +    val A = read_prop "PROP A"
    1.67 +  in
    1.68 +    store_standard_thm "imp_cong2" (implies_intr ABC (equal_intr
    1.69 +      (implies_intr AB (implies_intr A
    1.70 +        (equal_elim (implies_elim (assume ABC) (assume A))
    1.71 +          (implies_elim (assume AB) (assume A)))))
    1.72 +      (implies_intr AC (implies_intr A
    1.73 +        (equal_elim (symmetric (implies_elim (assume ABC) (assume A)))
    1.74 +          (implies_elim (assume AC) (assume A)))))))
    1.75 +  end;
    1.76 +
    1.77 +val swap_prems_eq =
    1.78 +  let
    1.79 +    val ABC = read_prop "PROP A ==> PROP B ==> PROP C"
    1.80 +    val BAC = read_prop "PROP B ==> PROP A ==> PROP C"
    1.81 +    val A = read_prop "PROP A"
    1.82 +    val B = read_prop "PROP B"
    1.83 +  in
    1.84 +    store_standard_thm "swap_prems_eq" (equal_intr
    1.85 +      (implies_intr ABC (implies_intr B (implies_intr A
    1.86 +        (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
    1.87 +      (implies_intr BAC (implies_intr A (implies_intr B
    1.88 +        (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
    1.89 +  end;
    1.90  
    1.91  val refl_implies = reflexive implies;
    1.92  
    1.93 -(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
    1.94 -(*Do not rewrite flex-flex pairs*)
    1.95 -fun goals_conv pred cv =
    1.96 -  let fun gconv i ct =
    1.97 -        let val (A,B) = dest_implies ct
    1.98 -            val (thA,j) = case term_of A of
    1.99 -                  Const("=?=",_)$_$_ => (reflexive A, i)
   1.100 -                | _ => (if pred i then cv A else reflexive A, i+1)
   1.101 -        in  combination (combination refl_implies thA) (gconv j B) end
   1.102 -        handle TERM _ => reflexive ct
   1.103 -  in gconv 1 end;
   1.104 -
   1.105 -(*Use a conversion to transform a theorem*)
   1.106 -fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   1.107 -
   1.108 -(*rewriting conversion*)
   1.109 -fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   1.110 -
   1.111 -(*Rewrite a theorem*)
   1.112 -fun rewrite_rule_aux _ [] = (fn th => th)
   1.113 -  | rewrite_rule_aux prover thms =
   1.114 -      fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms));
   1.115 -
   1.116 -fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
   1.117 -fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
   1.118 -
   1.119 -(*Rewrite the subgoals of a proof state (represented by a theorem) *)
   1.120 -fun rewrite_goals_rule_aux _ []   th = th
   1.121 -  | rewrite_goals_rule_aux prover thms th =
   1.122 -      fconv_rule (goals_conv (K true) (rew_conv (true, true, false) prover
   1.123 -        (Thm.mss_of thms))) th;
   1.124 -
   1.125 -(*Rewrite the subgoal of a proof state (represented by a theorem) *)
   1.126 -fun rewrite_goal_rule mode prover mss i thm =
   1.127 -  if 0 < i  andalso  i <= nprems_of thm
   1.128 -  then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
   1.129 -  else raise THM("rewrite_goal_rule",i,[thm]);
   1.130 -
   1.131  
   1.132  (*** Some useful meta-theorems ***)
   1.133  
   1.134 @@ -678,8 +667,8 @@
   1.135        val {sign,prop,...} = rep_thm eqth
   1.136        val (abst,absu) = Logic.dest_equals prop
   1.137        val cterm = cterm_of (Sign.merge (sign,signa))
   1.138 -  in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   1.139 -           (transitive combth (beta_conversion (cterm (absu$a))))
   1.140 +  in  transitive (symmetric (beta_conversion false (cterm (abst$a))))
   1.141 +           (transitive combth (beta_conversion false (cterm (absu$a))))
   1.142    end
   1.143    handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   1.144  
   1.145 @@ -803,17 +792,6 @@
   1.146  
   1.147  (* increment var indexes *)
   1.148  
   1.149 -fun incr_indexes 0 thm = thm
   1.150 -  | incr_indexes inc thm =
   1.151 -      let
   1.152 -        val sign = Thm.sign_of_thm thm;
   1.153 -
   1.154 -        fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
   1.155 -        fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
   1.156 -        val thm' = instantiate' (map inc_tvar (tvars_of thm)) [] thm;
   1.157 -        val thm'' = instantiate' [] (map inc_var (vars_of thm')) thm';
   1.158 -      in thm'' end;
   1.159 -
   1.160  fun incr_indexes_wrt is cTs cts thms =
   1.161    let
   1.162      val maxidx =
   1.163 @@ -821,7 +799,7 @@
   1.164          map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @
   1.165          map (#maxidx o Thm.rep_cterm) cts @
   1.166          map (#maxidx o Thm.rep_thm) thms);
   1.167 -  in incr_indexes (maxidx + 1) end;
   1.168 +  in Thm.incr_indexes (maxidx + 1) end;
   1.169  
   1.170  
   1.171  (* freeze_all *)