src/HOL/Library/SCT_Examples.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22665 cf152ff55d16
child 23374 a2f492c599e0
permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/SCT_Examples.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 *)
     5 
     6 header ""
     7 
     8 theory SCT_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") (* Build control graph *)
    26   apply (rule LJA_apply)                 (* Apply main theorem *)
    27   apply (simp add:finite_acg_ins finite_acg_empty) (* show finiteness *)
    28   apply (rule SCT'_exec)
    29   by eval (* Evaluate to true *)
    30 
    31 function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    32 where
    33   "p m n r = (if r>0 then p m (r - 1) n else
    34               if n>0 then p r (n - 1) m 
    35                      else m)"
    36 by pat_completeness auto
    37 
    38 termination
    39   unfolding p_rel_def lfp_const
    40   apply (rule SCT_on_relations)
    41   apply (tactic "Sct.abs_rel_tac") 
    42   apply (rule ext, rule ext, simp) 
    43   apply (tactic "Sct.mk_call_graph")
    44   apply (rule LJA_apply)            
    45   apply (simp add:finite_acg_ins finite_acg_empty) 
    46   apply (rule SCT'_exec)
    47   by eval
    48 
    49 function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    50 where
    51   "foo True (Suc n) m = foo True n (Suc m)"
    52 | "foo True 0 m = foo False 0 m"
    53 | "foo False n (Suc m) = foo False (Suc n) m"
    54 | "foo False n 0 = n"
    55 by pat_completeness auto
    56 
    57 termination
    58   unfolding foo_rel_def lfp_const
    59   apply (rule SCT_on_relations)
    60   apply (tactic "Sct.abs_rel_tac") 
    61   apply (rule ext, rule ext, simp) 
    62   apply (tactic "Sct.mk_call_graph")
    63   apply (rule LJA_apply)            
    64   apply (simp add:finite_acg_ins finite_acg_empty) 
    65   apply (rule SCT'_exec)
    66   by eval
    67 
    68 function (sequential) 
    69   bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    70 where
    71   "bar 0 (Suc n) m = bar m m m"
    72 | "bar k n m = 0"
    73 by pat_completeness auto
    74 
    75 termination
    76   unfolding bar_rel_def lfp_const
    77   apply (rule SCT_on_relations)
    78   apply (tactic "Sct.abs_rel_tac") 
    79   apply (rule ext, rule ext, simp) 
    80   apply (tactic "Sct.mk_call_graph")
    81   apply (rule LJA_apply)            
    82   apply (simp add:finite_acg_ins finite_acg_empty) 
    83   by (rule SCT'_empty)
    84 
    85 end