author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45970  b6d0cff57d96 
child 49918  cf441f4a358b 
permissions  rwrr 
43197  1 
(* Title: HOL/Metis_Examples/Trans_Closure.thy 
2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 

41144  3 
Author: Jasmin Blanchette, TU Muenchen 
23449  4 

43197  5 
Metis example featuring the transitive closure. 
23449  6 
*) 
7 

43197  8 
header {* Metis Example Featuring the Transitive Closure *} 
9 

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  12 
begin 
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  17 

18 
datatype val 

19 
= Unit  "dummy result value of void expressions" 

20 
 Null  "null reference" 

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  23 
 Addr addr  "addresses of objects in the heap" 
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  26 

36490
5abf45444a16
redo Sledgehammer proofs (and get rid of "neg_clausify")
blanchet
parents:
35096
diff
changeset

27 
consts f :: "addr \<Rightarrow> val" 
23449  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  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  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  56 
qed 
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  63 

64 
end 