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