As previously discussed in the thread "Safe for boolean equality", the current strategy for using equality hypotheses 'x = expr', in which substitution for x is done and then the hypothesis is discarded, is unsafe. The conclusion of that discussion was that the problem was annoying but fairly rare, that there is some concern it may become more common as local are used more extensively, and that fixing it would probably require a painful change to the behaviour of auto.

The problem is that by forgetting what x equates to in our goal, we lose the connection from the goal to the context outside our goal. There may be other facts available that name x. There may also be schematic variables which could be instantiated to "hd x" but not the bound variable replacing it.

The simple solution in my mind is to keep the equality in the goal, and since noone else seemed interested I thought I'd attempt to do this myself and see how difficult it was. I attach the resulting patch. After several rounds of bugfixes and compatibility improvements, it requires 23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word.

The code change in Provers/hypsubst.ML adds code for counting the free and bound variables in a goal, and checking whether either side of an equality hypothesis is a unique variable, occuring nowhere else. The main substitution algorithms avoid using such equalities and also preserve rather than delete the hypothesis they select. There is a new tactic for discarding these equalities, which is added as an unsafe wrapper in Context_Rules, allowing all unsafe tactics to behave roughly as before. The version of hypsubst called by blast is left unchanged, as blast proofs seem to be highly sensitive to changes. There is plenty of room for optimisation, I tried to keep the diff readable.

Three kinds of proofs seem to need fixing:
1. proofs where subgoal_tac or similar now needs to refer to xa rather than x. 2. proofs where erule ssubst, drule sym/arg_cong/fun_cong etc need to be further specialised. 3. proofs where variables are eliminated and then induction is performed, i.e. the word library. Explicitly adding "apply hypsubst_thin" seems the best solution.

At this stage I'm not sure how to proceed. I would be very happy to see safe get safer, but I'm not sure how acceptable this level of incompatibility is in an Isabelle change. There's an alternative approach I thought of recently but haven't tried yet - replacing used equalities with meta-equalities - which might reduce the incompatibilities of type 2.

I haven't checked whether there are any performance implications.

I'd be keen to hear what other Isabelle developers think.

Yours,
    Thomas.


diff -r 2e1b6a8a0fdd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy       Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Divides.thy       Mon Aug 23 17:33:59 2010 +1000
@@ -429,7 +429,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "-(y * k) = y * - k")
- apply (erule ssubst)
+ apply (simp only:)
  apply (erule div_mult_self1_is_id)
 apply simp
 done
@@ -438,8 +438,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
  apply simp
 apply simp
 done
diff -r 2e1b6a8a0fdd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/HOL.thy   Mon Aug 23 17:33:59 2010 +1000
@@ -871,6 +871,7 @@
   Hypsubst.hypsubst_setup
   (*prevent substitution on bool*)
   #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  #> Context_Rules.addWrapper (fn tac => Hypsubst.thin_triv_tac false ORELSE' 
tac)
 end
 *}
 
diff -r 2e1b6a8a0fdd src/HOL/Int.thy
--- a/src/HOL/Int.thy   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Int.thy   Mon Aug 23 17:33:59 2010 +1000
@@ -542,7 +542,7 @@
 lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat 
(Suc n))"
 apply (cases x)
 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x="y - Suc x" in exI, arith)
+apply (rule_tac x="y - Suc xa" in exI, arith)
 done
 
 
diff -r 2e1b6a8a0fdd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy      Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Library/Multiset.thy      Mon Aug 23 17:33:59 2010 +1000
@@ -1116,7 +1116,7 @@
  apply (simp (no_asm))
  apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  apply (simp (no_asm_simp) add: add_assoc [symmetric])
- apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
  apply (simp add: diff_union_single_conv)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
@@ -1127,7 +1127,7 @@
  apply (rule conjI)
   apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (rule conjI)
-  apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
+  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, 
simp)
   apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
