src/HOL/Metis_Examples/TransClosure.thy
author wenzelm
Wed Apr 28 19:43:45 2010 +0200 (2010-04-28)
changeset 36501 6c7ba330ab42
parent 36494 2478dd225b68
child 36925 ffad77bb3046
permissions -rw-r--r--
disabled spurious invocation of (interactive) sledgehammer;
paulson@23449
     1
(*  Title:      HOL/MetisTest/TransClosure.thy
paulson@23449
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@23449
     3
paulson@23449
     4
Testing the metis method
paulson@23449
     5
*)
paulson@23449
     6
paulson@23449
     7
theory TransClosure
blanchet@36494
     8
imports Main
paulson@23449
     9
begin
paulson@23449
    10
paulson@23449
    11
types addr = nat
paulson@23449
    12
paulson@23449
    13
datatype val
paulson@23449
    14
  = Unit        -- "dummy result value of void expressions"
paulson@23449
    15
  | Null        -- "null reference"
paulson@23449
    16
  | Bool bool   -- "Boolean value"
paulson@23449
    17
  | Intg int    -- "integer value" 
paulson@23449
    18
  | Addr addr   -- "addresses of objects in the heap"
paulson@23449
    19
blanchet@36490
    20
consts R :: "(addr \<times> addr) set"
paulson@23449
    21
blanchet@36490
    22
consts f :: "addr \<Rightarrow> val"
paulson@23449
    23
blanchet@36490
    24
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
    25
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
wenzelm@36501
    26
(* sledgehammer *)
blanchet@36494
    27
proof -
blanchet@36494
    28
  assume A1: "f c = Intg x"
blanchet@36494
    29
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
blanchet@36494
    30
  assume A3: "(a, b) \<in> R\<^sup>*"
blanchet@36494
    31
  assume A4: "(b, c) \<in> R\<^sup>*"
blanchet@36494
    32
  have F1: "f c \<noteq> f b" using A2 A1 by metis
blanchet@36494
    33
  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
blanchet@36494
    34
  have F3: "\<exists>x. (b, x R b c) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
blanchet@36494
    35
  have "c \<noteq> b" using F1 by metis
blanchet@36494
    36
  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
blanchet@36494
    37
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
blanchet@36494
    38
qed
paulson@23449
    39
blanchet@36490
    40
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
    41
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
blanchet@36490
    42
(* sledgehammer [isar_proof, shrink_factor = 2] *)
blanchet@36490
    43
proof -
blanchet@36490
    44
  assume A1: "f c = Intg x"
blanchet@36490
    45
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
blanchet@36490
    46
  assume A3: "(a, b) \<in> R\<^sup>*"
blanchet@36490
    47
  assume A4: "(b, c) \<in> R\<^sup>*"
blanchet@36490
    48
  have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
blanchet@36490
    49
  hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
blanchet@36490
    50
  have "b \<noteq> c" using A1 A2 by metis
blanchet@36494
    51
  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
blanchet@36490
    52
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
paulson@23449
    53
qed
paulson@23449
    54
blanchet@36490
    55
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
    56
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
blanchet@36490
    57
apply (erule_tac x = b in converse_rtranclE)
blanchet@36490
    58
 apply metis
blanchet@36490
    59
by (metis transitive_closure_trans(6))
paulson@23449
    60
paulson@23449
    61
end