src/HOL/Metis_Examples/TransClosure.thy
author hoelzl
Tue Mar 23 16:17:41 2010 +0100 (2010-03-23)
changeset 35928 d31f55f97663
parent 35096 f36965a1fd42
child 36490 5abf45444a16
permissions -rw-r--r--
Generate image for HOL-Probability
     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
     8 imports Main
     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 
    20 consts R::"(addr \<times> addr) set"
    21 
    22 consts f:: "addr \<Rightarrow> val"
    23 
    24 declare [[ atp_problem_prefix = "TransClosure__test" ]]
    25 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> 
    26    \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"  
    27 by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
    28 
    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> 
    30    \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
    31 proof (neg_clausify)
    32 assume 0: "f c = Intg x"
    33 assume 1: "(a, b) \<in> R\<^sup>*"
    34 assume 2: "(b, c) \<in> R\<^sup>*"
    35 assume 3: "f b \<noteq> Intg x"
    36 assume 4: "\<And>A. (b, A) \<notin> R \<or> (a, A) \<notin> R\<^sup>*"
    37 have 5: "b = c \<or> b \<in> Domain R"
    38   by (metis Not_Domain_rtrancl 2)
    39 have 6: "\<And>X1. (a, X1) \<in> R\<^sup>* \<or> (b, X1) \<notin> R"
    40   by (metis Transitive_Closure.rtrancl_into_rtrancl 1)
    41 have 7: "\<And>X1. (b, X1) \<notin> R"
    42   by (metis 6 4)
    43 have 8: "b \<notin> Domain R"
    44   by (metis 7 DomainE)
    45 have 9: "c = b"
    46   by (metis 5 8)
    47 have 10: "f b = Intg x"
    48   by (metis 0 9)
    49 show "False"
    50   by (metis 10 3)
    51 qed
    52 
    53 declare [[ atp_problem_prefix = "TransClosure__test_simpler" ]]
    54 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> 
    55    \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
    56 apply (erule_tac x="b" in converse_rtranclE)
    57 apply (metis rel_pow_0_E rel_pow_0_I)
    58 apply (metis DomainE Domain_iff Transitive_Closure.rtrancl_into_rtrancl)
    59 done
    60 
    61 end