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