diff -r 2e1b6a8a0fdd src/HOL/Nat.thy
--- a/src/HOL/Nat.thy   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Nat.thy   Mon Aug 23 17:33:59 2010 +1000
@@ -1076,7 +1076,7 @@
     -- {* elimination of @{text -} on @{text nat} *}
 by (cases "a < b")
   (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
-    not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero)
+    not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
 
 lemma nat_diff_split_asm:
   "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
diff -r 2e1b6a8a0fdd src/HOL/Parity.thy
--- a/src/HOL/Parity.thy        Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Parity.thy        Mon Aug 23 17:33:59 2010 +1000
@@ -66,9 +66,10 @@
   by presburger
 
 lemma even_times_anything: "even (x::int) ==> even (x * y)"
-  by algebra
+  by (simp add: int_even_iff_2_dvd)
 
-lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
+lemma anything_times_even: "even (y::int) ==> even (x * y)"
+  by (simp add: int_even_iff_2_dvd)
 
 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" 
   by (simp add: even_def zmod_zmult1_eq)
diff -r 2e1b6a8a0fdd src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy        Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Transcendental.thy        Mon Aug 23 17:33:59 2010 +1000
@@ -1909,7 +1909,7 @@
 apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y")
 apply (rule_tac [2] IVT2)
 apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos)
-apply (cut_tac x = xa and y = y in linorder_less_linear)
+apply (cut_tac x = xa and y = ya in linorder_less_linear)
 apply (rule ccontr, auto)
 apply (drule_tac f = cos in Rolle)
 apply (drule_tac [5] f = cos in Rolle)
@@ -2184,9 +2184,9 @@
 
 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
 apply (cut_tac y = y in lemma_tan_total1, auto)
-apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
-apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
-apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
+apply (cut_tac x = xa and y = ya in linorder_less_linear, auto)
+apply (subgoal_tac [2] "\<exists>z. ya < z & z < xa & DERIV tan z :> 0")
+apply (subgoal_tac "\<exists>z. xa < z & z < ya & DERIV tan z :> 0")
 apply (rule_tac [4] Rolle)
 apply (rule_tac [2] Rolle)
 apply (auto intro!: DERIV_tan DERIV_isCont exI 
diff -r 2e1b6a8a0fdd src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy      Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Word/BinBoolList.thy      Mon Aug 23 17:33:59 2010 +1000
@@ -570,7 +570,7 @@
 
 lemma takefill_same': 
   "l = length xs ==> takefill fill l xs = xs"
-  by clarify (induct xs, auto)
+  by (induct xs arbitrary: l, auto)
  
 lemmas takefill_same [simp] = takefill_same' [OF refl]
 
diff -r 2e1b6a8a0fdd src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy    Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Word/TdThs.thy    Mon Aug 23 17:33:59 2010 +1000
@@ -197,7 +197,7 @@
    prefer 2
    apply (simp add: o_assoc [symmetric])
   apply (rule ext)
-  apply (drule fun_cong)
+  apply (drule_tac f="?a o ?b" in fun_cong)
   apply simp
   done
 
diff -r 2e1b6a8a0fdd src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy        Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Word/WordShift.thy        Mon Aug 23 17:33:59 2010 +1000
@@ -394,7 +394,7 @@
   "us = of_bl bl >> n ==> length bl <= size us --> 
    us = of_bl (take (length bl - n) bl)"
   apply (unfold shiftr_def)
-  apply hypsubst
+  apply hypsubst_thin
   apply (unfold word_size)
   apply (induct n)
    apply clarsimp
@@ -428,6 +428,7 @@
   apply clarsimp
   apply (case_tac x, force)
   apply (case_tac m, auto)
+  apply hypsubst_thin
   apply (drule sym)
   apply auto
   apply (induct_tac list, auto)
@@ -442,6 +443,7 @@
   apply clarsimp
   apply (case_tac x, force)
   apply (case_tac m, auto)
+  apply hypsubst_thin
   apply (drule sym)
   apply auto
   apply (induct_tac list, auto)
@@ -934,6 +936,7 @@
   apply safe
    defer
    apply (clarsimp split: prod.splits)
+   apply hypsubst_thin
    apply (drule word_ubin.norm_Rep [THEN ssubst])
    apply (drule split_bintrunc)
    apply (simp add : of_bl_def bl2bin_drop word_size
diff -r 2e1b6a8a0fdd src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy      Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/ex/Dedekind_Real.thy      Mon Aug 23 17:33:59 2010 +1000
@@ -307,7 +307,7 @@
      "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u 
\<in> add_set A B. y < u"
 apply (auto simp add: add_set_def)
 apply (frule preal_exists_greater [of A], auto) 
-apply (rule_tac x="u + y" in exI)
+apply (rule_tac x="u + ya" in exI)
 apply (auto intro: add_strict_left_mono)
 done
 
@@ -434,7 +434,7 @@
      "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u 
\<in> mult_set A B. y < u"
 apply (auto simp add: mult_set_def)
 apply (frule preal_exists_greater [of A], auto) 
-apply (rule_tac x="u * y" in exI)
+apply (rule_tac x="u * ya" in exI)
 apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
                    mult_strict_right_mono)
 done
@@ -1583,7 +1583,7 @@
       "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal 
m)"
 apply (simp add: real_of_preal_def real_zero_def, cases x)
 apply (auto simp add: real_minus add_ac)
