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