src/HOL/Metis_Examples/Trans_Closure.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43197 c71657bbdbc0
child 45970 b6d0cff57d96
permissions -rw-r--r--
remove lemma stupid_ext
     1 (*  Title:      HOL/Metis_Examples/Trans_Closure.thy
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Metis example featuring the transitive closure.
     6 *)
     7 
     8 header {* Metis Example Featuring the Transitive Closure *}
     9 
    10 theory Trans_Closure
    11 imports Main
    12 begin
    13 
    14 declare [[metis_new_skolemizer]]
    15 
    16 type_synonym addr = nat
    17 
    18 datatype val
    19   = Unit        -- "dummy result value of void expressions"
    20   | Null        -- "null reference"
    21   | Bool bool   -- "Boolean value"
    22   | Intg int    -- "integer value"
    23   | Addr addr   -- "addresses of objects in the heap"
    24 
    25 consts R :: "(addr \<times> addr) set"
    26 
    27 consts f :: "addr \<Rightarrow> val"
    28 
    29 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>
    30        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
    31 (* sledgehammer *)
    32 proof -
    33   assume A1: "f c = Intg x"
    34   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
    35   assume A3: "(a, b) \<in> R\<^sup>*"
    36   assume A4: "(b, c) \<in> R\<^sup>*"
    37   have F1: "f c \<noteq> f b" using A2 A1 by metis
    38   have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
    39   have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
    40   have "c \<noteq> b" using F1 by metis
    41   hence "\<exists>u. (b, u) \<in> R" using F3 by metis
    42   thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
    43 qed
    44 
    45 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>
    46        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
    47 (* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
    48 proof -
    49   assume A1: "f c = Intg x"
    50   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
    51   assume A3: "(a, b) \<in> R\<^sup>*"
    52   assume A4: "(b, c) \<in> R\<^sup>*"
    53   have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
    54   hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
    55   have "b \<noteq> c" using A1 A2 by metis
    56   hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
    57   thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
    58 qed
    59 
    60 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>
    61        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
    62 apply (erule_tac x = b in converse_rtranclE)
    63  apply metis
    64 by (metis transitive_closure_trans(6))
    65 
    66 end