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
```