src/HOL/MetisExamples/TransClosure.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 28592 824f8390aaa2
child 32864 a226f29d4bdc
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/MetisTest/TransClosure.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 
     5 Testing the metis method
     6 *)
     7 
     8 theory TransClosure
     9 imports Main
    10 begin
    11 
    12 types addr = nat
    13 
    14 datatype val
    15   = Unit        -- "dummy result value of void expressions"
    16   | Null        -- "null reference"
    17   | Bool bool   -- "Boolean value"
    18   | Intg int    -- "integer value" 
    19   | Addr addr   -- "addresses of objects in the heap"
    20 
    21 consts R::"(addr \<times> addr) set"
    22 
    23 consts f:: "addr \<Rightarrow> val"
    24 
    25 ML {*AtpWrapper.problem_name := "TransClosure__test"*}
    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> 
    27    \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"  
    28 by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
    29 
    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> 
    31    \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
    32 proof (neg_clausify)
    33 assume 0: "f c = Intg x"
    34 assume 1: "(a, b) \<in> R\<^sup>*"
    35 assume 2: "(b, c) \<in> R\<^sup>*"
    36 assume 3: "f b \<noteq> Intg x"
    37 assume 4: "\<And>A. (b, A) \<notin> R \<or> (a, A) \<notin> R\<^sup>*"
    38 have 5: "b = c \<or> b \<in> Domain R"
    39   by (metis Not_Domain_rtrancl 2)
    40 have 6: "\<And>X1. (a, X1) \<in> R\<^sup>* \<or> (b, X1) \<notin> R"
    41   by (metis Transitive_Closure.rtrancl_into_rtrancl 1)
    42 have 7: "\<And>X1. (b, X1) \<notin> R"
    43   by (metis 6 4)
    44 have 8: "b \<notin> Domain R"
    45   by (metis 7 DomainE)
    46 have 9: "c = b"
    47   by (metis 5 8)
    48 have 10: "f b = Intg x"
    49   by (metis 0 9)
    50 show "False"
    51   by (metis 10 3)
    52 qed
    53 
    54 ML {*AtpWrapper.problem_name := "TransClosure__test_simpler"*}
    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> 
    56    \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
    57 apply (erule_tac x="b" in converse_rtranclE)
    58 apply (metis rel_pow_0_E rel_pow_0_I)
    59 apply (metis DomainE Domain_iff Transitive_Closure.rtrancl_into_rtrancl)
    60 done
    61 
    62 end