# HG changeset patch
# User blanchet
# Date 1325513320 -3600
# Node ID a109eb27f54f123171ce66b0463b17299e9a48e7
# Parent  0054a9513b374fcead043b2dfa638f74691230cd
ported a dozen of proofs to the "set" type constructor

diff -r 0054a9513b37 -r a109eb27f54f src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Mon Jan 02 14:45:13 2012 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Mon Jan 02 15:08:40 2012 +0100
@@ -23,11 +23,11 @@
   pset  :: "'a set => 'a set"
   order :: "'a set => ('a * 'a) set"
 
-(*lemma "a \<in> {x. P x} \<Longrightarrow> P a"
+lemma "a \<in> {x. P x} \<Longrightarrow> P a"
 proof -
   assume "a \<in> {x. P x}"
-  thus "P a" by metis
-qed*)
+  thus "P a" by (metis mem_Collect_eq)
+qed
 
 lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
 by (metis mem_Collect_eq)
@@ -35,14 +35,14 @@
 lemma "a \<in> {x. P x --> Q x} \<Longrightarrow> a \<in> {x. P x} \<Longrightarrow> a \<in> {x. Q x}"
 by (metis Collect_imp_eq ComplD UnE)
 
-(*lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
+lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A \<and> b \<in> B a"
 proof -
   assume A1: "(a, b) \<in> Sigma A B"
   hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
   have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
   have "b \<in> B a" by (metis F1)
   thus "a \<in> A \<and> b \<in> B a" by (metis F2)
-qed*)
+qed
 
 lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
 by (metis SigmaD1 SigmaD2)
@@ -50,96 +50,91 @@
 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 by (metis (full_types, lam_lifting) CollectD SigmaD1 SigmaD2)
 
-(*lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 proof -
   assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
   hence F1: "a \<in> A" by (metis mem_Sigma_iff)
   have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
-  hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
-  hence "a = f b" by (unfold mem_def)
+  hence "a = f b" by (metis (full_types) mem_Collect_eq)
   thus "a \<in> A \<and> a = f b" by (metis F1)
-qed*)
+qed
 
 lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
 by (metis Collect_mem_eq SigmaD2)
 
-(*lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
+lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
 proof -
   assume A1: "(cl, f) \<in> CLF"
   assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
-  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
   have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
-  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
+  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis mem_Collect_eq)
   thus "f \<in> pset cl" by (metis A1)
-qed*)
+qed
 
-(*lemma
+lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
-by (metis (no_types) Sigma_triv)*)
+by (metis (no_types) Collect_mem_eq Sigma_triv)
 
-(*lemma
+lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
 proof -
   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
-  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
   have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
-  thus "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
-qed*)
+  thus "f \<in> pset cl \<rightarrow> pset cl" by (metis mem_Collect_eq)
+qed
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
 
-(*lemma
+lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 proof -
   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
-  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
   have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
-  hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def)
-  hence "f \<in> Id_on cl `` pset cl" by metis
+  hence "f \<in> Id_on cl `` pset cl" by (metis Int_commute Image_Id_on mem_Collect_eq)
   hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
   thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
-qed*)
+qed
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
 by auto
 
-(*lemma
+lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
-by (metis (lam_lifting) Sigma_triv subsetD)*)
+by (metis (lam_lifting) CollectD Sigma_triv subsetD)
 
-(*lemma
+lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
-by (metis (lam_lifting) Int_Collect SigmaD2 inf1I mem_def)*)
+by (metis (lam_lifting) CollectD Sigma_triv)
 
-(*lemma
+lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
-by (metis (lam_lifting) Collect_def Sigma_triv mem_def subsetD)*)
+by (metis (lam_lifting) CollectD Sigma_triv subsetD)
 
-(*lemma
+lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
-by (metis (lam_lifting) Collect_def Sigma_triv mem_def)*)
+by (metis (lam_lifting) CollectD Sigma_triv)
 
-(*lemma
+lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
    (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
-by auto*)
+by auto
 
 lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
 apply (induct xs)
@@ -153,16 +148,16 @@
  apply (metis map.simps(1) zip_Nil)
 by auto
 
-(*lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
-by (metis Collect_def image_eqI mem_def subsetD)*)
+lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
+by (metis mem_Collect_eq image_eqI subsetD)
 
-(*lemma
+lemma
   "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
    (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
-by (metis Collect_def imageI mem_def set_rev_mp)*)
+by (metis mem_Collect_eq imageI set_rev_mp)
 
-(*lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
-by (metis (lam_lifting) imageE)*)
+lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
+by (metis (lam_lifting) imageE)
 
 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
 by (metis map_pair_def map_pair_surj_on)