src/Pure/drule.ML
changeset 13325 5b5e12f0aee0
parent 13198 3e40f48a500f
child 13368 8f8ba32d148b
equal deleted inserted replaced
13324:39d1b3a4c6f4 13325:5b5e12f0aee0
   128   val conj_intr_list: thm list -> thm
   128   val conj_intr_list: thm list -> thm
   129   val conj_elim: thm -> thm * thm
   129   val conj_elim: thm -> thm * thm
   130   val conj_elim_list: thm -> thm list
   130   val conj_elim_list: thm -> thm list
   131   val conj_elim_precise: int -> thm -> thm list
   131   val conj_elim_precise: int -> thm -> thm list
   132   val conj_intr_thm: thm
   132   val conj_intr_thm: thm
       
   133   val abs_def: thm -> thm
   133 end;
   134 end;
   134 
   135 
   135 structure Drule: DRULE =
   136 structure Drule: DRULE =
   136 struct
   137 struct
   137 
   138 
   587         (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
   588         (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
   588   end;
   589   end;
   589 
   590 
   590 val refl_implies = reflexive implies;
   591 val refl_implies = reflexive implies;
   591 
   592 
       
   593 fun abs_def thm =
       
   594   let
       
   595     val (_, cvs) = strip_comb (fst (dest_equals (cprop_of thm)));
       
   596     val thm' = foldr (fn (ct, thm) => Thm.abstract_rule
       
   597       (case term_of ct of Var ((a, _), _) => a | Free (a, _) => a | _ => "x")
       
   598         ct thm) (cvs, thm)
       
   599   in transitive
       
   600     (symmetric (eta_conversion (fst (dest_equals (cprop_of thm'))))) thm'
       
   601   end;
       
   602 
   592 
   603 
   593 (*** Some useful meta-theorems ***)
   604 (*** Some useful meta-theorems ***)
   594 
   605 
   595 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   606 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   596 val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
   607 val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));