src/HOL/SizeChange/Criterion.thy
author krauss
Tue Nov 06 17:44:53 2007 +0100 (2007-11-06)
changeset 25314 5eaf3e8b50a4
child 25764 878c37886eed
permissions -rw-r--r--
moved stuff about size change termination to its own session
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
krauss@25314
    18
instance sedge :: one
krauss@25314
    19
  one_sedge_def: "1 \<equiv> \<Down>" ..
krauss@25314
    20
krauss@25314
    21
instance sedge :: times
krauss@25314
    22
  mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" ..
krauss@25314
    23
krauss@25314
    24
instance sedge :: comm_monoid_mult
krauss@25314
    25
proof
krauss@25314
    26
  fix a b c :: sedge
krauss@25314
    27
  show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
krauss@25314
    28
  show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
krauss@25314
    29
  show "a * b = b * a" unfolding mult_sedge_def
krauss@25314
    30
    by (cases a, simp) (cases b, auto)
krauss@25314
    31
qed
krauss@25314
    32
krauss@25314
    33
lemma sedge_UNIV:
krauss@25314
    34
  "UNIV = { LESS, LEQ }"
krauss@25314
    35
proof (intro equalityI subsetI)
krauss@25314
    36
  fix x show "x \<in> { LESS, LEQ }"
krauss@25314
    37
    by (cases x) auto
krauss@25314
    38
qed auto
krauss@25314
    39
krauss@25314
    40
instance sedge :: finite
krauss@25314
    41
proof
krauss@25314
    42
  show "finite (UNIV::sedge set)"
krauss@25314
    43
    by (simp add: sedge_UNIV)
krauss@25314
    44
qed
krauss@25314
    45
krauss@25314
    46
lemmas [code func] = sedge_UNIV
krauss@25314
    47
krauss@25314
    48
krauss@25314
    49
types 'a scg = "('a, sedge) graph"
krauss@25314
    50
types 'a acg = "('a, 'a scg) graph"
krauss@25314
    51
krauss@25314
    52
krauss@25314
    53
subsection {* Size-Change Termination *}
krauss@25314
    54
krauss@25314
    55
abbreviation (input)
krauss@25314
    56
  "desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))"
krauss@25314
    57
krauss@25314
    58
abbreviation (input)
krauss@25314
    59
  "dsc G i j \<equiv> has_edge G i LESS j"
krauss@25314
    60
krauss@25314
    61
abbreviation (input)
krauss@25314
    62
  "eq G i j \<equiv> has_edge G i LEQ j"
krauss@25314
    63
krauss@25314
    64
abbreviation
krauss@25314
    65
  eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
krauss@25314
    66
("_ \<turnstile> _ \<leadsto> _")
krauss@25314
    67
where
krauss@25314
    68
  "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
krauss@25314
    69
krauss@25314
    70
krauss@25314
    71
abbreviation (input) descat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
krauss@25314
    72
where
krauss@25314
    73
  "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
krauss@25314
    74
krauss@25314
    75
abbreviation (input) eqat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
krauss@25314
    76
where
krauss@25314
    77
  "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
krauss@25314
    78
krauss@25314
    79
krauss@25314
    80
abbreviation (input) eqlat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
krauss@25314
    81
where
krauss@25314
    82
  "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
krauss@25314
    83
                  \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
krauss@25314
    84
krauss@25314
    85
krauss@25314
    86
definition is_desc_thread :: "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
krauss@25314
    87
where
krauss@25314
    88
  "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
    89
krauss@25314
    90
definition SCT :: "'a acg \<Rightarrow> bool"
krauss@25314
    91
where
krauss@25314
    92
  "SCT \<A> = 
krauss@25314
    93
  (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
krauss@25314
    94
krauss@25314
    95
krauss@25314
    96
krauss@25314
    97
definition no_bad_graphs :: "'a acg \<Rightarrow> bool"
krauss@25314
    98
where
krauss@25314
    99
  "no_bad_graphs A = 
krauss@25314
   100
  (\<forall>n G. has_edge A n G n \<and> G * G = G
krauss@25314
   101
  \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
krauss@25314
   102
krauss@25314
   103
krauss@25314
   104
definition SCT' :: "'a acg \<Rightarrow> bool"
krauss@25314
   105
where
krauss@25314
   106
  "SCT' A = no_bad_graphs (tcl A)"
krauss@25314
   107
krauss@25314
   108
end