# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 865ce93ce0257d4d1a58413b5af57b7416aa0b9b
# Parent  ebf603e5406114d669f5d01eb6cfa04faa9caf14
handle equality proxy in a more backward-compatible way

diff -r ebf603e54061 -r 865ce93ce025 src/HOL/Metis_Examples/HO_Reas.thy
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
@@ -58,6 +58,16 @@
 
 text {* Proxies for logical constants *}
 
+lemma "id (op =) x x"
+sledgehammer [type_sys = erased, expect = none] (id_apply)
+sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
+sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+by (metis id_apply)
+
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags!, expect = some] (id_apply)
diff -r ebf603e54061 -r 865ce93ce025 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -540,6 +540,7 @@
   | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"
   | fn_isa_to_met_sublevel "c_implies" = "c_fimplies"
   | fn_isa_to_met_sublevel x = x
+
 fun fn_isa_to_met_toplevel "equal" = "="
   | fn_isa_to_met_toplevel x = x
 
@@ -640,6 +641,7 @@
       end
   end;
 
+(* "true" indicates that a sound type encoding is needed *)
 val metis_helpers =
   [("COMBI", (false, @{thms Meson.COMBI_def})),
    ("COMBK", (false, @{thms Meson.COMBK_def})),
@@ -647,8 +649,11 @@
    ("COMBC", (false, @{thms Meson.COMBC_def})),
    ("COMBS", (false, @{thms Meson.COMBS_def})),
    ("fequal",
-    (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
-                   fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+    (* This is a lie: Higher-order equality doesn't need a sound type encoding.
+       However, this is done so for backward compatibility: Including the
+       equality helpers by default in Metis breaks a few existing proofs. *)
+    (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+                  fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    ("fFalse", (true, [@{lemma "x = fTrue | x = fFalse"
                           by (unfold fFalse_def fTrue_def) fast}])),
    ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),