src/HOL/Metis_Examples/Trans_Closure.thy
 author blanchet Tue Nov 06 15:15:33 2012 +0100 (2012-11-06) changeset 50020 6b9611abcd4c parent 49918 cf441f4a358b child 50705 0e943b33d907 permissions -rw-r--r--
renamed Sledgehammer option
```     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_proofs, isar_shrink = 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 "b \<noteq> c" using A1 A2 by metis
```
```    54   hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
```
```    55   thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
```
```    56 qed
```
```    57
```
```    58 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>
```
```    59        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
```
```    60 apply (erule_tac x = b in converse_rtranclE)
```
```    61  apply metis
```
```    62 by (metis transitive_closure_trans(6))
```
```    63
```
```    64 end
```