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