src/HOL/SizeChange/Examples.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 26875 e18574413bc4
permissions -rw-r--r--
simplified method setup;
krauss@25314
     1
(*  Title:      HOL/Library/SCT_Examples.thy
krauss@25314
     2
    ID:         $Id$
krauss@25314
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@25314
     4
*)
krauss@25314
     5
krauss@25314
     6
header {* Examples for Size-Change Termination *}
krauss@25314
     7
krauss@25314
     8
theory Examples
krauss@25314
     9
imports Size_Change_Termination
krauss@25314
    10
begin
krauss@25314
    11
krauss@25314
    12
function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@25314
    13
where
krauss@25314
    14
  "f n 0 = n"
krauss@25314
    15
| "f 0 (Suc m) = f (Suc m) m"
krauss@25314
    16
| "f (Suc n) (Suc m) = f m n"
krauss@25314
    17
by pat_completeness auto
krauss@25314
    18
krauss@25314
    19
krauss@25314
    20
termination
krauss@25314
    21
  unfolding f_rel_def lfp_const
krauss@25314
    22
  apply (rule SCT_on_relations)
krauss@25314
    23
  apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
krauss@25314
    24
  apply (rule ext, rule ext, simp) (* Show that they are correct *)
krauss@26875
    25
  apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *)
krauss@25314
    26
  apply (rule SCT_Main)                 (* Apply main theorem *)
krauss@25314
    27
  apply (simp add:finite_acg_simps) (* show finiteness *)
berghofe@26822
    28
  oops (*FIXME by eval*) (* Evaluate to true *)
krauss@25314
    29
krauss@25314
    30
function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@25314
    31
where
krauss@25314
    32
  "p m n r = (if r>0 then p m (r - 1) n else
krauss@25314
    33
              if n>0 then p r (n - 1) m 
krauss@25314
    34
                     else m)"
krauss@25314
    35
by pat_completeness auto
krauss@25314
    36
krauss@25314
    37
termination
krauss@25314
    38
  unfolding p_rel_def lfp_const
krauss@25314
    39
  apply (rule SCT_on_relations)
krauss@25314
    40
  apply (tactic "Sct.abs_rel_tac") 
krauss@25314
    41
  apply (rule ext, rule ext, simp) 
krauss@26875
    42
  apply (tactic "Sct.mk_call_graph @{context}")
krauss@25314
    43
  apply (rule SCT_Main)
krauss@25314
    44
  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
berghofe@26822
    45
  oops (* FIXME by eval *)
krauss@25314
    46
krauss@25314
    47
function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@25314
    48
where
krauss@25314
    49
  "foo True (Suc n) m = foo True n (Suc m)"
krauss@25314
    50
| "foo True 0 m = foo False 0 m"
krauss@25314
    51
| "foo False n (Suc m) = foo False (Suc n) m"
krauss@25314
    52
| "foo False n 0 = n"
krauss@25314
    53
by pat_completeness auto
krauss@25314
    54
krauss@25314
    55
termination
krauss@25314
    56
  unfolding foo_rel_def lfp_const
krauss@25314
    57
  apply (rule SCT_on_relations)
krauss@25314
    58
  apply (tactic "Sct.abs_rel_tac") 
krauss@25314
    59
  apply (rule ext, rule ext, simp) 
krauss@26875
    60
  apply (tactic "Sct.mk_call_graph @{context}")
krauss@25314
    61
  apply (rule SCT_Main)
krauss@25314
    62
  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
berghofe@26822
    63
  oops (* FIXME by eval *)
krauss@25314
    64
krauss@25314
    65
krauss@25314
    66
function (sequential) 
krauss@25314
    67
  bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@25314
    68
where
krauss@25314
    69
  "bar 0 (Suc n) m = bar m m m"
krauss@25314
    70
| "bar k n m = 0"
krauss@25314
    71
by pat_completeness auto
krauss@25314
    72
krauss@25314
    73
termination
krauss@25314
    74
  unfolding bar_rel_def lfp_const
krauss@25314
    75
  apply (rule SCT_on_relations)
krauss@25314
    76
  apply (tactic "Sct.abs_rel_tac") 
krauss@25314
    77
  apply (rule ext, rule ext, simp) 
krauss@26875
    78
  apply (tactic "Sct.mk_call_graph @{context}")
krauss@25314
    79
  apply (rule SCT_Main)
krauss@25314
    80
  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
krauss@25314
    81
  by (simp only:sctTest_simps cong: sctTest_congs)
krauss@25314
    82
krauss@25314
    83
end