subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
authorwenzelm
Mon Feb 17 22:39:20 2014 +0100 (2014-02-17)
changeset 55547384bfd19ee61
parent 55546 76979adf0b96
child 55548 a645277885cf
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
NEWS
src/Doc/IsarImplementation/Tactic.thy
src/Pure/context.ML
src/Pure/more_thm.ML
     1.1 --- a/NEWS	Mon Feb 17 21:37:41 2014 +0100
     1.2 +++ b/NEWS	Mon Feb 17 22:39:20 2014 +0100
     1.3 @@ -358,6 +358,13 @@
     1.4  pass runtime Proof.context (and ensure that the simplified entity
     1.5  actually belongs to it).
     1.6  
     1.7 +* Subtle change of semantics of Thm.eq_thm: theory stamps are not
     1.8 +compared (according to Thm.thm_ord), but assumed to be covered by the
     1.9 +current background theory.  Thus equivalent data produced in different
    1.10 +branches of the theory graph usually coincides (e.g. relevant for
    1.11 +theory merge).  Note that the softer Thm.eq_thm_prop is often more
    1.12 +appropriate than Thm.eq_thm.
    1.13 +
    1.14  
    1.15  *** System ***
    1.16  
     2.1 --- a/src/Doc/IsarImplementation/Tactic.thy	Mon Feb 17 21:37:41 2014 +0100
     2.2 +++ b/src/Doc/IsarImplementation/Tactic.thy	Mon Feb 17 22:39:20 2014 +0100
     2.3 @@ -920,9 +920,8 @@
     2.4    "thm"} has fewer than @{text "n"} premises.
     2.5  
     2.6    \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
     2.7 -  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have
     2.8 -  compatible background theories.  Both theorems must have the same
     2.9 -  conclusions, the same set of hypotheses, and the same set of sort
    2.10 +  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the
    2.11 +  same conclusions, the same set of hypotheses, and the same set of sort
    2.12    hypotheses.  Names of bound variables are ignored as usual.
    2.13  
    2.14    \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
     3.1 --- a/src/Pure/context.ML	Mon Feb 17 21:37:41 2014 +0100
     3.2 +++ b/src/Pure/context.ML	Mon Feb 17 22:39:20 2014 +0100
     3.3 @@ -43,7 +43,6 @@
     3.4    val this_theory: theory -> string -> theory
     3.5    val eq_thy: theory * theory -> bool
     3.6    val subthy: theory * theory -> bool
     3.7 -  val joinable: theory * theory -> bool
     3.8    val merge: theory * theory -> theory
     3.9    val finish_thy: theory -> theory
    3.10    val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    3.11 @@ -246,8 +245,6 @@
    3.12  
    3.13  fun subthy thys = eq_thy thys orelse proper_subthy thys;
    3.14  
    3.15 -fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
    3.16 -
    3.17  
    3.18  (* consistent ancestors *)
    3.19  
     4.1 --- a/src/Pure/more_thm.ML	Mon Feb 17 21:37:41 2014 +0100
     4.2 +++ b/src/Pure/more_thm.ML	Mon Feb 17 22:39:20 2014 +0100
     4.3 @@ -37,7 +37,6 @@
     4.4    val thm_cache: (thm -> 'a) -> thm -> 'a
     4.5    val is_reflexive: thm -> bool
     4.6    val eq_thm: thm * thm -> bool
     4.7 -  val eq_thm_thy: thm * thm -> bool
     4.8    val eq_thm_prop: thm * thm -> bool
     4.9    val eq_thm_strict: thm * thm -> bool
    4.10    val equiv_thm: thm * thm -> bool
    4.11 @@ -191,17 +190,17 @@
    4.12  fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
    4.13    handle TERM _ => false;
    4.14  
    4.15 -fun eq_thm ths =
    4.16 -  Context.joinable (pairself Thm.theory_of_thm ths) andalso
    4.17 -  is_equal (thm_ord ths);
    4.18 +val eq_thm = is_equal o thm_ord;
    4.19  
    4.20 -val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
    4.21  val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
    4.22  
    4.23  fun eq_thm_strict ths =
    4.24 -  eq_thm_thy ths andalso eq_thm ths andalso
    4.25 -    let val (rep1, rep2) = pairself Thm.rep_thm ths
    4.26 -    in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
    4.27 +  eq_thm ths andalso
    4.28 +    let val (rep1, rep2) = pairself Thm.rep_thm ths in
    4.29 +      Theory.eq_thy (#thy rep1, #thy rep2) andalso
    4.30 +      #maxidx rep1 = #maxidx rep2 andalso
    4.31 +      #tags rep1 = #tags rep2
    4.32 +    end;
    4.33  
    4.34  
    4.35  (* pattern equivalence *)