src/HOL/Metis_Examples/Trans_Closure.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
blanchet@43197
     1
(*  Title:      HOL/Metis_Examples/Trans_Closure.thy
blanchet@43197
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@41144
     3
    Author:     Jasmin Blanchette, TU Muenchen
paulson@23449
     4
blanchet@43197
     5
Metis example featuring the transitive closure.
paulson@23449
     6
*)
paulson@23449
     7
blanchet@43197
     8
header {* Metis Example Featuring the Transitive Closure *}
blanchet@43197
     9
blanchet@43197
    10
theory Trans_Closure
blanchet@36494
    11
imports Main
paulson@23449
    12
begin
paulson@23449
    13
blanchet@50705
    14
declare [[metis_new_skolem]]
blanchet@42104
    15
blanchet@42104
    16
type_synonym addr = nat
paulson@23449
    17
blanchet@58310
    18
datatype val
paulson@23449
    19
  = Unit        -- "dummy result value of void expressions"
paulson@23449
    20
  | Null        -- "null reference"
paulson@23449
    21
  | Bool bool   -- "Boolean value"
blanchet@42104
    22
  | Intg int    -- "integer value"
paulson@23449
    23
  | Addr addr   -- "addresses of objects in the heap"
paulson@23449
    24
blanchet@36490
    25
consts R :: "(addr \<times> addr) set"
paulson@23449
    26
blanchet@36490
    27
consts f :: "addr \<Rightarrow> val"
paulson@23449
    28
blanchet@36490
    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>
blanchet@36490
    30
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
wenzelm@36501
    31
(* sledgehammer *)
blanchet@36494
    32
proof -
blanchet@36494
    33
  assume A1: "f c = Intg x"
blanchet@36494
    34
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
blanchet@36494
    35
  assume A3: "(a, b) \<in> R\<^sup>*"
blanchet@36494
    36
  assume A4: "(b, c) \<in> R\<^sup>*"
blanchet@36494
    37
  have F1: "f c \<noteq> f b" using A2 A1 by metis
blanchet@36494
    38
  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
blanchet@42104
    39
  have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
blanchet@36494
    40
  have "c \<noteq> b" using F1 by metis
blanchet@36494
    41
  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
blanchet@36494
    42
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
blanchet@36494
    43
qed
paulson@23449
    44
blanchet@36490
    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>
blanchet@36490
    46
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
blanchet@57245
    47
(* sledgehammer [isar_proofs, compress = 2] *)
blanchet@36490
    48
proof -
blanchet@36490
    49
  assume A1: "f c = Intg x"
blanchet@36490
    50
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
blanchet@36490
    51
  assume A3: "(a, b) \<in> R\<^sup>*"
blanchet@36490
    52
  assume A4: "(b, c) \<in> R\<^sup>*"
blanchet@36490
    53
  have "b \<noteq> c" using A1 A2 by metis
wenzelm@53015
    54
  hence "\<exists>x\<^sub>1. (b, x\<^sub>1) \<in> R" using A4 by (metis converse_rtranclE)
haftmann@45970
    55
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
paulson@23449
    56
qed
paulson@23449
    57
blanchet@42104
    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>
blanchet@36490
    59
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
blanchet@36490
    60
apply (erule_tac x = b in converse_rtranclE)
blanchet@36490
    61
 apply metis
blanchet@36490
    62
by (metis transitive_closure_trans(6))
paulson@23449
    63
paulson@23449
    64
end