src/Pure/drule.ML
changeset 10414 f7aeff3e9e1e
parent 10403 2955ee2424ce
child 10441 d727c39c4a4b
equal deleted inserted replaced
10413:0e015d9bea4e 10414:f7aeff3e9e1e
    11 signature BASIC_DRULE =
    11 signature BASIC_DRULE =
    12 sig
    12 sig
    13   val mk_implies        : cterm * cterm -> cterm
    13   val mk_implies        : cterm * cterm -> cterm
    14   val list_implies      : cterm list * cterm -> cterm
    14   val list_implies      : cterm list * cterm -> cterm
    15   val dest_implies      : cterm -> cterm * cterm
    15   val dest_implies      : cterm -> cterm * cterm
       
    16   val dest_equals       : cterm -> cterm * cterm
    16   val skip_flexpairs    : cterm -> cterm
    17   val skip_flexpairs    : cterm -> cterm
    17   val strip_imp_prems   : cterm -> cterm list
    18   val strip_imp_prems   : cterm -> cterm list
       
    19   val strip_imp_concl   : cterm -> cterm
    18   val cprems_of         : thm -> cterm list
    20   val cprems_of         : thm -> cterm list
    19   val read_insts        :
    21   val read_insts        :
    20           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    22           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    21                   -> (indexname -> typ option) * (indexname -> sort option)
    23                   -> (indexname -> typ option) * (indexname -> sort option)
    22                   -> string list -> (string*string)list
    24                   -> string list -> (string*string)list
    57   val reflexive_thm     : thm
    59   val reflexive_thm     : thm
    58   val symmetric_thm     : thm
    60   val symmetric_thm     : thm
    59   val transitive_thm    : thm
    61   val transitive_thm    : thm
    60   val refl_implies      : thm
    62   val refl_implies      : thm
    61   val symmetric_fun     : thm -> thm
    63   val symmetric_fun     : thm -> thm
    62   val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    64   val imp_cong          : thm
    63   val rewrite_thm       : bool * bool * bool
    65   val swap_prems_eq     : thm
    64                           -> (meta_simpset -> thm -> thm option)
       
    65                           -> meta_simpset -> thm -> thm
       
    66   val rewrite_cterm     : bool * bool * bool
       
    67                           -> (meta_simpset -> thm -> thm option)
       
    68                           -> meta_simpset -> cterm -> thm
       
    69   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
       
    70   val rewrite_goal_rule : bool* bool * bool
       
    71                           -> (meta_simpset -> thm -> thm option)
       
    72                           -> meta_simpset -> int -> thm -> thm
       
    73   val equal_abs_elim    : cterm  -> thm -> thm
    66   val equal_abs_elim    : cterm  -> thm -> thm
    74   val equal_abs_elim_list: cterm list -> thm -> thm
    67   val equal_abs_elim_list: cterm list -> thm -> thm
    75   val flexpair_abs_elim_list: cterm list -> thm -> thm
    68   val flexpair_abs_elim_list: cterm list -> thm -> thm
    76   val asm_rl            : thm
    69   val asm_rl            : thm
    77   val cut_rl            : thm
    70   val cut_rl            : thm
    80   val triv_forall_equality: thm
    73   val triv_forall_equality: thm
    81   val swap_prems_rl     : thm
    74   val swap_prems_rl     : thm
    82   val equal_intr_rule   : thm
    75   val equal_intr_rule   : thm
    83   val inst              : string -> string -> thm -> thm
    76   val inst              : string -> string -> thm -> thm
    84   val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
    77   val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
    85   val incr_indexes      : int -> thm -> thm
       
    86   val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    78   val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    87 end;
    79 end;
    88 
    80 
    89 signature DRULE =
    81 signature DRULE =
    90 sig
    82 sig
   132         (Const("==>", _) $ _ $ _) =>
   124         (Const("==>", _) $ _ $ _) =>
   133             let val (ct1,ct2) = dest_comb ct
   125             let val (ct1,ct2) = dest_comb ct
   134             in  (#2 (dest_comb ct1), ct2)  end
   126             in  (#2 (dest_comb ct1), ct2)  end
   135       | _ => raise TERM ("dest_implies", [term_of ct]) ;
   127       | _ => raise TERM ("dest_implies", [term_of ct]) ;
   136 
   128 
       
   129 fun dest_equals ct =
       
   130     case term_of ct of
       
   131         (Const("==", _) $ _ $ _) =>
       
   132             let val (ct1,ct2) = dest_comb ct
       
   133             in  (#2 (dest_comb ct1), ct2)  end
       
   134       | _ => raise TERM ("dest_equals", [term_of ct]) ;
       
   135 
   137 
   136 
   138 (*Discard flexflex pairs; return a cterm*)
   137 (*Discard flexflex pairs; return a cterm*)
   139 fun skip_flexpairs ct =
   138 fun skip_flexpairs ct =
   140     case term_of ct of
   139     case term_of ct of
   141         (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   140         (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   480       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   479       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   481   in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   480   in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   482 
   481 
   483 fun symmetric_fun thm = thm RS symmetric_thm;
   482 fun symmetric_fun thm = thm RS symmetric_thm;
   484 
   483 
   485 (** Below, a "conversion" has type cterm -> thm **)
   484 val imp_cong =
       
   485   let
       
   486     val ABC = read_prop "PROP A ==> PROP B == PROP C"
       
   487     val AB = read_prop "PROP A ==> PROP B"
       
   488     val AC = read_prop "PROP A ==> PROP C"
       
   489     val A = read_prop "PROP A"
       
   490   in
       
   491     store_standard_thm "imp_cong2" (implies_intr ABC (equal_intr
       
   492       (implies_intr AB (implies_intr A
       
   493         (equal_elim (implies_elim (assume ABC) (assume A))
       
   494           (implies_elim (assume AB) (assume A)))))
       
   495       (implies_intr AC (implies_intr A
       
   496         (equal_elim (symmetric (implies_elim (assume ABC) (assume A)))
       
   497           (implies_elim (assume AC) (assume A)))))))
       
   498   end;
       
   499 
       
   500 val swap_prems_eq =
       
   501   let
       
   502     val ABC = read_prop "PROP A ==> PROP B ==> PROP C"
       
   503     val BAC = read_prop "PROP B ==> PROP A ==> PROP C"
       
   504     val A = read_prop "PROP A"
       
   505     val B = read_prop "PROP B"
       
   506   in
       
   507     store_standard_thm "swap_prems_eq" (equal_intr
       
   508       (implies_intr ABC (implies_intr B (implies_intr A
       
   509         (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
       
   510       (implies_intr BAC (implies_intr A (implies_intr B
       
   511         (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
       
   512   end;
   486 
   513 
   487 val refl_implies = reflexive implies;
   514 val refl_implies = reflexive implies;
   488 
       
   489 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
       
   490 (*Do not rewrite flex-flex pairs*)
       
   491 fun goals_conv pred cv =
       
   492   let fun gconv i ct =
       
   493         let val (A,B) = dest_implies ct
       
   494             val (thA,j) = case term_of A of
       
   495                   Const("=?=",_)$_$_ => (reflexive A, i)
       
   496                 | _ => (if pred i then cv A else reflexive A, i+1)
       
   497         in  combination (combination refl_implies thA) (gconv j B) end
       
   498         handle TERM _ => reflexive ct
       
   499   in gconv 1 end;
       
   500 
       
   501 (*Use a conversion to transform a theorem*)
       
   502 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
       
   503 
       
   504 (*rewriting conversion*)
       
   505 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
       
   506 
       
   507 (*Rewrite a theorem*)
       
   508 fun rewrite_rule_aux _ [] = (fn th => th)
       
   509   | rewrite_rule_aux prover thms =
       
   510       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms));
       
   511 
       
   512 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
       
   513 fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
       
   514 
       
   515 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
       
   516 fun rewrite_goals_rule_aux _ []   th = th
       
   517   | rewrite_goals_rule_aux prover thms th =
       
   518       fconv_rule (goals_conv (K true) (rew_conv (true, true, false) prover
       
   519         (Thm.mss_of thms))) th;
       
   520 
       
   521 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
       
   522 fun rewrite_goal_rule mode prover mss i thm =
       
   523   if 0 < i  andalso  i <= nprems_of thm
       
   524   then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
       
   525   else raise THM("rewrite_goal_rule",i,[thm]);
       
   526 
   515 
   527 
   516 
   528 (*** Some useful meta-theorems ***)
   517 (*** Some useful meta-theorems ***)
   529 
   518 
   530 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   519 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   676   let val {sign=signa, t=a, ...} = rep_cterm ca
   665   let val {sign=signa, t=a, ...} = rep_cterm ca
   677       and combth = combination eqth (reflexive ca)
   666       and combth = combination eqth (reflexive ca)
   678       val {sign,prop,...} = rep_thm eqth
   667       val {sign,prop,...} = rep_thm eqth
   679       val (abst,absu) = Logic.dest_equals prop
   668       val (abst,absu) = Logic.dest_equals prop
   680       val cterm = cterm_of (Sign.merge (sign,signa))
   669       val cterm = cterm_of (Sign.merge (sign,signa))
   681   in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   670   in  transitive (symmetric (beta_conversion false (cterm (abst$a))))
   682            (transitive combth (beta_conversion (cterm (absu$a))))
   671            (transitive combth (beta_conversion false (cterm (absu$a))))
   683   end
   672   end
   684   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   673   handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   685 
   674 
   686 (*Calling equal_abs_elim with multiple terms*)
   675 (*Calling equal_abs_elim with multiple terms*)
   687 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   676 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   801   Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
   790   Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
   802 
   791 
   803 
   792 
   804 (* increment var indexes *)
   793 (* increment var indexes *)
   805 
   794 
   806 fun incr_indexes 0 thm = thm
       
   807   | incr_indexes inc thm =
       
   808       let
       
   809         val sign = Thm.sign_of_thm thm;
       
   810 
       
   811         fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
       
   812         fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
       
   813         val thm' = instantiate' (map inc_tvar (tvars_of thm)) [] thm;
       
   814         val thm'' = instantiate' [] (map inc_var (vars_of thm')) thm';
       
   815       in thm'' end;
       
   816 
       
   817 fun incr_indexes_wrt is cTs cts thms =
   795 fun incr_indexes_wrt is cTs cts thms =
   818   let
   796   let
   819     val maxidx =
   797     val maxidx =
   820       foldl Int.max (~1, is @
   798       foldl Int.max (~1, is @
   821         map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @
   799         map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @
   822         map (#maxidx o Thm.rep_cterm) cts @
   800         map (#maxidx o Thm.rep_cterm) cts @
   823         map (#maxidx o Thm.rep_thm) thms);
   801         map (#maxidx o Thm.rep_thm) thms);
   824   in incr_indexes (maxidx + 1) end;
   802   in Thm.incr_indexes (maxidx + 1) end;
   825 
   803 
   826 
   804 
   827 (* freeze_all *)
   805 (* freeze_all *)
   828 
   806 
   829 (*freeze all (T)Vars; assumes thm in standard form*)
   807 (*freeze all (T)Vars; assumes thm in standard form*)