src/HOL/Metis_Examples/Trans_Closure.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45970 b6d0cff57d96
child 49918 cf441f4a358b
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42104
diff changeset
     1
(*  Title:      HOL/Metis_Examples/Trans_Closure.thy
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42104
diff changeset
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
41144
509e51b7509a example tuning
blanchet
parents: 41141
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     4
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42104
diff changeset
     5
Metis example featuring the transitive closure.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     7
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42104
diff changeset
     8
header {* Metis Example Featuring the Transitive Closure *}
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42104
diff changeset
     9
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42104
diff changeset
    10
theory Trans_Closure
36494
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    11
imports Main
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    12
begin
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
42104
22e37d9bc21c made one more Metis example use the new Skolemizer
blanchet
parents: 41144
diff changeset
    14
declare [[metis_new_skolemizer]]
22e37d9bc21c made one more Metis example use the new Skolemizer
blanchet
parents: 41144
diff changeset
    15
22e37d9bc21c made one more Metis example use the new Skolemizer
blanchet
parents: 41144
diff changeset
    16
type_synonym addr = nat
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
datatype val
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    19
  = Unit        -- "dummy result value of void expressions"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
  | Null        -- "null reference"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
  | Bool bool   -- "Boolean value"
42104
22e37d9bc21c made one more Metis example use the new Skolemizer
blanchet
parents: 41144
diff changeset
    22
  | Intg int    -- "integer value"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    23
  | Addr addr   -- "addresses of objects in the heap"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    24
36490
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    25
consts R :: "(addr \<times> addr) set"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    26
36490
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    27
consts f :: "addr \<Rightarrow> val"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    28
36490
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    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>
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    30
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
36501
6c7ba330ab42 disabled spurious invocation of (interactive) sledgehammer;
wenzelm
parents: 36494
diff changeset
    31
(* sledgehammer *)
36494
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    32
proof -
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    33
  assume A1: "f c = Intg x"
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    34
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    35
  assume A3: "(a, b) \<in> R\<^sup>*"
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    36
  assume A4: "(b, c) \<in> R\<^sup>*"
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    37
  have F1: "f c \<noteq> f b" using A2 A1 by metis
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    38
  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
42104
22e37d9bc21c made one more Metis example use the new Skolemizer
blanchet
parents: 41144
diff changeset
    39
  have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
36494
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    40
  have "c \<noteq> b" using F1 by metis
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    41
  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    42
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    43
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    44
36490
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    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>
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    46
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
36925
ffad77bb3046 renamed Sledgehammer options
blanchet
parents: 36501
diff changeset
    47
(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
36490
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    48
proof -
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    49
  assume A1: "f c = Intg x"
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    50
  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    51
  assume A3: "(a, b) \<in> R\<^sup>*"
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    52
  assume A4: "(b, c) \<in> R\<^sup>*"
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    53
  have "b \<noteq> c" using A1 A2 by metis
36494
2478dd225b68 add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
blanchet
parents: 36490
diff changeset
    54
  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43197
diff changeset
    55
  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    56
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    57
42104
22e37d9bc21c made one more Metis example use the new Skolemizer
blanchet
parents: 41144
diff changeset
    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>
36490
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    59
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    60
apply (erule_tac x = b in converse_rtranclE)
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    61
 apply metis
5abf45444a16 redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents: 35096
diff changeset
    62
by (metis transitive_closure_trans(6))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    63
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    64
end