src/HOL/SizeChange/Criterion.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 26513 6f306c8c2c54 permissions -rw-r--r--
simplified method setup;
```     1 (*  Title:      HOL/Library/SCT_Definition.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Alexander Krauss, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* The Size-Change Principle (Definition) *}
```
```     7
```
```     8 theory Criterion
```
```     9 imports Graphs Infinite_Set
```
```    10 begin
```
```    11
```
```    12 subsection {* Size-Change Graphs *}
```
```    13
```
```    14 datatype sedge =
```
```    15     LESS ("\<down>")
```
```    16   | LEQ ("\<Down>")
```
```    17
```
```    18 instantiation sedge :: comm_monoid_mult
```
```    19 begin
```
```    20
```
```    21 definition
```
```    22   one_sedge_def: "1 = \<Down>"
```
```    23
```
```    24 definition
```
```    25   mult_sedge_def:" a * b = (if a = \<down> then \<down> else b)"
```
```    26
```
```    27 instance  proof
```
```    28   fix a b c :: sedge
```
```    29   show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
```
```    30   show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
```
```    31   show "a * b = b * a" unfolding mult_sedge_def
```
```    32     by (cases a, simp) (cases b, auto)
```
```    33 qed
```
```    34
```
```    35 end
```
```    36
```
```    37 lemma sedge_UNIV:
```
```    38   "UNIV = { LESS, LEQ }"
```
```    39 proof (intro equalityI subsetI)
```
```    40   fix x show "x \<in> { LESS, LEQ }"
```
```    41     by (cases x) auto
```
```    42 qed auto
```
```    43
```
```    44 instance sedge :: finite
```
```    45 proof
```
```    46   show "finite (UNIV::sedge set)"
```
```    47   by (simp add: sedge_UNIV)
```
```    48 qed
```
```    49
```
```    50
```
```    51
```
```    52 types 'a scg = "('a, sedge) graph"
```
```    53 types 'a acg = "('a, 'a scg) graph"
```
```    54
```
```    55
```
```    56 subsection {* Size-Change Termination *}
```
```    57
```
```    58 abbreviation (input)
```
```    59   "desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))"
```
```    60
```
```    61 abbreviation (input)
```
```    62   "dsc G i j \<equiv> has_edge G i LESS j"
```
```    63
```
```    64 abbreviation (input)
```
```    65   "eqp G i j \<equiv> has_edge G i LEQ j"
```
```    66
```
```    67 abbreviation
```
```    68   eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```    69 ("_ \<turnstile> _ \<leadsto> _")
```
```    70 where
```
```    71   "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
```
```    72
```
```    73
```
```    74 abbreviation (input) descat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
```
```    75 where
```
```    76   "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
```
```    77
```
```    78 abbreviation (input) eqat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
```
```    79 where
```
```    80   "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
```
```    81
```
```    82
```
```    83 abbreviation (input) eqlat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
```
```    84 where
```
```    85   "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
```
```    86                   \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
```
```    87
```
```    88
```
```    89 definition is_desc_thread :: "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
```
```    90 where
```
```    91   "is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))"
```
```    92
```
```    93 definition SCT :: "'a acg \<Rightarrow> bool"
```
```    94 where
```
```    95   "SCT \<A> =
```
```    96   (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
```
```    97
```
```    98
```
```    99
```
```   100 definition no_bad_graphs :: "'a acg \<Rightarrow> bool"
```
```   101 where
```
```   102   "no_bad_graphs A =
```
```   103   (\<forall>n G. has_edge A n G n \<and> G * G = G
```
```   104   \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
```
```   105
```
```   106
```
```   107 definition SCT' :: "'a acg \<Rightarrow> bool"
```
```   108 where
```
```   109   "SCT' A = no_bad_graphs (tcl A)"
```
```   110
```
```   111 end
```