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