src/Pure/drule.ML
changeset 68727 ec0b2833cfc4
parent 68539 6740e3611a86
child 69023 cef000855cf4
equal deleted inserted replaced
68726:782d6b89fb19 68727:ec0b2833cfc4
    96   val dummy_thm: thm
    96   val dummy_thm: thm
    97   val free_dummy_thm: thm
    97   val free_dummy_thm: thm
    98   val is_sort_constraint: term -> bool
    98   val is_sort_constraint: term -> bool
    99   val sort_constraintI: thm
    99   val sort_constraintI: thm
   100   val sort_constraint_eq: thm
   100   val sort_constraint_eq: thm
   101   val sort_constraint_intr: indexname * sort -> thm -> thm
       
   102   val sort_constraint_intr_shyps: thm -> thm
       
   103   val with_subgoal: int -> (thm -> thm) -> thm -> thm
   101   val with_subgoal: int -> (thm -> thm) -> thm -> thm
   104   val comp_no_flatten: thm * int -> int -> thm -> thm
   102   val comp_no_flatten: thm * int -> int -> thm -> thm
   105   val rename_bvars: (string * string) list -> thm -> thm
   103   val rename_bvars: (string * string) list -> thm -> thm
   106   val rename_bvars': string option list -> thm -> thm
   104   val rename_bvars': string option list -> thm -> thm
   107   val incr_indexes: thm -> thm -> thm
   105   val incr_indexes: thm -> thm -> thm
   646   store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>)))
   644   store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>)))
   647     (Thm.equal_intr
   645     (Thm.equal_intr
   648       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
   646       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
   649         (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
   647         (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
   650       (implies_intr_list [A, C] (Thm.assume A)));
   648       (implies_intr_list [A, C] (Thm.assume A)));
   651 
       
   652 val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
       
   653 
       
   654 fun sort_constraint_intr tvar thm =
       
   655   Thm.equal_elim
       
   656     (Thm.instantiate
       
   657       ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
       
   658        [((("A", 0), propT), Thm.cprop_of thm)])
       
   659       sort_constraint_eq') thm;
       
   660 
       
   661 fun sort_constraint_intr_shyps raw_thm =
       
   662   let val thm = Thm.strip_shyps raw_thm in
       
   663     (case Thm.extra_shyps thm of
       
   664       [] => thm
       
   665     | shyps =>
       
   666         let
       
   667           val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
       
   668           val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
       
   669         in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
       
   670   end;
       
   671 
   649 
   672 end;
   650 end;
   673 
   651 
   674 
   652 
   675 (* HHF normalization *)
   653 (* HHF normalization *)