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