thys2/Recs.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 25 May 2013 11:46:25 +0100
changeset 265 fa3c214559b0
parent 263 aa102c182132
child 266 b1b47d28c295
permissions -rwxr-xr-x
finished recusive version of the UF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
theory Recs
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
     2
imports Main Fact 
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
     3
        "~~/src/HOL/Number_Theory/Primes" 
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
     4
        "~~/src/HOL/Library/Nat_Bijection"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
     5
        "~~/src/HOL/Library/Discrete"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
begin
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
     8
declare One_nat_def[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
     9
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    10
(*
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    11
  some definitions from 
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    12
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    13
    A Course in Formal Languages, Automata and Groups
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    14
    I M Chiswell 
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    15
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    16
  and
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    17
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    18
    Lecture on undecidability
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    19
    Michael M. Wolf 
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    20
*)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
    21
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
lemma if_zero_one [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
  "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
  "(0::nat) < (if P then 1 else 0) = P"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    25
  "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
by (simp_all)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
lemma nth:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
  "(x # xs) ! 0 = x"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
  "(x # y # xs) ! 1 = y"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
  "(x # y # z # xs) ! 2 = z"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
  "(x # y # z # u # xs) ! 3 = u"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
by (simp_all)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    35
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    36
section {* Some auxiliary lemmas about @{text "\<Sum>"} and @{text "\<Prod>"} *}
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    37
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    38
lemma setprod_atMost_Suc[simp]: 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    39
  "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
by(simp add:atMost_Suc mult_ac)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    42
lemma setprod_lessThan_Suc[simp]: 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    43
  "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
by (simp add:lessThan_Suc mult_ac)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
  setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
apply(subst setsum_Un_disjoint[symmetric])
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
apply(auto simp add: ivl_disj_un_one)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
done
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
lemma setsum_eq_zero [simp]:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    53
  fixes f::"nat \<Rightarrow> nat"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    54
  shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    55
        "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
by (auto)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
lemma setprod_eq_zero [simp]:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    59
  fixes f::"nat \<Rightarrow> nat"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    60
  shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    61
        "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
by (auto)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
lemma setsum_one_less:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
  fixes n::nat
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
  assumes "\<forall>i < n. f i \<le> 1" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
  shows "(\<Sum>i < n. f i) \<le> n"  
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
using assms
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
by (induct n) (auto)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
241
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    71
lemma setsum_one_le:
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    72
  fixes n::nat
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    73
  assumes "\<forall>i \<le> n. f i \<le> 1" 
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    74
  shows "(\<Sum>i \<le> n. f i) \<le> Suc n"  
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    75
using assms
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    76
by (induct n) (auto)
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    77
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    78
lemma setsum_eq_one_le:
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    79
  fixes n::nat
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    80
  assumes "\<forall>i \<le> n. f i = 1" 
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    81
  shows "(\<Sum>i \<le> n. f i) = Suc n"  
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    82
using assms
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    83
by (induct n) (auto)
e59e549e6ab6 uodated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 240
diff changeset
    84
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
lemma setsum_least_eq:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
    86
  fixes f::"nat \<Rightarrow> nat"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
  assumes h0: "p \<le> n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
  assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
  assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
  shows "(\<Sum>i \<le> n. f i) = p"  
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
proof -
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
  have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
    using h1 by (induct p) (simp_all)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
  have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
    using h2 by auto
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
    using h0 by (simp add: setsum_add_nat_ivl2) 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
  also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
  finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
qed
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   102
lemma nat_mult_le_one:
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   103
  fixes m n::nat
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   104
  assumes "m \<le> 1" "n \<le> 1"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   105
  shows "m * n \<le> 1"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   106
using assms by (induct n) (auto)
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   107
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
lemma setprod_one_le:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   109
  fixes f::"nat \<Rightarrow> nat"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   110
  assumes "\<forall>i \<le> n. f i \<le> 1" 
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
  shows "(\<Prod>i \<le> n. f i) \<le> 1" 
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   112
using assms 
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   113
by (induct n) (auto intro: nat_mult_le_one)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
lemma setprod_greater_zero:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   116
  fixes f::"nat \<Rightarrow> nat"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   117
  assumes "\<forall>i \<le> n. f i \<ge> 0" 
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
  shows "(\<Prod>i \<le> n. f i) \<ge> 0" 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   119
using assms by (induct n) (auto)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
lemma setprod_eq_one:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   122
  fixes f::"nat \<Rightarrow> nat"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
  assumes "\<forall>i \<le> n. f i = Suc 0" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
  shows "(\<Prod>i \<le> n. f i) = Suc 0" 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   125
using assms by (induct n) (auto)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
lemma setsum_cut_off_less:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   128
  fixes f::"nat \<Rightarrow> nat"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
  assumes h1: "m \<le> n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
  and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
  shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
proof -
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
  have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
    using h2 by auto
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   135
  have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
    using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
  finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
qed
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
lemma setsum_cut_off_le:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   142
  fixes f::"nat \<Rightarrow> nat"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   143
  assumes h1: "m \<le> n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
  and     h2: "\<forall>i \<in> {m..n}. f i = 0"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
  shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
proof -
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
  have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
    using h2 by auto
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   150
    using h1 by (simp add: setsum_add_nat_ivl2)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   151
  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   152
  finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   153
qed
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   154
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   155
lemma setprod_one [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   156
  fixes n::nat
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   157
  shows "(\<Prod>i < n. Suc 0) = Suc 0"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   158
        "(\<Prod>i \<le> n. Suc 0) = Suc 0"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   159
by (induct n) (simp_all)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   160
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   161
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   162
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   163
section {* Recursive Functions *}
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   164
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   165
datatype recf =  Z
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   166
              |  S
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   167
              |  Id nat nat
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   168
              |  Cn nat recf "recf list"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
              |  Pr nat recf recf
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   170
              |  Mn nat recf 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   171
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   172
fun arity :: "recf \<Rightarrow> nat"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   173
  where
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   174
  "arity Z = 1" 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   175
| "arity S = 1"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   176
| "arity (Id m n) = m"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   177
| "arity (Cn n f gs) = n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
| "arity (Pr n f g) = Suc n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
| "arity (Mn n f) = n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
abbreviation
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
  "CN f gs \<equiv> Cn (arity (hd gs)) f gs"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   183
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
abbreviation
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
  "PR f g \<equiv> Pr (arity f) f g"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   186
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   187
abbreviation
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   188
  "MN f \<equiv> Mn (arity f - 1) f"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   189
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   190
fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
  where
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   192
  "rec_eval Z xs = 0" 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   193
| "rec_eval S xs = Suc (xs ! 0)" 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   194
| "rec_eval (Id m n) xs = xs ! n" 
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
| "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
| "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
| "rec_eval (Pr n f g) (Suc x # xs) = 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   198
     rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   199
| "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   200
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   201
inductive 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   202
  terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   203
where
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   204
  termi_z: "terminates Z [n]"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   205
| termi_s: "terminates S [n]"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   206
| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (Id m n) xs"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   207
| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   208
              \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   209
| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   210
              terminates f xs;
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   211
              length xs = n\<rbrakk> 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   212
              \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   213
| termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   214
              rec_eval f (r # xs) = 0;
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   215
              \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   216
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   217
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   218
section {* Recursive Function Definitions *}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   220
text {*
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   221
  @{text "constn n"} is the recursive function which computes 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
  natural number @{text "n"}.
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
*}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   224
fun constn :: "nat \<Rightarrow> recf"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   225
  where
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   226
  "constn 0 = Z"  |
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   227
  "constn (Suc n) = CN S [constn n]"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   229
definition
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   230
  "rec_swap f = CN f [Id 2 1, Id 2 0]"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   232
definition
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   233
  "rec_add = PR (Id 1 0) (CN S [Id 3 1])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   236
  "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
definition 
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   239
  "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
definition
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   242
  "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   243
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   245
  "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   246
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
definition 
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   248
  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   249
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   250
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   251
text {* 
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   252
  The @{text "sign"} function returns 1 when the input argument 
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   253
  is greater than @{text "0"}. *}
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   255
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   256
  "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   257
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   258
definition 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   259
  "rec_not = CN rec_minus [constn 1, Id 1 0]"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   260
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   261
text {*
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   262
  @{text "rec_eq"} compares two arguments: returns @{text "1"}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   263
  if they are equal; @{text "0"} otherwise. *}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   264
definition 
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   265
  "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   266
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   267
definition 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   268
  "rec_noteq = CN rec_not [rec_eq]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   269
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   270
definition 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   271
  "rec_conj = CN rec_sign [rec_mult]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   272
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   273
definition 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   274
  "rec_disj = CN rec_sign [rec_add]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   275
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   276
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   277
  "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   278
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   279
text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   280
  y otherwise;  @{term "rec_if [z, x, y]"} returns x if z is *not*
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   281
  zero, y otherwise *}
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   282
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   283
definition 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   284
  "rec_ifz = PR (Id 2 0) (Id 4 3)"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   285
245
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   286
definition 
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   287
  "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   288
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   289
text {*
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   290
  @{text "rec_less"} compares two arguments and returns @{text "1"} if
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   291
  the first is less than the second; otherwise returns @{text "0"}. *}
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   292
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   293
definition 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   294
  "rec_less = CN rec_sign [rec_swap rec_minus]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   295
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   296
definition 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   297
  "rec_le = CN rec_disj [rec_less, rec_eq]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   298
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   299
text {* Sigma and Accum for function with one and two arguments *}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   300
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   301
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   302
  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   303
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   304
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   305
  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   306
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   307
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   308
  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   309
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   310
definition 
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   311
  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   312
265
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   313
definition 
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   314
  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   315
                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   316
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   317
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   318
text {* Bounded quantifiers for one and two arguments *}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   319
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   320
definition
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   321
  "rec_all1 f = CN rec_sign [rec_accum1 f]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   322
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   323
definition
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   324
  "rec_all2 f = CN rec_sign [rec_accum2 f]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   325
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   326
definition
265
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   327
  "rec_all3 f = CN rec_sign [rec_accum3 f]"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   328
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   329
definition
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   330
  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   331
                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   332
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   333
definition
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   334
  "rec_all2_less f = (let f' = CN rec_disj [CN rec_eq [Id 4 0, Id 4 1], CN f [Id 4 0, Id 4 2, Id 4 3]] 
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   335
                      in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   336
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   337
definition
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   338
  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   339
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   340
definition
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   341
  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   342
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   343
text {* Dvd, Quotient, Modulo *}
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   344
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   345
(* FIXME: probably all not needed *)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   346
definition 
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   347
  "rec_dvd = 
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   348
     rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"  
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   349
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   350
definition
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   351
  "rec_quo = (let lhs = CN S [Id 3 0] in
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   352
              let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
245
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   353
              let cond = CN rec_eq [lhs, rhs] in
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   354
              let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   355
              in PR Z if_stmt)"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   356
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   357
definition
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   358
  "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   359
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   360
text {* Iteration *}
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   361
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   362
definition
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   363
   "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   364
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   365
fun Iter where
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   366
  "Iter f 0 = id"
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   367
| "Iter f (Suc n) = f \<circ> (Iter f n)"
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   368
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   369
lemma Iter_comm:
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   370
  "(Iter f n) (f x) = f ((Iter f n) x)"
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   371
by (induct n) (simp_all)
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   372
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   373
lemma iter_lemma [simp]:
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   374
  "rec_eval (rec_iter f) [n, x] =  Iter (\<lambda>x. rec_eval f [x]) n x"
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   375
by (induct n) (simp_all add: rec_iter_def)
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   376
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   377
section {* Correctness of Recursive Functions *}
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   378
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   379
lemma constn_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   380
  "rec_eval (constn n) xs = n"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   381
by (induct n) (simp_all)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   382
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   383
lemma swap_lemma [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   384
  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   385
by (simp add: rec_swap_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   386
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   387
lemma add_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   388
  "rec_eval rec_add [x, y] =  x + y"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   389
by (induct x) (simp_all add: rec_add_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   390
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   391
lemma mult_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   392
  "rec_eval rec_mult [x, y] = x * y"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   393
by (induct x) (simp_all add: rec_mult_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   394
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   395
lemma power_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   396
  "rec_eval rec_power [x, y] = x ^ y"
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   397
by (induct y) (simp_all add: rec_power_def)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   398
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   399
lemma fact_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   400
  "rec_eval rec_fact [x] = fact x"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   401
by (induct x) (simp_all add: rec_fact_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   402
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   403
lemma pred_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   404
  "rec_eval rec_pred [x] =  x - 1"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   405
by (induct x) (simp_all add: rec_pred_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   406
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   407
lemma minus_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   408
  "rec_eval rec_minus [x, y] = x - y"
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   409
by (induct y) (simp_all add: rec_minus_def)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   410
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   411
lemma sign_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   412
  "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   413
by (simp add: rec_sign_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   414
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   415
lemma not_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   416
  "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   417
by (simp add: rec_not_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   418
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   419
lemma eq_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   420
  "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   421
by (simp add: rec_eq_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   422
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   423
lemma noteq_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   424
  "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   425
by (simp add: rec_noteq_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   426
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   427
lemma conj_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   428
  "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   429
by (simp add: rec_conj_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   430
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   431
lemma disj_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   432
  "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   433
by (simp add: rec_disj_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   434
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   435
lemma imp_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   436
  "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   437
by (simp add: rec_imp_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   438
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   439
lemma less_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   440
  "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   441
by (simp add: rec_less_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   442
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   443
lemma le_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   444
  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   445
by(simp add: rec_le_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   446
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   447
lemma ifz_lemma [simp]:
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   448
  "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   449
by (case_tac z) (simp_all add: rec_ifz_def)
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   450
245
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   451
lemma if_lemma [simp]:
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   452
  "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   453
by (simp add: rec_if_def)
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   454
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   455
lemma sigma1_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   456
  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   457
by (induct x) (simp_all add: rec_sigma1_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   458
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   459
lemma sigma2_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   460
  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   461
by (induct x) (simp_all add: rec_sigma2_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   462
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   463
lemma accum1_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   464
  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   465
by (induct x) (simp_all add: rec_accum1_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   466
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   467
lemma accum2_lemma [simp]: 
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   468
  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   469
by (induct x) (simp_all add: rec_accum2_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   470
265
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   471
lemma accum3_lemma [simp]: 
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   472
  shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   473
by (induct x) (simp_all add: rec_accum3_def)
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   474
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   475
lemma ex1_lemma [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   476
 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   477
by (simp add: rec_ex1_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   478
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   479
lemma ex2_lemma [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   480
 "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   481
by (simp add: rec_ex2_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   482
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   483
lemma all1_lemma [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   484
 "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   485
by (simp add: rec_all1_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   486
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   487
lemma all2_lemma [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   488
 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   489
by (simp add: rec_all2_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   490
265
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   491
lemma all3_lemma [simp]:
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   492
 "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   493
by (simp add: rec_all3_def)
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   494
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   495
lemma all1_less_lemma [simp]:
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   496
  "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   497
apply(auto simp add: Let_def rec_all1_less_def)
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   498
apply (metis nat_less_le)+
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   499
done
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   500
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   501
lemma all2_less_lemma [simp]:
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   502
  "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   503
apply(auto simp add: Let_def rec_all2_less_def)
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   504
apply(metis nat_less_le)+
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   505
done
fa3c214559b0 finished recusive version of the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   506
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   507
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   508
lemma dvd_alt_def:
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   509
  fixes x y k:: nat
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   510
  shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)"
240
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   511
apply(auto simp add: dvd_def)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   512
apply(case_tac x)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   513
apply(auto)
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   514
done
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   515
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   516
lemma dvd_lemma [simp]:
696081f445c2 added improved Recsursive function theory (not yet finished)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   517
  "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
247
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   518
unfolding dvd_alt_def
89ed51d72e4a eliminated explicit swap_lemmas
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 246
diff changeset
   519
by (auto simp add: rec_dvd_def)
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   520
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   521
fun Quo where
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   522
  "Quo x 0 = 0"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   523
| "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   524
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   525
lemma Quo0:
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   526
  shows "Quo 0 y = 0"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   527
apply(induct y)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   528
apply(auto)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   529
done
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   530
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   531
lemma Quo1:
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   532
  "x * (Quo x y) \<le> y"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   533
by (induct y) (simp_all)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   534
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   535
lemma Quo2: 
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   536
  "b * (Quo b a) + a mod b = a"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   537
by (induct a) (auto simp add: mod_Suc)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   538
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   539
lemma Quo3:
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   540
  "n * (Quo n m) = m - m mod n"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   541
using Quo2[of n m] by (auto)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   542
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   543
lemma Quo4:
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   544
  assumes h: "0 < x"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   545
  shows "y < x + x * Quo x y"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   546
proof -
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   547
  have "x - (y mod x) > 0" using mod_less_divisor assms by auto
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   548
  then have "y < y + (x - (y mod x))" by simp
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   549
  then have "y < x + (y - (y mod x))" by simp
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   550
  then show "y < x + x * (Quo x y)" by (simp add: Quo3) 
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   551
qed
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   552
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   553
lemma Quo_div: 
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   554
  shows "Quo x y = y div x"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   555
apply(case_tac "x = 0")
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   556
apply(simp add: Quo0)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   557
apply(subst split_div_lemma[symmetric])
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   558
apply(auto intro: Quo1 Quo4)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   559
done
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   560
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   561
lemma Quo_rec_quo:
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   562
  shows "rec_eval rec_quo [y, x] = Quo x y"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   563
by (induct y) (simp_all add: rec_quo_def)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   564
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   565
lemma quo_lemma [simp]:
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   566
  shows "rec_eval rec_quo [y, x] = y div x"
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   567
by (simp add: Quo_div Quo_rec_quo)
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   568
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   569
lemma rem_lemma [simp]:
249
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   570
  shows "rec_eval rec_mod [y, x] = y mod x"
6e7244ae43b8 polised a bit of the Recs-theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 247
diff changeset
   571
by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   572
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   573
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   574
section {* Bounded Maximisation *}
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   575
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   576
fun BMax_rec where
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   577
  "BMax_rec R 0 = 0"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   578
| "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   579
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   580
definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   581
  where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   582
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   583
lemma BMax_rec_eq1:
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   584
 "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   585
apply(induct x)
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   586
apply(auto intro: Greatest_equality Greatest_equality[symmetric])
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   587
apply(simp add: le_Suc_eq)
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   588
by metis
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   589
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   590
lemma BMax_rec_eq2:
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   591
  "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   592
apply(induct x)
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   593
apply(auto intro: Max_eqI Max_eqI[symmetric])
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   594
apply(simp add: le_Suc_eq)
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   595
by metis
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   596
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   597
lemma BMax_rec_eq3:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   598
  "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   599
by (simp add: BMax_rec_eq2 Set.filter_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   600
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   601
definition 
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   602
  "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   603
 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   604
lemma max1_lemma [simp]:
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   605
  "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   606
by (induct x) (simp_all add: rec_max1_def)
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   607
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   608
definition 
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   609
  "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
243
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   610
 
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   611
lemma max2_lemma [simp]:
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   612
  "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   613
by (induct x) (simp_all add: rec_max2_def)
ac32cc069e30 added max and lg functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 241
diff changeset
   614
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   615
section {* Encodings using Cantor's pairing function *}
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   616
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   617
text {*
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   618
  We use Cantor's pairing function from Nat_Bijection.
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   619
  However, we need to prove that the formulation of the
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   620
  decoding function there is recursive. For this we first 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   621
  prove that we can extract the maximal triangle number 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   622
  using @{term prod_decode}.
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   623
*}
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   624
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   625
abbreviation Max_triangle_aux where
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   626
  "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)"
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   627
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   628
abbreviation Max_triangle where
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   629
  "Max_triangle z \<equiv> Max_triangle_aux 0 z"
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   630
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   631
abbreviation
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   632
  "pdec1 z \<equiv> fst (prod_decode z)"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   633
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   634
abbreviation
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   635
  "pdec2 z \<equiv> snd (prod_decode z)"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   636
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   637
abbreviation 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   638
  "penc m n \<equiv> prod_encode (m, n)"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   639
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   640
lemma fst_prod_decode: 
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   641
  "pdec1 z = z - triangle (Max_triangle z)"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   642
by (subst (3) prod_decode_inverse[symmetric]) 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   643
   (simp add: prod_encode_def prod_decode_def split: prod.split)
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   644
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   645
lemma snd_prod_decode: 
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   646
  "pdec2 z = Max_triangle z - pdec1 z"
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   647
by (simp only: prod_decode_def)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   648
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   649
lemma le_triangle:
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   650
  "m \<le> triangle (n + m)"
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   651
by (induct_tac m) (simp_all)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   652
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   653
lemma Max_triangle_triangle_le:
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   654
  "triangle (Max_triangle z) \<le> z"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   655
by (subst (9) prod_decode_inverse[symmetric])
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   656
   (simp add: prod_decode_def prod_encode_def split: prod.split)
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   657
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   658
lemma Max_triangle_le: 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   659
  "Max_triangle z \<le> z"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   660
proof -
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   661
  have "Max_triangle z \<le> triangle (Max_triangle z)"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   662
    using le_triangle[of _ 0, simplified] by simp
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   663
  also have "... \<le> z" by (rule Max_triangle_triangle_le)
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   664
  finally show "Max_triangle z \<le> z" .
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   665
qed
254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   666
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   667
lemma w_aux: 
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   668
  "Max_triangle (triangle k + m) = Max_triangle_aux k m"
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   669
by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   670
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   671
lemma y_aux: "y \<le> Max_triangle_aux y k"
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   672
apply(induct k arbitrary: y rule: nat_less_induct)
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   673
apply(subst (1 2) prod_decode_aux.simps)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   674
apply(simp)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   675
apply(rule impI)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   676
apply(drule_tac x="n - Suc y" in spec)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   677
apply(drule mp)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   678
apply(auto)[1]
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   679
apply(drule_tac x="Suc y" in spec)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   680
apply(erule Suc_leD)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   681
done
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   682
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   683
lemma Max_triangle_greatest: 
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   684
  "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   685
apply(rule Greatest_equality[symmetric])
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   686
apply(rule disjI1)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   687
apply(rule conjI)
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   688
apply(rule Max_triangle_triangle_le)
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   689
apply(rule Max_triangle_le)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   690
apply(erule disjE)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   691
apply(erule conjE)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   692
apply(subst (asm) (1) le_iff_add)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   693
apply(erule exE)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   694
apply(clarify)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   695
apply(simp only: w_aux)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   696
apply(rule y_aux)
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   697
apply(simp)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   698
done
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   699
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   700
definition 
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   701
  "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]"
250
745547bdc1c7 added lemmas about a pairing function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 249
diff changeset
   702
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   703
lemma triangle_lemma [simp]:
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   704
  "rec_eval rec_triangle [x] = triangle x"
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   705
by (simp add: rec_triangle_def triangle_def)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   706
 
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   707
definition
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   708
  "rec_max_triangle = 
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   709
       (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   710
        CN (rec_max1 cond) [Id 1 0, Id 1 0])"
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   711
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   712
lemma max_triangle_lemma [simp]:
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   713
  "rec_eval rec_max_triangle [x] = Max_triangle x"
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   714
by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) 
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   715
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   716
definition
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   717
  "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   718
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   719
definition 
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   720
  "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]" 
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   721
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   722
definition 
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   723
  "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" 
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   724
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   725
lemma pdec1_lemma [simp]:
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   726
  "rec_eval rec_pdec1 [z] = pdec1 z"
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   727
by (simp add: rec_pdec1_def fst_prod_decode)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   728
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   729
lemma pdec2_lemma [simp]:
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   730
  "rec_eval rec_pdec2 [z] = pdec2 z"
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   731
by (simp add: rec_pdec2_def snd_prod_decode)
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   732
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   733
lemma penc_lemma [simp]:
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   734
  "rec_eval rec_penc [m, n] = penc m n"
255
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   735
by (simp add: rec_penc_def prod_encode_def)
4bf4d425e65d added recusive functions that decode triangle numbers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 254
diff changeset
   736
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   737
text {* encoding and decoding of lists of natural numbers *}
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   738
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   739
fun 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   740
  lenc :: "nat list \<Rightarrow> nat" 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   741
where
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   742
  "lenc [] = 0"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   743
| "lenc (x # xs) = penc (Suc x) (lenc xs)"
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   744
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   745
fun
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   746
  ldec :: "nat \<Rightarrow> nat \<Rightarrow> nat"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   747
where
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   748
  "ldec z 0 = (pdec1 z) - 1"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   749
| "ldec z (Suc n) = ldec (pdec2 z) n"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   750
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   751
lemma pdec_zero_simps [simp]:
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   752
  "pdec1 0 = 0" 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   753
  "pdec2 0 = 0"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   754
by (simp_all add: prod_decode_def prod_decode_aux.simps)
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   755
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   756
lemma ldec_zero:
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   757
  "ldec 0 n = 0"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   758
by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps)
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   759
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   760
lemma list_encode_inverse: 
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   761
  "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)"
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   762
by (induct xs arbitrary: n rule: lenc.induct) 
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   763
   (auto simp add: ldec_zero nth_Cons split: nat.splits)
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   764
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   765
259
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   766
lemma lenc_length_le:
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   767
  "length xs \<le> lenc xs"  
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   768
by (induct xs) (simp_all add: prod_encode_def)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   769
257
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   770
fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   771
  "within z 0 = (0 < z)"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   772
| "within z (Suc n) = within (pdec2 z) n"
df6e8cb22995 more about the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 256
diff changeset
   773
    
259
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   774
definition enclen :: "nat \<Rightarrow> nat" where
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   775
  "enclen z = BMax_rec (\<lambda>x. within z (x - 1)) z"
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   776
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   777
lemma within_False [simp]:
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   778
  "within 0 n = False"
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   779
by (induct n) (simp_all)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   780
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   781
lemma within_length [simp]:
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   782
  "within (lenc xs) s = (s < length xs)"
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   783
apply(induct s arbitrary: xs)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   784
apply(case_tac xs)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   785
apply(simp_all add: prod_encode_def)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   786
apply(case_tac xs)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   787
apply(simp_all)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   788
done
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   789
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   790
lemma enclen_length [simp]:
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   791
  "enclen (lenc xs) = length xs"
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   792
unfolding enclen_def
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   793
apply(simp add: BMax_rec_eq1)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   794
apply(rule Greatest_equality)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   795
apply(auto simp add: lenc_length_le)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   796
done
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   797
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   798
lemma enclen_penc [simp]:
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   799
  "enclen (penc (Suc x) (lenc xs)) = Suc (enclen (lenc xs))"
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   800
by (simp only: lenc.simps[symmetric] enclen_length) (simp)
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   801
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   802
lemma enclen_zero [simp]:
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   803
  "enclen 0 = 0"
4524c5edcafb moved new theries into a separate directory
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   804
by (simp add: enclen_def)
256
04700724250f completed coding functions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 255
diff changeset
   805
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   806
fun 
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   807
  rec_lenc :: "recf list \<Rightarrow> recf" 
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   808
where
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   809
  "rec_lenc [] = Z"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   810
| "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]"
260
1e45b5b6482a added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   811
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   812
definition 
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   813
  "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   814
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   815
definition 
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   816
  "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   817
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   818
definition
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   819
  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   820
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   821
lemma ldec_iter:
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   822
  "ldec z n = pdec1 ((Iter pdec2 n) z) - 1"
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   823
by (induct n arbitrary: z) (simp | subst Iter_comm)+
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   824
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   825
lemma within_iter:
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   826
  "within z n = (0 < (Iter pdec2 n) z)"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   827
by (induct n arbitrary: z) (simp | subst Iter_comm)+
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   828
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   829
lemma lenc_lemma [simp]:
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   830
  "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   831
by (induct fs) (simp_all)
245
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   832
262
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   833
lemma ldec_lemma [simp]:
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   834
  "rec_eval rec_ldec [z, n] = ldec z n"
5704925ad138 started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 260
diff changeset
   835
by (simp add: ldec_iter rec_ldec_def)
245
af60d84e0677 introduced rec_if
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   836
263
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   837
lemma within_lemma [simp]:
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   838
  "rec_eval rec_within [z, n] = (if within z n then 1 else 0)"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   839
by (simp add: within_iter rec_within_def)
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   840
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   841
lemma enclen_lemma [simp]:
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   842
  "rec_eval rec_enclen [z] = enclen z"
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   843
by (simp add: rec_enclen_def enclen_def)
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   844
aa102c182132 more rec-funs definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 262
diff changeset
   845
244
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   846
end
8dba6ae39bf0 started with UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   847