added trans_terms/props;
authorwenzelm
Thu Dec 14 15:31:21 2006 +0100 (2006-12-14 ago)
changeset 21844e10b8bd7a886
parent 21843 2015be1b6a03
child 21845 da545169fe06
added trans_terms/props;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Dec 14 15:31:20 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Dec 14 15:31:21 2006 +0100
     1.3 @@ -15,6 +15,8 @@
     1.4    val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     1.5      (term * (bstring * thm)) list * Proof.context
     1.6    val export: Proof.context -> Proof.context -> thm -> thm list * thm
     1.7 +  val trans_terms: Proof.context -> thm list -> thm
     1.8 +  val trans_props: Proof.context -> thm list -> thm
     1.9    val print_rules: Proof.context -> unit
    1.10    val defn_add: attribute
    1.11    val defn_del: attribute
    1.12 @@ -111,6 +113,28 @@
    1.13    in (map Drule.abs_def defs, th') end;
    1.14  
    1.15  
    1.16 +(* basic transitivity reasoning -- modulo beta-eta *)
    1.17 +
    1.18 +local
    1.19 +
    1.20 +val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
    1.21 +
    1.22 +fun trans_list _ _ [] = raise Empty
    1.23 +  | trans_list trans ctxt (th :: raw_eqs) =
    1.24 +      (case filter_out is_trivial raw_eqs of
    1.25 +        [] => th
    1.26 +      | eqs =>
    1.27 +          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
    1.28 +          in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
    1.29 +
    1.30 +in
    1.31 +
    1.32 +val trans_terms = trans_list (fn eq2 => fn eq1 => eq2 COMP (eq1 COMP Drule.transitive_thm));
    1.33 +val trans_props = trans_list (fn eq => fn th => th COMP (eq COMP Drule.equal_elim_rule1));
    1.34 +
    1.35 +end;
    1.36 +
    1.37 +
    1.38  
    1.39  (** defived definitions **)
    1.40