# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID 22e37d9bc21c4b78d1db503752908a9559c1d221
# Parent  6066a35f66784ef9adfec339156d1f4066ff3a4a
made one more Metis example use the new Skolemizer

diff -r 6066a35f6678 -r 22e37d9bc21c src/HOL/Metis_Examples/TransClosure.thy
--- a/src/HOL/Metis_Examples/TransClosure.thy	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/TransClosure.thy	Thu Mar 24 17:49:27 2011 +0100
@@ -9,13 +9,15 @@
 imports Main
 begin
 
-types addr = nat
+declare [[metis_new_skolemizer]]
+
+type_synonym addr = nat
 
 datatype val
   = Unit        -- "dummy result value of void expressions"
   | Null        -- "null reference"
   | Bool bool   -- "Boolean value"
-  | Intg int    -- "integer value" 
+  | Intg int    -- "integer value"
   | Addr addr   -- "addresses of objects in the heap"
 
 consts R :: "(addr \<times> addr) set"
@@ -32,7 +34,7 @@
   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 F3: "\<exists>x. (b, x b c R) \<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
@@ -53,7 +55,7 @@
   thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
 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> 
+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>*"
 apply (erule_tac x = b in converse_rtranclE)
  apply metis