merged

--- a/src/HOL/Library/FuncSet.thy	Mon Mar 01 15:09:57 2021 +0100
+++ b/src/HOL/Library/FuncSet.thy	Mon Mar 01 14:47:08 2021 +0000
@@ -175,9 +175,6 @@
 lemma restrict_cong: "I = J \<Longrightarrow> (\<And>i. i \<in> J =simp=> f i = g i) \<Longrightarrow> restrict f I = restrict g J"
   by (auto simp: restrict_def fun_eq_iff simp_implies_def)
 
-lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B"
-  by (simp add: Pi_def restrict_def)
-
 lemma restrictI[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> Pi A B"
   by (simp add: Pi_def restrict_def)
 
@@ -435,6 +432,9 @@
 lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   by (simp add: PiE_def Pi_iff)
 
+lemma restrict_PiE_iff [simp]: "restrict f I \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i \<in> I. f i \<in> X i)"
+  by (simp add: PiE_iff)
+
 lemma ext_funcset_to_sing_iff [simp]: "A \<rightarrow>\<^sub>E {a} = {\<lambda>x\<in>A. a}"
   by (auto simp: PiE_def Pi_iff extensionalityI)
 
@@ -495,10 +495,7 @@
 lemma extensional_funcset_fun_upd_restricts_rangeI:
   "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f \<in> (insert x S) \<rightarrow>\<^sub>E T \<Longrightarrow> f(x := undefined) \<in> S \<rightarrow>\<^sub>E (T - {f x})"
   unfolding extensional_funcset_def extensional_def
-  apply auto
-  apply (case_tac "x = xa")
-  apply auto
-  done
+  by (auto split: if_split_asm)
 
 lemma extensional_funcset_fun_upd_extends_rangeI:
   assumes "a \<in> T" "f \<in> S \<rightarrow>\<^sub>E (T - {a})"

--- a/src/HOL/Metis_Examples/Tarski.thy	Mon Mar 01 15:09:57 2021 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Mar 01 14:47:08 2021 +0000
@@ -905,8 +905,8 @@
 
 
 lemma (in Tarski) intY1_func: "(\<lambda>x \<in> intY1. f x) \<in> intY1 \<rightarrow> intY1"
-apply (rule restrict_in_funcset)
-apply (metis intY1_f_closed restrict_in_funcset)
+apply (rule restrictI)
+apply (metis intY1_f_closed)
 done
 
 
@@ -1018,15 +1018,8 @@
 
 theorem (in CLF) Tarski_full:
      "(| pset = P, order = induced P r|) \<in> CompleteLattice"
-(*sledgehammer*)
-apply (rule CompleteLatticeI_simp)
-apply (rule fixf_po, clarify)
-(*never proved, 2007-01-22*)
+  using A_def CLF_axioms P_def Tarski.intro Tarski_axioms.intro fixf_po r_def by blast
 (*sledgehammer*)
-apply (simp add: P_def A_def r_def)
-apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
-  OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
-done
 
 declare (in CLF) fixf_po [rule del] P_def [simp del] A_def [simp del] r_def [simp del]
          Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]