src/HOL/MetisExamples/TransClosure.thy
author boehmes
Sat, 03 Oct 2009 12:05:40 +0200
changeset 32864 a226f29d4bdc
parent 28592 824f8390aaa2
permissions -rw-r--r--
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     1
(*  Title:      HOL/MetisTest/TransClosure.thy
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     2
    ID:         $Id$
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     4
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     5
Testing the metis method
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     7
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     8
theory TransClosure
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     9
imports Main
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    10
begin
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    11
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    12
types addr = nat
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    14
datatype val
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    15
  = Unit        -- "dummy result value of void expressions"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    16
  | Null        -- "null reference"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
  | Bool bool   -- "Boolean value"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
  | Intg int    -- "integer value" 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    19
  | Addr addr   -- "addresses of objects in the heap"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
consts R::"(addr \<times> addr) set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    22
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    23
consts f:: "addr \<Rightarrow> val"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    24
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 28592
diff changeset
    25
declare [[ atp_problem_prefix = "TransClosure__test" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    26
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> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    27
   \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    28
by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    29
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    30
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> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
   \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    32
proof (neg_clausify)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    33
assume 0: "f c = Intg x"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    34
assume 1: "(a, b) \<in> R\<^sup>*"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    35
assume 2: "(b, c) \<in> R\<^sup>*"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    36
assume 3: "f b \<noteq> Intg x"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    37
assume 4: "\<And>A. (b, A) \<notin> R \<or> (a, A) \<notin> R\<^sup>*"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    38
have 5: "b = c \<or> b \<in> Domain R"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    39
  by (metis Not_Domain_rtrancl 2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    40
have 6: "\<And>X1. (a, X1) \<in> R\<^sup>* \<or> (b, X1) \<notin> R"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    41
  by (metis Transitive_Closure.rtrancl_into_rtrancl 1)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    42
have 7: "\<And>X1. (b, X1) \<notin> R"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    43
  by (metis 6 4)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    44
have 8: "b \<notin> Domain R"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    45
  by (metis 7 DomainE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    46
have 9: "c = b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    47
  by (metis 5 8)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    48
have 10: "f b = Intg x"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
  by (metis 0 9)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    50
show "False"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    51
  by (metis 10 3)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    52
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    53
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 28592
diff changeset
    54
declare [[ atp_problem_prefix = "TransClosure__test_simpler" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
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> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    56
   \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    57
apply (erule_tac x="b" in converse_rtranclE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    58
apply (metis rel_pow_0_E rel_pow_0_I)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    59
apply (metis DomainE Domain_iff Transitive_Closure.rtrancl_into_rtrancl)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    60
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    61
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    62
end