src/HOL/Library/SCT_Implementation.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24348 c708ea5b109a
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
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@23416
     6
header {* Implemtation of the SCT criterion *}
wenzelm@22665
     7
krauss@22359
     8
theory SCT_Implementation
haftmann@24423
     9
imports SCT_Definition SCT_Theorem
krauss@22359
    10
begin
krauss@22359
    11
krauss@22359
    12
fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
krauss@22359
    13
where
krauss@22359
    14
  "edges_match ((n, e, m), (n',e',m')) = (m = n')"
krauss@22359
    15
krauss@22359
    16
fun connect_edges :: 
krauss@22359
    17
  "('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n)
krauss@22359
    18
  \<Rightarrow> ('n \<times> 'e \<times> 'n)"
krauss@22359
    19
where
krauss@22359
    20
  "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
krauss@22359
    21
haftmann@22744
    22
lemma grcomp_code [code]:
krauss@22359
    23
  "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
krauss@22359
    24
  by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
krauss@22359
    25
krauss@23416
    26
krauss@23416
    27
lemma mk_tcl_finite_terminates:
krauss@23416
    28
  fixes A :: "'a acg"
krauss@23416
    29
  assumes fA: "finite_acg A" 
krauss@23416
    30
  shows "mk_tcl_dom (A, A)"
krauss@23416
    31
proof -
krauss@23416
    32
  from fA have fin_tcl: "finite_acg (tcl A)"
krauss@23416
    33
    by (simp add:finite_tcl)
krauss@23416
    34
krauss@23416
    35
  hence "finite (dest_graph (tcl A))"
krauss@23416
    36
    unfolding finite_acg_def finite_graph_def ..
krauss@23416
    37
krauss@23416
    38
  let ?count = "\<lambda>G. card (dest_graph G)"
krauss@23416
    39
  let ?N = "?count (tcl A)"
krauss@23416
    40
  let ?m = "\<lambda>X. ?N - (?count X)"
krauss@23416
    41
krauss@23416
    42
  let ?P = "\<lambda>X. mk_tcl_dom (A, X)"
krauss@23416
    43
  
krauss@23416
    44
  {
krauss@23416
    45
    fix X
krauss@23416
    46
    assume "X \<le> tcl A"
krauss@23416
    47
    then
krauss@23416
    48
    have "mk_tcl_dom (A, X)"
krauss@23416
    49
    proof (induct X rule:measure_induct_rule[of ?m])
krauss@23416
    50
      case (less X)
krauss@23416
    51
      show ?case
krauss@23416
    52
      proof (cases "X * A \<le> X")
krauss@23416
    53
        case True 
krauss@23416
    54
        with mk_tcl.domintros show ?thesis by auto
krauss@23416
    55
      next
krauss@23416
    56
        case False
krauss@23416
    57
        then have l: "X < X + X * A"
krauss@23416
    58
          unfolding graph_less_def graph_leq_def graph_plus_def
krauss@23416
    59
          by auto
krauss@23416
    60
krauss@23416
    61
        from `X \<le> tcl A` 
krauss@23416
    62
        have "X * A \<le> tcl A * A" by (simp add:mult_mono)
krauss@23416
    63
        also have "\<dots> \<le> A + tcl A * A" by simp
krauss@23416
    64
        also have "\<dots> = tcl A" by (simp add:tcl_unfold_right[symmetric])
krauss@23416
    65
        finally have "X * A \<le> tcl A" .
krauss@23416
    66
        with `X \<le> tcl A` 
krauss@23416
    67
        have "X + X * A \<le> tcl A + tcl A"
krauss@23416
    68
          by (rule add_mono)
krauss@23416
    69
        hence less_tcl: "X + X * A \<le> tcl A" by simp 
krauss@23416
    70
        hence "X < tcl A"
krauss@23416
    71
          using l `X \<le> tcl A` by auto
krauss@23416
    72
krauss@23416
    73
        from less_tcl fin_tcl
krauss@23416
    74
        have "finite_acg (X + X * A)" by (rule finite_acg_subset)
krauss@23416
    75
        hence "finite (dest_graph (X + X * A))" 
krauss@23416
    76
          unfolding finite_acg_def finite_graph_def ..
krauss@23416
    77
        
krauss@23416
    78
        hence X: "?count X < ?count (X + X * A)"
krauss@23416
    79
          using l[simplified graph_less_def graph_leq_def]
krauss@23416
    80
          by (rule psubset_card_mono)
krauss@23416
    81
        
krauss@23416
    82
        have "?count X < ?N" 
krauss@23416
    83
          apply (rule psubset_card_mono)
krauss@23416
    84
          by fact (rule `X < tcl A`[simplified graph_less_def])
krauss@23416
    85
        
krauss@23416
    86
        with X have "?m (X + X * A) < ?m X" by arith
krauss@23416
    87
        
krauss@23416
    88
        from  less.hyps this less_tcl
krauss@23416
    89
        have "mk_tcl_dom (A, X + X * A)" .
krauss@23416
    90
        with mk_tcl.domintros show ?thesis .
krauss@23416
    91
      qed
krauss@23416
    92
    qed
krauss@23416
    93
  }
krauss@23416
    94
  from this less_tcl show ?thesis .
krauss@23416
    95
qed
krauss@23416
    96
krauss@23416
    97
krauss@23416
    98
lemma mk_tcl_finite_tcl:
krauss@23416
    99
  fixes A :: "'a acg"
krauss@23416
   100
  assumes fA: "finite_acg A"
krauss@23416
   101
  shows "mk_tcl A A = tcl A"
krauss@23416
   102
  using mk_tcl_finite_terminates[OF fA]
krauss@23416
   103
  by (simp only: tcl_def mk_tcl_correctness star_commute)
krauss@23416
   104
krauss@23416
   105
definition test_SCT :: "nat acg \<Rightarrow> bool"
krauss@22359
   106
where
krauss@22359
   107
  "test_SCT \<A> = 
krauss@22359
   108
  (let \<T> = mk_tcl \<A> \<A>
krauss@23416
   109
    in (\<forall>(n,G,m)\<in>dest_graph \<T>. 
krauss@22359
   110
          n \<noteq> m \<or> G * G \<noteq> G \<or> 
krauss@23416
   111
         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
krauss@22359
   112
krauss@22359
   113
krauss@22359
   114
lemma SCT'_exec:
krauss@23416
   115
  assumes fin: "finite_acg A"
krauss@23416
   116
  shows "SCT' A = test_SCT A"
krauss@23416
   117
  using mk_tcl_finite_tcl[OF fin]
krauss@23416
   118
  unfolding test_SCT_def Let_def 
krauss@23416
   119
  unfolding SCT'_def no_bad_graphs_def has_edge_def
krauss@23416
   120
  by force
krauss@22359
   121
krauss@22359
   122
code_modulename SML
krauss@22359
   123
  Implementation Graphs
krauss@22359
   124
krauss@22359
   125
lemma [code func]:
krauss@22359
   126
  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
krauss@22359
   127
  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
krauss@22359
   128
  unfolding graph_leq_def graph_less_def by rule+
krauss@22359
   129
krauss@22359
   130
lemma [code func]:
krauss@22359
   131
  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
krauss@22359
   132
  unfolding graph_plus_def ..
krauss@22359
   133
krauss@22359
   134
lemma [code func]:
krauss@22359
   135
  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
krauss@22359
   136
  unfolding graph_mult_def ..
krauss@22359
   137
krauss@22359
   138
krauss@22359
   139
krauss@22359
   140
lemma SCT'_empty: "SCT' (Graph {})"
krauss@22359
   141
  unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric]
krauss@22359
   142
  tcl_zero
krauss@22359
   143
  by (simp add:in_grzero)
krauss@22359
   144
krauss@22359
   145
krauss@22359
   146
krauss@22359
   147
subsection {* Witness checking *}
krauss@22359
   148
krauss@22359
   149
krauss@23416
   150
definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool"
krauss@22359
   151
where
krauss@22359
   152
  "test_SCT_witness A T = 
krauss@22359
   153
  (A \<le> T \<and> A * T \<le> T \<and>
krauss@22359
   154
       (\<forall>(n,G,m)\<in>dest_graph T. 
krauss@22359
   155
          n \<noteq> m \<or> G * G \<noteq> G \<or> 
krauss@22359
   156
         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
krauss@22359
   157
krauss@22359
   158
krauss@22359
   159
lemma no_bad_graphs_ucl:
krauss@22359
   160
  assumes "A \<le> B"
krauss@22359
   161
  assumes "no_bad_graphs B"
krauss@22359
   162
  shows "no_bad_graphs A"
wenzelm@23394
   163
  using assms
wenzelm@23394
   164
  unfolding no_bad_graphs_def has_edge_def graph_leq_def 
wenzelm@23394
   165
  by blast
krauss@22359
   166
krauss@22359
   167
krauss@22359
   168
krauss@22359
   169
lemma SCT'_witness:
krauss@22359
   170
  assumes a: "test_SCT_witness A T"
krauss@22359
   171
  shows "SCT' A"
krauss@22359
   172
proof -
krauss@22359
   173
  from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def)
krauss@22359
   174
  hence "A + A * T \<le> T" 
krauss@22359
   175
    by (subst add_idem[of T, symmetric], rule add_mono)
krauss@22359
   176
  with star3' have "tcl A \<le> T" unfolding tcl_def .
krauss@22359
   177
  moreover
krauss@22359
   178
  from a have "no_bad_graphs T"
krauss@22359
   179
    unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def
krauss@22359
   180
    by auto
krauss@22359
   181
  ultimately
krauss@22359
   182
  show ?thesis
krauss@22359
   183
    unfolding SCT'_def
krauss@22359
   184
    by (rule no_bad_graphs_ucl)
krauss@22359
   185
qed
krauss@22359
   186
krauss@22359
   187
krauss@22359
   188
code_modulename SML
krauss@22359
   189
  Graphs SCT
krauss@22359
   190
  Kleene_Algebras SCT
krauss@22359
   191
  SCT_Implementation SCT
krauss@22359
   192
haftmann@24348
   193
export_code test_SCT in SML
krauss@22359
   194
krauss@22359
   195
end