src/HOL/Library/SCT_Implementation.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22845 5f9138bcb3d7
child 23374 a2f492c599e0
permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/SCT_Implementation.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 *)
     5 
     6 header ""
     7 
     8 theory SCT_Implementation
     9 imports ExecutableSet SCT_Definition
    10 begin
    11 
    12 fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
    13 where
    14   "edges_match ((n, e, m), (n',e',m')) = (m = n')"
    15 
    16 fun connect_edges :: 
    17   "('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n)
    18   \<Rightarrow> ('n \<times> 'e \<times> 'n)"
    19 where
    20   "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
    21 
    22 lemma grcomp_code [code]:
    23   "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
    24   by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
    25 
    26 definition test_SCT :: "acg \<Rightarrow> bool"
    27 where
    28   "test_SCT \<A> = 
    29   (let \<T> = mk_tcl \<A> \<A>
    30     in (\<T> \<noteq> 0 \<and>
    31        (\<forall>(n,G,m)\<in>dest_graph \<T>. 
    32           n \<noteq> m \<or> G * G \<noteq> G \<or> 
    33          (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS))))"
    34 
    35 
    36 lemma SCT'_exec:
    37   assumes a: "test_SCT \<A>"
    38   shows "SCT' \<A>"
    39 proof -
    40   from mk_tcl_correctness2 a 
    41   have "mk_tcl \<A> \<A> = tcl \<A>" 
    42     unfolding test_SCT_def Let_def by auto
    43   
    44   with a
    45   show ?thesis
    46     unfolding SCT'_def no_bad_graphs_def test_SCT_def Let_def has_edge_def
    47     by auto
    48 qed
    49 
    50 code_modulename SML
    51   Implementation Graphs
    52 
    53 lemma [code func]:
    54   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
    55   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
    56   unfolding graph_leq_def graph_less_def by rule+
    57 
    58 lemma [code func]:
    59   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
    60   unfolding graph_plus_def ..
    61 
    62 lemma [code func]:
    63   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
    64   unfolding graph_mult_def ..
    65 
    66 
    67 
    68 lemma SCT'_empty: "SCT' (Graph {})"
    69   unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric]
    70   tcl_zero
    71   by (simp add:in_grzero)
    72 
    73 
    74 
    75 subsection {* Witness checking *}
    76 
    77 
    78 definition test_SCT_witness :: "acg \<Rightarrow> acg \<Rightarrow> bool"
    79 where
    80   "test_SCT_witness A T = 
    81   (A \<le> T \<and> A * T \<le> T \<and>
    82        (\<forall>(n,G,m)\<in>dest_graph T. 
    83           n \<noteq> m \<or> G * G \<noteq> G \<or> 
    84          (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
    85 
    86 
    87 lemma no_bad_graphs_ucl:
    88   assumes "A \<le> B"
    89   assumes "no_bad_graphs B"
    90   shows "no_bad_graphs A"
    91 using prems
    92 unfolding no_bad_graphs_def has_edge_def graph_leq_def 
    93 by blast
    94 
    95 
    96 
    97 lemma SCT'_witness:
    98   assumes a: "test_SCT_witness A T"
    99   shows "SCT' A"
   100 proof -
   101   from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def)
   102   hence "A + A * T \<le> T" 
   103     by (subst add_idem[of T, symmetric], rule add_mono)
   104   with star3' have "tcl A \<le> T" unfolding tcl_def .
   105   moreover
   106   from a have "no_bad_graphs T"
   107     unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def
   108     by auto
   109   ultimately
   110   show ?thesis
   111     unfolding SCT'_def
   112     by (rule no_bad_graphs_ucl)
   113 qed
   114 
   115 
   116 code_modulename SML
   117   Graphs SCT
   118   Kleene_Algebras SCT
   119   SCT_Implementation SCT
   120 
   121 code_gen test_SCT in SML
   122 
   123 end