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