src/Pure/drule.ML
changeset 2004 3411fe560611
parent 1906 4699a9058a4f
child 2152 76d5ed939545
equal deleted inserted replaced
2003:b48f066d52dc 2004:3411fe560611
    15   val asm_rl		: thm
    15   val asm_rl		: thm
    16   val assume_ax		: theory -> string -> thm
    16   val assume_ax		: theory -> string -> thm
    17   val COMP		: thm * thm -> thm
    17   val COMP		: thm * thm -> thm
    18   val compose		: thm * int * thm -> thm list
    18   val compose		: thm * int * thm -> thm list
    19   val cprems_of		: thm -> cterm list
    19   val cprems_of		: thm -> cterm list
    20   val cskip_flexpairs	: cterm -> cterm
       
    21   val cstrip_imp_prems	: cterm -> cterm list
       
    22   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    20   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    23   val cut_rl		: thm
    21   val cut_rl		: thm
    24   val equal_abs_elim	: cterm  -> thm -> thm
    22   val equal_abs_elim	: cterm  -> thm -> thm
    25   val equal_abs_elim_list: cterm list -> thm -> thm
    23   val equal_abs_elim_list: cterm list -> thm -> thm
    26   val eq_thm		: thm * thm -> bool
    24   val eq_thm		: thm * thm -> bool
    33   val forall_elim_list	: cterm list -> thm -> thm
    31   val forall_elim_list	: cterm list -> thm -> thm
    34   val forall_elim_var	: int -> thm -> thm
    32   val forall_elim_var	: int -> thm -> thm
    35   val forall_elim_vars	: int -> thm -> thm
    33   val forall_elim_vars	: int -> thm -> thm
    36   val implies_elim_list	: thm -> thm list -> thm
    34   val implies_elim_list	: thm -> thm list -> thm
    37   val implies_intr_list	: cterm list -> thm -> thm
    35   val implies_intr_list	: cterm list -> thm -> thm
    38   val dest_cimplies     : cterm -> cterm * cterm
    36   val dest_implies      : cterm -> cterm * cterm
    39   val MRL		: thm list list * thm list -> thm list
    37   val MRL		: thm list list * thm list -> thm list
    40   val MRS		: thm list * thm -> thm
    38   val MRS		: thm list * thm -> thm
    41   val read_instantiate	: (string*string)list -> thm -> thm
    39   val read_instantiate	: (string*string)list -> thm -> thm
    42   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    40   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    43   val read_insts	:
    41   val read_insts	:
    44           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    42           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    45                   -> (indexname -> typ option) * (indexname -> sort option)
    43                   -> (indexname -> typ option) * (indexname -> sort option)
    46                   -> string list -> (string*string)list
    44                   -> string list -> (string*string)list
    47                   -> (indexname*ctyp)list * (cterm*cterm)list
    45                   -> (indexname*ctyp)list * (cterm*cterm)list
    48   val reflexive_thm	: thm
    46   val reflexive_thm	: thm
       
    47   val refl_implies      : thm
    49   val revcut_rl		: thm
    48   val revcut_rl		: thm
    50   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
    49   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
    51         -> meta_simpset -> int -> thm -> thm
    50         -> meta_simpset -> int -> thm -> thm
    52   val rewrite_goals_rule: thm list -> thm -> thm
    51   val rewrite_goals_rule: thm list -> thm -> thm
    53   val rewrite_rule	: thm list -> thm -> thm
    52   val rewrite_rule	: thm list -> thm -> thm
    54   val RS		: thm * thm -> thm
    53   val RS		: thm * thm -> thm
    55   val RSN		: thm * (int * thm) -> thm
    54   val RSN		: thm * (int * thm) -> thm
    56   val RL		: thm list * thm list -> thm list
    55   val RL		: thm list * thm list -> thm list
    57   val RLN		: thm list * (int * thm list) -> thm list
    56   val RLN		: thm list * (int * thm list) -> thm list
    58   val size_of_thm	: thm -> int
    57   val size_of_thm	: thm -> int
       
    58   val skip_flexpairs	: cterm -> cterm
    59   val standard		: thm -> thm
    59   val standard		: thm -> thm
       
    60   val strip_imp_prems	: cterm -> cterm list
    60   val swap_prems_rl     : thm
    61   val swap_prems_rl     : thm
    61   val symmetric_thm	: thm
    62   val symmetric_thm	: thm
    62   val thin_rl		: thm
    63   val thin_rl		: thm
    63   val transitive_thm	: thm
    64   val transitive_thm	: thm
    64   val triv_forall_equality: thm
    65   val triv_forall_equality: thm
   192 
   193 
   193 (**** More derived rules and operations on theorems ****)
   194 (**** More derived rules and operations on theorems ****)
   194 
   195 
   195 (** some cterm->cterm operations: much faster than calling cterm_of! **)
   196 (** some cterm->cterm operations: much faster than calling cterm_of! **)
   196 
   197 
       
   198 (** SAME NAMES as in structure Logic: use compound identifiers! **)
       
   199 
   197 (*dest_implies for cterms. Note T=prop below*)
   200 (*dest_implies for cterms. Note T=prop below*)
   198 fun dest_cimplies ct =
   201 fun dest_implies ct =
   199   (let val (ct1, ct2) = dest_comb ct
   202     case term_of ct of 
   200        val {t, ...} = rep_cterm ct1;
   203 	(Const("==>", _) $ _ $ _) => 
   201    in case head_of t of
   204 	    let val (ct1,ct2) = dest_comb ct
   202           Const("==>", _) => (snd (dest_comb ct1), ct2)
   205 	    in  (#2 (dest_comb ct1), ct2)  end	     
   203         | _ => raise TERM ("dest_cimplies", [term_of ct])
   206       | _ => raise TERM ("dest_implies", [term_of ct]) ;
   204    end
       
   205   ) handle CTERM "dest_comb" => raise TERM ("dest_cimplies", [term_of ct]);
       
   206 
   207 
   207 
   208 
   208 (*Discard flexflex pairs; return a cterm*)
   209 (*Discard flexflex pairs; return a cterm*)
   209 fun cskip_flexpairs ct =
   210 fun skip_flexpairs ct =
   210     case term_of ct of
   211     case term_of ct of
   211 	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   212 	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
   212 	    cskip_flexpairs (#2 (dest_cimplies ct))
   213 	    skip_flexpairs (#2 (dest_implies ct))
   213       | _ => ct;
   214       | _ => ct;
   214 
   215 
   215 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   216 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   216 fun cstrip_imp_prems ct =
   217 fun strip_imp_prems ct =
   217     let val (cA,cB) = dest_cimplies ct
   218     let val (cA,cB) = dest_implies ct
   218     in  cA :: cstrip_imp_prems cB  end
   219     in  cA :: strip_imp_prems cB  end
   219     handle TERM _ => [];
   220     handle TERM _ => [];
   220 
   221 
       
   222 (* A1==>...An==>B  goes to B, where B is not an implication *)
       
   223 fun strip_imp_concl ct =
       
   224     case term_of ct of (Const("==>", _) $ _ $ _) => 
       
   225 	strip_imp_concl (#2 (dest_comb ct))
       
   226   | _ => ct;
       
   227 
   221 (*The premises of a theorem, as a cterm list*)
   228 (*The premises of a theorem, as a cterm list*)
   222 val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
   229 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
   223 
   230 
   224 
   231 
   225 (** reading of instantiations **)
   232 (** reading of instantiations **)
   226 
   233 
   227 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   234 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   516       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   523       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   517   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   524   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   518 
   525 
   519 (** Below, a "conversion" has type cterm -> thm **)
   526 (** Below, a "conversion" has type cterm -> thm **)
   520 
   527 
   521 val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
   528 val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
   522 
   529 
   523 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   530 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   524 (*Do not rewrite flex-flex pairs*)
   531 (*Do not rewrite flex-flex pairs*)
   525 fun goals_conv pred cv =
   532 fun goals_conv pred cv =
   526   let fun gconv i ct =
   533   let fun gconv i ct =
   527         let val (A,B) = dest_cimplies ct
   534         let val (A,B) = dest_implies ct
   528             val (thA,j) = case term_of A of
   535             val (thA,j) = case term_of A of
   529                   Const("=?=",_)$_$_ => (reflexive A, i)
   536                   Const("=?=",_)$_$_ => (reflexive A, i)
   530                 | _ => (if pred i then cv A else reflexive A, i+1)
   537                 | _ => (if pred i then cv A else reflexive A, i+1)
   531         in  combination (combination refl_cimplies thA) (gconv j B) end
   538         in  combination (combination refl_implies thA) (gconv j B) end
   532         handle TERM _ => reflexive ct
   539         handle TERM _ => reflexive ct
   533   in gconv 1 end;
   540   in gconv 1 end;
   534 
   541 
   535 (*Use a conversion to transform a theorem*)
   542 (*Use a conversion to transform a theorem*)
   536 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   543 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   574 
   581 
   575 (*Calling equal_abs_elim with multiple terms*)
   582 (*Calling equal_abs_elim with multiple terms*)
   576 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   583 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
   577 
   584 
   578 local
   585 local
   579   open Logic
       
   580   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   586   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   581   fun err th = raise THM("flexpair_inst: ", 0, [th])
   587   fun err th = raise THM("flexpair_inst: ", 0, [th])
   582   fun flexpair_inst def th =
   588   fun flexpair_inst def th =
   583     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   589     let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   584         val cterm = cterm_of sign
   590         val cterm = cterm_of sign