src/HOL/SizeChange/Implementation.thy
 author haftmann Fri Jan 02 08:12:46 2009 +0100 (2009-01-02) changeset 29332 edc1e2a56398 parent 28562 4e74209f113e child 31979 09f65e860bdb permissions -rw-r--r--
named code theorem for Fract_norm
```     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 Implementation
```
```     9 imports Correctness
```
```    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]:
```
```   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]:
```
```   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]:
```
```   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 definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool"
```
```   150 where
```
```   151   "test_SCT_witness A T =
```
```   152   (A \<le> T \<and> A * T \<le> T \<and>
```
```   153        (\<forall>(n,G,m)\<in>dest_graph T.
```
```   154           n \<noteq> m \<or> G * G \<noteq> G \<or>
```
```   155          (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
```
```   156
```
```   157 lemma no_bad_graphs_ucl:
```
```   158   assumes "A \<le> B"
```
```   159   assumes "no_bad_graphs B"
```
```   160   shows "no_bad_graphs A"
```
```   161   using assms
```
```   162   unfolding no_bad_graphs_def has_edge_def graph_leq_def
```
```   163   by blast
```
```   164
```
```   165 lemma SCT'_witness:
```
```   166   assumes a: "test_SCT_witness A T"
```
```   167   shows "SCT' A"
```
```   168 proof -
```
```   169   from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def)
```
```   170   hence "A + A * T \<le> T"
```
```   171     by (subst add_idem[of T, symmetric], rule add_mono)
```
```   172   with star3' have "tcl A \<le> T" unfolding tcl_def .
```
```   173   moreover
```
```   174   from a have "no_bad_graphs T"
```
```   175     unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def
```
```   176     by auto
```
```   177   ultimately
```
```   178   show ?thesis
```
```   179     unfolding SCT'_def
```
```   180     by (rule no_bad_graphs_ucl)
```
```   181 qed
```
```   182
```
```   183 (* ML {* @{code test_SCT} *} *)
```
```   184
```
```   185 end
```