src/HOL/Metis_Examples/TransClosure.thy
author blanchet
Thu Mar 24 17:49:27 2011 +0100 (2011-03-24)
changeset 42104 22e37d9bc21c
parent 41144 509e51b7509a
permissions -rw-r--r--
made one more Metis example use the new Skolemizer
blanchet@41141
     1
(*  Title:      HOL/Metis_Examples/TransClosure.thy
paulson@23449
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
blanchet@41144
     3
    Author:     Jasmin Blanchette, TU Muenchen
paulson@23449
     4
blanchet@41144
     5
Testing Metis.
paulson@23449
     6
*)
paulson@23449
     7
paulson@23449
     8
theory TransClosure
blanchet@36494
     9
imports Main
paulson@23449
    10
begin
paulson@23449
    11
blanchet@42104
    12
declare [[metis_new_skolemizer]]
blanchet@42104
    13
blanchet@42104
    14
type_synonym addr = nat
paulson@23449
    15
paulson@23449
    16
datatype val
paulson@23449
    17
  = Unit        -- "dummy result value of void expressions"
paulson@23449
    18
  | Null        -- "null reference"
paulson@23449
    19
  | Bool bool   -- "Boolean value"
blanchet@42104
    20
  | Intg int    -- "integer value"
paulson@23449
    21
  | Addr addr   -- "addresses of objects in the heap"
paulson@23449
    22
blanchet@36490
    23
consts R :: "(addr \<times> addr) set"
paulson@23449
    24
blanchet@36490
    25
consts f :: "addr \<Rightarrow> val"
paulson@23449
    26
blanchet@36490
    27
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
    28
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
wenzelm@36501
    29
(* sledgehammer *)
blanchet@36494
    30
proof -
blanchet@36494
    31
  assume A1: "f c = Intg x"
blanchet@36494
    32
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
blanchet@36494
    33
  assume A3: "(a, b) \<in> R\<^sup>*"
blanchet@36494
    34
  assume A4: "(b, c) \<in> R\<^sup>*"
blanchet@36494
    35
  have F1: "f c \<noteq> f b" using A2 A1 by metis
blanchet@36494
    36
  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
blanchet@42104
    37
  have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
blanchet@36494
    38
  have "c \<noteq> b" using F1 by metis
blanchet@36494
    39
  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
blanchet@36494
    40
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
blanchet@36494
    41
qed
paulson@23449
    42
blanchet@36490
    43
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
    44
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
blanchet@36925
    45
(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
blanchet@36490
    46
proof -
blanchet@36490
    47
  assume A1: "f c = Intg x"
blanchet@36490
    48
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
blanchet@36490
    49
  assume A3: "(a, b) \<in> R\<^sup>*"
blanchet@36490
    50
  assume A4: "(b, c) \<in> R\<^sup>*"
blanchet@36490
    51
  have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
blanchet@36490
    52
  hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
blanchet@36490
    53
  have "b \<noteq> c" using A1 A2 by metis
blanchet@36494
    54
  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
blanchet@36490
    55
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 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