added implies_intr_goals;
authorwenzelm
Tue Oct 16 23:00:21 2001 +0200 (2001-10-16)
changeset 11815ef7619398680
parent 11814 1de4a3321976
child 11816 545aab7410ac
added implies_intr_goals;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Oct 16 22:59:30 2001 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Oct 16 23:00:21 2001 +0200
     1.3 @@ -96,26 +96,25 @@
     1.4    val corollaryK        : string
     1.5    val internalK         : string
     1.6    val kind_internal     : 'a attribute
     1.7 -  val has_internal	: tag list -> bool
     1.8 +  val has_internal      : tag list -> bool
     1.9    val close_derivation  : thm -> thm
    1.10    val compose_single    : thm * int * thm -> thm
    1.11 -  val add_rules		: thm list -> thm list -> thm list
    1.12 -  val del_rules		: thm list -> thm list -> thm list
    1.13 -  val merge_rules	: thm list * thm list -> thm list
    1.14 -  val norm_hhf_eq	: thm
    1.15 +  val add_rules         : thm list -> thm list -> thm list
    1.16 +  val del_rules         : thm list -> thm list -> thm list
    1.17 +  val merge_rules       : thm list * thm list -> thm list
    1.18 +  val norm_hhf_eq       : thm
    1.19    val triv_goal         : thm
    1.20    val rev_triv_goal     : thm
    1.21 +  val implies_intr_goals: cterm list -> thm -> thm
    1.22    val freeze_all        : thm -> thm
    1.23    val mk_triv_goal      : cterm -> thm
    1.24 -  val mk_cgoal          : cterm -> cterm
    1.25 -  val assume_goal       : cterm -> thm
    1.26    val tvars_of_terms    : term list -> (indexname * sort) list
    1.27    val vars_of_terms     : term list -> (indexname * typ) list
    1.28    val tvars_of          : thm -> (indexname * sort) list
    1.29    val vars_of           : thm -> (indexname * typ) list
    1.30    val unvarifyT         : thm -> thm
    1.31    val unvarify          : thm -> thm
    1.32 -  val tvars_intr_list	: string list -> thm -> thm
    1.33 +  val tvars_intr_list   : string list -> thm -> thm
    1.34  end;
    1.35  
    1.36  structure Drule: DRULE =
    1.37 @@ -313,7 +312,7 @@
    1.38  (*Specialization over a list of cterms*)
    1.39  fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
    1.40  
    1.41 -(* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
    1.42 +(* maps A1,...,An |- B   to   [| A1;...;An |] ==> B  *)
    1.43  fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
    1.44  
    1.45  (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
    1.46 @@ -392,7 +391,7 @@
    1.47     Any remaining trailing positions are left unchanged. *)
    1.48  val rearrange_prems = let
    1.49    fun rearr new []      thm = thm
    1.50 -  |   rearr new (p::ps) thm = rearr (new+1) 
    1.51 +  |   rearr new (p::ps) thm = rearr (new+1)
    1.52       (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
    1.53       (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
    1.54    in rearr 0 end;
    1.55 @@ -752,6 +751,10 @@
    1.56  val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
    1.57  fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
    1.58  
    1.59 +fun implies_intr_goals cprops thm =
    1.60 +  implies_elim_list (implies_intr_list cprops thm) (map assume_goal cprops)
    1.61 +  |> implies_intr_list (map mk_cgoal cprops);
    1.62 +
    1.63  
    1.64  
    1.65  (** variations on instantiate **)