# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 08970468f99b01861fd4d024ac3eba8629c5dcb7
# Parent  ccb904a09e70dcdd257c04cdea28690cf7bb025e
more "metis" calls in example

diff -r ccb904a09e70 -r 08970468f99b src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Fri Nov 18 11:47:12 2011 +0100
@@ -8,16 +8,14 @@
 header {* Example Featuring Metis's Support for Lambda-Abstractions *}
 
 theory Abstraction
-imports Main "~~/src/HOL/Library/FuncSet"
+imports "~~/src/HOL/Library/FuncSet"
 begin
 
-declare [[metis_new_skolemizer]]
-
 (* For Christoph Benzmüller *)
 lemma "x < 1 \<and> ((op =) = (op =)) \<Longrightarrow> ((op =) = (op =)) \<and> x < (2::nat)"
 by (metis nat_1_add_1 trans_less_add2)
 
-lemma "(op = ) = (%x y. y = x)"
+lemma "(op = ) = (\<lambda>x y. y = x)"
 by metis
 
 consts
@@ -25,20 +23,20 @@
   pset  :: "'a set => 'a set"
   order :: "'a set => ('a * 'a) set"
 
-lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
+lemma "a \<in> {x. P x} \<Longrightarrow> P a"
 proof -
   assume "a \<in> {x. P x}"
   hence "a \<in> P" by (metis Collect_def)
   thus "P a" by (metis mem_def)
 qed
 
-lemma Collect_triv: "a \<in> {x. P x} ==> P a"
+lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
 by (metis mem_Collect_eq)
 
-lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
+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 ==> a \<in> A & b \<in> B a"
+lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
 proof -
   assume A1: "(a, b) \<in> Sigma A B"
   hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
@@ -47,17 +45,11 @@
   thus "a \<in> A \<and> b \<in> B a" by (metis F2)
 qed
 
-lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
+lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
 by (metis SigmaD1 SigmaD2)
 
 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
-(* Metis says this is satisfiable!
-by (metis CollectD SigmaD1 SigmaD2)
-*)
-by (meson CollectD SigmaD1 SigmaD2)
-
-lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
-by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
+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"
 proof -
@@ -69,44 +61,42 @@
   thus "a \<in> A \<and> a = f b" by (metis F1)
 qed
 
-lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
+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 ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> 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 "f \<in> pset cl" by (metis A1)
-  thus "f \<in> pset cl" by metis
+  thus "f \<in> pset cl" by (metis A1)
 qed
 
 lemma
-    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
-    f \<in> pset cl \<rightarrow> pset cl"
+  "(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) Collect_def Sigma_triv mem_def)
 
 lemma
-    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
-    f \<in> pset cl \<rightarrow> pset cl"
+  "(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
-  hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
-  thus "f \<in> pset cl \<rightarrow> pset cl" by metis
+  thus "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
 qed
 
 lemma
-    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
-    f \<in> pset cl \<inter> cl"
+  "(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
-    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
-    f \<in> pset cl \<inter> cl"
+  "(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)
@@ -118,71 +108,73 @@
 qed
 
 lemma
-    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
+  "(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 "(cl,f) \<in> CLF ==>
-   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
+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) Collect_def Sigma_triv mem_def subsetD)
+
+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)
+
+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)
+
+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)
+
+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
 
-lemma "(cl,f) \<in> CLF ==>
-   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
-   f \<in> pset cl \<inter> cl"
-by auto
-
-lemma
-   "(cl,f) \<in> CLF ==>
-    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
-    f \<in> pset cl \<rightarrow> pset cl"
-by fast
-
-lemma
-  "(cl,f) \<in> CLF ==>
-   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
-   f \<in> pset cl \<rightarrow> pset cl"
-by auto
-
-lemma
-  "(cl,f) \<in> CLF ==>
-   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
-   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
-by auto
-
-lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
-apply (induct xs)
- apply (metis map.simps(1) zip_Nil)
-by (metis (lam_lifting, no_types) map.simps(2) zip_Cons_Cons)
-
-lemma "map (%w. (w -> w, w \<times> w)) xs =
-       zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
+lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
 apply (induct xs)
  apply (metis map.simps(1) zip_Nil)
 by auto
 
-lemma "(%x. Suc (f x)) ` {x. even x} <= A ==> \<forall>x. even x --> Suc (f x) \<in> A"
+lemma
+  "map (\<lambda>w. (w -> w, w \<times> w)) xs =
+   zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
+apply (induct xs)
+ 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 "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
-       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
+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)
 
-lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"
-(* sledgehammer *)
-by auto
+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: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
+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)
 
 lemma image_TimesB:
-    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
-(* sledgehammer *)
+    "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
 by force
 
 lemma image_TimesC:
-    "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
-     ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"
+  "(\<lambda>(x, y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
+   ((\<lambda>x. x \<rightarrow> x) ` A) \<times> ((\<lambda>y. y \<times> y) ` B)"
 by (metis image_TimesA)
 
 end