-apply (cut_tac x = x and y = y in linorder_less_linear)
+apply (cut_tac x = xa and y = y in linorder_less_linear)
 apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric])
 done
 
diff -r 2e1b6a8a0fdd src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/Provers/hypsubst.ML   Mon Aug 23 17:33:59 2010 +1000
@@ -54,6 +54,7 @@
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
+  val thin_triv_tac          : bool -> int -> tactic
 end;
 
 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
@@ -115,27 +116,55 @@
      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
                        then raise Match
                        else false               (*eliminates u*)
-     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
+     | (Free f, _) =>  if bnd orelse Logic.occs(Free f,u) orelse
                           novars andalso has_vars u
                        then raise Match
                        else true                (*eliminates t*)
-     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
+     | (_, Free f) =>  if bnd orelse Logic.occs(Free f,t) orelse
                           novars andalso has_vars t
                        then raise Match
                        else false               (*eliminates u*)
      | _ => raise Match;
 
+(* Counts the occurences of Free and Bound variables in a term. *)
+fun count_vars' _ (Free f) = Termtab.map_default (Free f, 0) (fn x => x + 1)
+  | count_vars' _ (Var _) = I
+  | count_vars' _ (Const _) = I
+  | count_vars' n (Bound m) = Termtab.map_default (Bound (m - n), 0)
+      (fn x => x + 1)
+  | count_vars' n (Abs (_, _, t)) = count_vars' (n + 1) t
+  | count_vars' n (f $ x) = count_vars' n f o count_vars' n x
+
+fun count_vars ts = fold (count_vars' 0) ts Termtab.empty
+
+(* An equality hypothesis 'x = y' is trivial if substituting with it would have
+   no useful effect. The principal test for this is if x or y is a unique
+   variable, occuring nowhere else in the goal.  The exception to the rule is
+   if x is bound and y is unique but free. *)
+fun triv_asm bnd t = let
+    val vars = count_vars (Logic.strip_assums_concl t
+        :: Logic.strip_assums_hyp t)
+    fun triv v = (if bnd then is_Bound v else true) 
+      andalso (Termtab.lookup vars v = SOME 1)
+  in fn eq => case try (pairself Envir.beta_eta_contract
+            o Data.dest_eq o Data.dest_Trueprop) eq of
+      NONE => false
+    | SOME (a, b) => if exists is_Bound [a, b]
+        then exists triv (filter is_Bound [a, b])
+        else exists triv [a, b]
+  end
+
 (*Locates a substitutable variable on the left (resp. right) of an equality
    assumption.  Returns the number of intervening assumptions. *)
-fun eq_var bnd novars =
-  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
-        | eq_var_aux k (Const("==>",_) $ A $ B) =
-              ((k, inspect_pair bnd novars
-                    (Data.dest_eq (Data.dest_Trueprop A)))
-               handle TERM _ => eq_var_aux (k+1) B
-                 | Match => eq_var_aux (k+1) B)
-        | eq_var_aux k _ = raise EQ_VAR
-  in  eq_var_aux 0  end;
+fun eq_var bnd novars skiptriv t = let
+    val triv = if skiptriv then triv_asm false t else K false
+    fun eq_var_aux hyp =
+      (if (inspect_pair bnd novars (Data.dest_eq (Data.dest_Trueprop hyp)))
+      then if triv hyp then NONE else SOME true
+      else SOME false)
+        handle TERM _ => NONE | Match => NONE
+  in get_index eq_var_aux (Logic.strip_assums_hyp t) |> the
+    handle Option => raise EQ_VAR end
 
 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   No vars are allowed here, as simpsets are built from meta-assumptions*)
