# HG changeset patch
# User blanchet
# Date 1676296918 -3600
# Node ID 27be31d7ad88f6312a779f7c2598c6f06fc89112
# Parent  9a60a2d19a4c2876f7107c6cb961b57a56540f16
careful eta-contraction in Metis to keep argument to All and Ex expanded

diff -r 9a60a2d19a4c -r 27be31d7ad88 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Sun Feb 12 22:05:02 2023 +0100
+++ b/src/HOL/Metis.thy	Mon Feb 13 15:01:58 2023 +0100
@@ -27,7 +27,8 @@
 lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A"
 unfolding select_def by (rule not_atomize)
 
-lemma select_FalseI: "False \<Longrightarrow> select False" by simp
+lemma select_FalseI: "False \<Longrightarrow> select False"
+by simp
 
 definition lambda :: "'a \<Rightarrow> 'a" where
 "lambda = (\<lambda>x. x)"
diff -r 9a60a2d19a4c -r 27be31d7ad88 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Sun Feb 12 22:05:02 2023 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Feb 13 15:01:58 2023 +0100
@@ -54,8 +54,21 @@
   let val T = fastype_of t
   in \<^Const>\<open>Meson.skolem T for t\<close> end
 
+fun eta_expand_All_Ex_arg ((cst as (Const _)) $ Abs (s, T, t')) =
+    cst $ Abs (s, T, eta_expand_All_Ex_arg t')
+  | eta_expand_All_Ex_arg ((cst as (Const (cst_s, cst_T))) $ t') =
+    if member (op =) [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>] cst_s then
+      cst $ Abs (Name.uu, domain_type (domain_type cst_T),
+        incr_boundvars 1 (eta_expand_All_Ex_arg t') $ Bound 0)
+    else
+      cst $ eta_expand_All_Ex_arg t'
+  | eta_expand_All_Ex_arg (Abs (s, T, t')) = Abs (s, T, eta_expand_All_Ex_arg t')
+  | eta_expand_All_Ex_arg (t1 $ t2) =
+    eta_expand_All_Ex_arg t1 $ eta_expand_All_Ex_arg t2
+  | eta_expand_All_Ex_arg t = t
+
 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
-  | beta_eta_in_abs_body t = Envir.beta_eta_contract t
+  | beta_eta_in_abs_body t = eta_expand_All_Ex_arg (Envir.beta_eta_contract t)
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun old_skolem_defs th =