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