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