@@ -154,11 +183,12 @@
   fun gen_hyp_subst_tac bnd =
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
-        val (k, _) = eq_var bnd true Bi
+        val (k, symopt) = eq_var bnd true true Bi
         val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) 
empty_ss
           setmksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
-        etac thin_rl i, rotate_tac (~k) i]
+        if not symopt then dtac Data.sym i THEN rotate_tac (~1) i else all_tac,
+        rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
     in REPEAT_DETERM1 o tac end;
 
@@ -201,28 +231,41 @@
 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
 (* premises containing meta-implications or quantifiers                *)
 
+(* copied from blast.ML *)
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+
+val dup_subst = rev_dup_elim ssubst
+
 (*Old version of the tactic above -- slower but the only way
   to handle equalities containing Vars.*)
 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
       let val n = length(Logic.strip_assums_hyp Bi) - 1
-          val (k,symopt) = eq_var bnd false Bi
+          val (k,symopt) = eq_var bnd false true Bi
+          val rl = if symopt then dup_subst else (Data.sym RS dup_subst)
       in
          DETERM
            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
                    rotate_tac 1 i,
                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
-                   inst_subst_tac symopt (if symopt then ssubst else 
Data.subst) i,
+                   inst_subst_tac symopt rl i,
                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
       end
       handle THM _ => no_tac | EQ_VAR => no_tac);
 
-(*Substitutes for Free or Bound variables*)
-val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
-        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
+fun thin_triv_tac bnd = SUBGOAL (fn (t, i) => let
+    val n = find_index (triv_asm bnd t) (Logic.strip_assums_hyp t)
+  in if n <> ~1 then EVERY' 
+    [rotate_tac n, etac thin_rl, rotate_tac (~ n)] i else no_tac end)
+
+(*Substitutes for Free or Bound variables, thins out Bound equalities *)
+val hyp_subst_tac = REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
+        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false,
+        thin_triv_tac true];
 
 (*Substitutes for Bound variables only -- this is always safe*)
 val bound_hyp_subst_tac =
-    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
+    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true
+      ORELSE' thin_triv_tac true;
 
 
 (** Version for Blast_tac.  Hyps that are affected by the substitution are
@@ -256,7 +299,7 @@
 
 
 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
-      let val (k,symopt) = eq_var false false Bi
+      let val (k,symopt) = eq_var false false false Bi
           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
           (*omit selected equality, returning other hyps*)
           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
@@ -282,10 +325,15 @@
 
 (* theory setup *)
 
+val hypsubst_thin = REPEAT_DETERM1 o (hyp_subst_tac ORELSE' thin_triv_tac 
false)
+
 val hypsubst_setup =
   Method.setup @{binding hypsubst}
     (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
     "substitution using an assumption (improper)" #>
+  Method.setup @{binding hypsubst_thin}
+    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hypsubst_thin))))
+    "substitution and discarding of an assumption (improper)" #>
   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K 
(SIMPLE_METHOD' (stac th))))
     "simple substitution";
 
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to