add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
--- a/src/HOL/Metis_Examples/TransClosure.thy Wed Apr 28 16:03:49 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy Wed Apr 28 16:05:38 2010 +0200
@@ -5,7 +5,7 @@
*)
theory TransClosure
-imports Sledgehammer2d (* ### *)
+imports Main
begin
types addr = nat
@@ -23,7 +23,19 @@
lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
\<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-by (metis converse_rtranclE transitive_closure_trans(6))
+sledgehammer
+proof -
+ assume A1: "f c = Intg x"
+ assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
+ assume A3: "(a, b) \<in> R\<^sup>*"
+ assume A4: "(b, c) \<in> R\<^sup>*"
+ have F1: "f c \<noteq> f b" using A2 A1 by metis
+ have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
+ have F3: "\<exists>x. (b, x R b c) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
+ have "c \<noteq> b" using F1 by metis
+ hence "\<exists>u. (b, u) \<in> R" using F3 by metis
+ thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
+qed
lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
\<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
@@ -36,7 +48,7 @@
have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
have "b \<noteq> c" using A1 A2 by metis
- hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis mem_def converse_rtranclE)
+ hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
qed