Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Recs.thy
changeset 243 ac32cc069e30
parent 241 e59e549e6ab6
child 244 8dba6ae39bf0
equal deleted inserted replaced
242:4a943f0fe1b0 243:ac32cc069e30 
     2 imports Main Fact "~~/src/HOL/Number_Theory/Primes"
 
     2 imports Main Fact "~~/src/HOL/Number_Theory/Primes"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 lemma if_zero_one [simp]:
 
     5 lemma if_zero_one [simp]:
 
     6   "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
 
     6   "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
 
     7   "(if P then 0 else 1) = (0::nat) \<longleftrightarrow> P"
 
       
     8   "(0::nat) < (if P then 1 else 0) = P"
 
     7   "(0::nat) < (if P then 1 else 0) = P"
 
       
     8   "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))"
 
     9 by (simp_all)
 
     9 by (simp_all)
 
    10 
    10 
    11 lemma nth:
 
    11 lemma nth:
 
    12   "(x # xs) ! 0 = x"
 
    12   "(x # xs) ! 0 = x"
 
    13   "(x # y # xs) ! 1 = y"
 
    13   "(x # y # xs) ! 1 = y"
 
    14   "(x # y # z # xs) ! 2 = z"
 
    14   "(x # y # z # xs) ! 2 = z"
 
    15   "(x # y # z # u # xs) ! 3 = u"
 
    15   "(x # y # z # u # xs) ! 3 = u"
 
    16 by (simp_all)
 
    16 by (simp_all)
 
    17 
    17 
    18 lemma setprod_atMost_Suc[simp]: "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
 
    18 
       
    19 section {* Some auxiliary lemmas about @{text "\<Sum>"} and @{text "\<Prod>"} *}
 
       
    20 
       
    21 lemma setprod_atMost_Suc[simp]: 
       
    22   "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
 
    19 by(simp add:atMost_Suc mult_ac)
 
    23 by(simp add:atMost_Suc mult_ac)
 
    20 
    24 
    21 lemma setprod_lessThan_Suc[simp]: "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
 
    25 lemma setprod_lessThan_Suc[simp]: 
       
    26   "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
 
    22 by (simp add:lessThan_Suc mult_ac)
 
    27 by (simp add:lessThan_Suc mult_ac)
 
    23 
    28 
    24 lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
 
    29 lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
 
    25   setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
 
    30   setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
 
    26 apply(subst setsum_Un_disjoint[symmetric])
 
    31 apply(subst setsum_Un_disjoint[symmetric])
 
    27 apply(auto simp add: ivl_disj_un_one)
 
    32 apply(auto simp add: ivl_disj_un_one)
 
    28 done
 
    33 done
 
    29 
    34 
    30 
       
    31 lemma setsum_eq_zero [simp]:
 
    35 lemma setsum_eq_zero [simp]:
 
    32   fixes n::nat
 
    36   fixes f::"nat \<Rightarrow> nat"
 
    33   shows "(\<Sum>i < n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
    37   shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
    34         "(\<Sum>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
    38         "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
    35 by (auto)
 
    39 by (auto)
 
    36 
    40 
    37 lemma setprod_eq_zero [simp]:
 
    41 lemma setprod_eq_zero [simp]:
 
    38   fixes n::nat
 
    42   fixes f::"nat \<Rightarrow> nat"
 
    39   shows "(\<Prod>i < n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
    43   shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
    40         "(\<Prod>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
    44         "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
    41 by (auto)
 
    45 by (auto)
 
    42 
    46 
    43 lemma setsum_one_less:
 
    47 lemma setsum_one_less:
 
    44   fixes n::nat
 
    48   fixes n::nat
 
    45   assumes "\<forall>i < n. f i \<le> 1" 
    49   assumes "\<forall>i < n. f i \<le> 1" 
    60   shows "(\<Sum>i \<le> n. f i) = Suc n"  
    64   shows "(\<Sum>i \<le> n. f i) = Suc n"  
    61 using assms
 
    65 using assms
 
    62 by (induct n) (auto)
 
    66 by (induct n) (auto)
 
    63 
    67 
    64 lemma setsum_least_eq:
 
    68 lemma setsum_least_eq:
 
    65   fixes n p::nat
 
    69   fixes f::"nat \<Rightarrow> nat"
 
    66   assumes h0: "p \<le> n"
 
    70   assumes h0: "p \<le> n"
 
    67   assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
 
    71   assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
 
    68   assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
 
    72   assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
 
    69   shows "(\<Sum>i \<le> n. f i) = p"  
    73   shows "(\<Sum>i \<le> n. f i) = p"  
    70 proof -
 
    74 proof -
 
    76     using h0 by (simp add: setsum_add_nat_ivl2) 
    80     using h0 by (simp add: setsum_add_nat_ivl2) 
    77   also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp
 
    81   also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp
 
    78   finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp
 
    82   finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp
 
    79 qed
 
    83 qed
 
    80 
    84 
       
    85 lemma nat_mult_le_one:
 
       
    86   fixes m n::nat
 
       
    87   assumes "m \<le> 1" "n \<le> 1"
 
       
    88   shows "m * n \<le> 1"
 
       
    89 using assms by (induct n) (auto)
 
       
    90 
    81 lemma setprod_one_le:
 
    91 lemma setprod_one_le:
 
    82   fixes n::nat
 
    92   fixes f::"nat \<Rightarrow> nat"
 
    83   assumes "\<forall>i \<le> n. f i \<le> (1::nat)" 
    93   assumes "\<forall>i \<le> n. f i \<le> 1" 
    84   shows "(\<Prod>i \<le> n. f i) \<le> 1" 
    94   shows "(\<Prod>i \<le> n. f i) \<le> 1" 
    85 using assms
 
    95 using assms by (induct n) (auto intro: nat_mult_le_one)
 
    86 apply(induct n) 
       
    87 apply(auto)
 
       
    88 by (metis One_nat_def eq_iff le_0_eq le_SucE mult_0 nat_mult_1)
 
       
    89 
    96 
    90 lemma setprod_greater_zero:
 
    97 lemma setprod_greater_zero:
 
    91   fixes n::nat
 
    98   fixes f::"nat \<Rightarrow> nat"
 
    92   assumes "\<forall>i \<le> n. f i \<ge> (0::nat)" 
    99   assumes "\<forall>i \<le> n. f i \<ge> 0" 
    93   shows "(\<Prod>i \<le> n. f i) \<ge> 0" 
   100   shows "(\<Prod>i \<le> n. f i) \<ge> 0" 
    94 using assms
 
   101 using assms by (induct n) (auto)
 
    95 by (induct n) (auto)
 
       
    96 
   102 
    97 lemma setprod_eq_one:
 
   103 lemma setprod_eq_one:
 
    98   fixes n::nat
 
   104   fixes f::"nat \<Rightarrow> nat"
 
    99   assumes "\<forall>i \<le> n. f i = Suc 0" 
   105   assumes "\<forall>i \<le> n. f i = Suc 0" 
   100   shows "(\<Prod>i \<le> n. f i) = Suc 0" 
   106   shows "(\<Prod>i \<le> n. f i) = Suc 0" 
   101 using assms
 
   107 using assms by (induct n) (auto)
 
   102 by (induct n) (auto)
 
       
   103 
   108 
   104 lemma setsum_cut_off_less:
 
   109 lemma setsum_cut_off_less:
 
   105   fixes n::nat
 
   110   fixes f::"nat \<Rightarrow> nat"
 
   106   assumes h1: "m \<le> n"
 
   111   assumes h1: "m \<le> n"
 
   107   and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
 
   112   and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
 
   108   shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
 
   113   shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
 
   109 proof -
 
   114 proof -
 
   110   have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 
   115   have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 
   114   also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
 
   119   also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
 
   115   finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp
 
   120   finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp
 
   116 qed
 
   121 qed
 
   117 
   122 
   118 lemma setsum_cut_off_le:
 
   123 lemma setsum_cut_off_le:
 
   119   fixes n::nat
 
   124   fixes f::"nat \<Rightarrow> nat"
 
   120   assumes h1: "m \<le> n"
 
   125   assumes h1: "m \<le> n"
 
   121   and     h2: "\<forall>i \<in> {m..n}. f i = 0"
 
   126   and     h2: "\<forall>i \<in> {m..n}. f i = 0"
 
   122   shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
 
   127   shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
 
   123 proof -
 
   128 proof -
 
   124   have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" 
   129   have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" 
   134   shows "(\<Prod>i < n. Suc 0) = Suc 0"
 
   139   shows "(\<Prod>i < n. Suc 0) = Suc 0"
 
   135         "(\<Prod>i \<le> n. Suc 0) = Suc 0"
 
   140         "(\<Prod>i \<le> n. Suc 0) = Suc 0"
 
   136 by (induct n) (simp_all)
 
   141 by (induct n) (simp_all)
 
   137 
   142 
   138 
   143 
   139 datatype recf =  z
 
   144 
   140               |  s
 
   145 section {* Recursive Functions *}
 
   141               |  id nat nat
 
   146 
       
   147 datatype recf =  Z
 
       
   148               |  S
 
       
   149               |  Id nat nat
 
   142               |  Cn nat recf "recf list"
 
   150               |  Cn nat recf "recf list"
 
   143               |  Pr nat recf recf
 
   151               |  Pr nat recf recf
 
   144               |  Mn nat recf 
   152               |  Mn nat recf 
   145 
   153 
   146 fun arity :: "recf \<Rightarrow> nat"
 
   154 fun arity :: "recf \<Rightarrow> nat"
 
   147   where
 
   155   where
 
   148   "arity z = 1" 
   156   "arity Z = 1" 
   149 | "arity s = 1"
 
   157 | "arity S = 1"
 
   150 | "arity (id m n) = m"
 
   158 | "arity (Id m n) = m"
 
   151 | "arity (Cn n f gs) = n"
 
   159 | "arity (Cn n f gs) = n"
 
   152 | "arity (Pr n f g) = Suc n"
 
   160 | "arity (Pr n f g) = Suc n"
 
   153 | "arity (Mn n f) = n"
 
   161 | "arity (Mn n f) = n"
 
   154 
   162 
   155 abbreviation
 
   163 abbreviation
 
   158 abbreviation
 
   166 abbreviation
 
   159   "PR f g \<equiv> Pr (arity f) f g"
 
   167   "PR f g \<equiv> Pr (arity f) f g"
 
   160 
   168 
   161 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
 
   169 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
 
   162   where
 
   170   where
 
   163   "rec_eval z xs = 0" 
   171   "rec_eval Z xs = 0" 
   164 | "rec_eval s xs = Suc (xs ! 0)" 
   172 | "rec_eval S xs = Suc (xs ! 0)" 
   165 | "rec_eval (id m n) xs = xs ! n" 
   173 | "rec_eval (Id m n) xs = xs ! n" 
   166 | "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 
   174 | "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 
   167 | "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"
 
   175 | "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"
 
   168 | "rec_eval (Pr n f g) (Suc x # xs) = 
   176 | "rec_eval (Pr n f g) (Suc x # xs) = 
   169      rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)"
 
   177      rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)"
 
   170 | "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)"
 
   178 | "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)"
 
   171 
   179 
   172 inductive 
   180 inductive 
   173   terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
 
   181   terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
 
   174 where
 
   182 where
 
   175   termi_z: "terminates z [n]"
 
   183   termi_z: "terminates Z [n]"
 
   176 | termi_s: "terminates s [n]"
 
   184 | termi_s: "terminates S [n]"
 
   177 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"
 
   185 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (Id m n) xs"
 
   178 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
   186 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
   179               \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
 
   187               \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
 
   180 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
 
   188 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
 
   181               terminates f xs;
 
   189               terminates f xs;
 
   182               length xs = n\<rbrakk> 
   190               length xs = n\<rbrakk> 
   192   @{text "constn n"} is the recursive function which computes 
   200   @{text "constn n"} is the recursive function which computes 
   193   natural number @{text "n"}.
 
   201   natural number @{text "n"}.
 
   194 *}
 
   202 *}
 
   195 fun constn :: "nat \<Rightarrow> recf"
 
   203 fun constn :: "nat \<Rightarrow> recf"
 
   196   where
 
   204   where
 
   197   "constn 0 = z"  |
 
   205   "constn 0 = Z"  |
 
   198   "constn (Suc n) = CN s [constn n]"
 
   206   "constn (Suc n) = CN S [constn n]"
 
   199 
   207 
   200 definition
 
   208 definition
 
   201   "rec_swap f = CN f [id 2 1, id 2 0]"
 
   209   "rec_swap f = CN f [Id 2 1, Id 2 0]"
 
   202 
   210 
   203 definition
 
   211 definition
 
   204   "rec_add = PR (id 1 0) (CN s [id 3 1])"
 
   212   "rec_add = PR (Id 1 0) (CN S [Id 3 1])"
 
   205 
   213 
   206 definition 
   214 definition 
   207   "rec_mult = PR z (CN rec_add [id 3 1, id 3 2])"
 
   215   "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
 
   208 
   216 
   209 definition 
   217 definition 
   210   "rec_power_swap = PR (constn 1) (CN rec_mult [id 3 1, id 3 2])"
 
   218   "rec_power_swap = PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2])"
 
   211 
   219 
   212 definition
 
   220 definition
 
   213   "rec_power = rec_swap rec_power_swap"
 
   221   "rec_power = rec_swap rec_power_swap"
 
   214 
   222 
   215 definition
 
   223 definition
 
   216   "rec_fact = PR (constn 1) (CN rec_mult [CN s [id 3 0], id 3 1])"
 
   224   "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
 
   217 
   225 
   218 definition 
   226 definition 
   219   "rec_pred = CN (PR z (id 3 0)) [id 1 0, id 1 0]"
 
   227   "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
   220 
   228 
   221 definition 
   229 definition 
   222   "rec_minus_swap = (PR (id 1 0) (CN rec_pred [id 3 1]))"
 
   230   "rec_minus_swap = (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
   223 
   231 
   224 definition
 
   232 definition
 
   225   "rec_minus = rec_swap rec_minus_swap"
 
   233   "rec_minus = rec_swap rec_minus_swap"
 
   226 
   234 
   227 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
 
   235 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
 
   228 definition 
   236 
   229   "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, id 1 0]]"
 
   237 definition 
   230 
   238   "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
 
   231 definition 
   239 
   232   "rec_not = CN rec_minus [constn 1, id 1 0]"
 
   240 definition 
       
   241   "rec_not = CN rec_minus [constn 1, Id 1 0]"
 
   233 
   242 
   234 text {*
 
   243 text {*
 
   235   @{text "rec_eq"} compares two arguments: returns @{text "1"}
 
   244   @{text "rec_eq"} compares two arguments: returns @{text "1"}
 
   236   if they are equal; @{text "0"} otherwise. *}
 
   245   if they are equal; @{text "0"} otherwise. *}
 
   237 definition 
   246 definition 
   238   "rec_eq = CN rec_minus 
   247   "rec_eq = CN rec_minus 
   239              [CN (constn 1) [id 2 0], 
   248              [CN (constn 1) [Id 2 0], 
   240               CN rec_add [rec_minus, rec_swap rec_minus]]"
 
   249               CN rec_add [rec_minus, rec_swap rec_minus]]"
 
   241 
   250 
   242 definition 
   251 definition 
   243   "rec_noteq = CN rec_not [rec_eq]"
 
   252   "rec_noteq = CN rec_not [rec_eq]"
 
   244 
   253 
   247 
   256 
   248 definition 
   257 definition 
   249   "rec_disj = CN rec_sign [rec_add]"
 
   258   "rec_disj = CN rec_sign [rec_add]"
 
   250 
   259 
   251 definition 
   260 definition 
   252   "rec_imp = CN rec_disj [CN rec_not [id 2 0], id 2 1]"
 
   261   "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
 
       
   262 
       
   263 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
 
       
   264   y otherwise *}
 
       
   265 definition 
       
   266   "rec_ifz = PR (Id 2 0) (Id 4 3)"
 
   253 
   267 
   254 text {*
 
   268 text {*
 
   255   @{text "rec_less"} compares two arguments and returns @{text "1"} if
 
   269   @{text "rec_less"} compares two arguments and returns @{text "1"} if
 
   256   the first is less than the second; otherwise returns @{text "0"}. *}
 
   270   the first is less than the second; otherwise returns @{text "0"}. *}
 
   257 definition 
   271 definition 
   261   "rec_le = CN rec_disj [rec_less, rec_eq]"
 
   275   "rec_le = CN rec_disj [rec_less, rec_eq]"
 
   262 
   276 
   263 text {* Sigma and Accum for function with one and two arguments *}
 
   277 text {* Sigma and Accum for function with one and two arguments *}
 
   264 
   278 
   265 definition 
   279 definition 
   266   "rec_sigma1 f = PR (CN f [z, id 1 0]) (CN rec_add [id 3 1, CN f [s, id 3 2]])"
 
   280   "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
 
   267 
   281 
   268 definition 
   282 definition 
   269   "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]])"
 
   283   "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]])"
 
   270 
   284 
   271 definition 
   285 definition 
   272   "rec_accum1 f = PR (CN f [z, id 1 0]) (CN rec_mult [id 3 1, CN f [s, id 3 2]])"
 
   286   "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
 
   273 
   287 
   274 definition 
   288 definition 
   275   "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]])"
 
   289   "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]])"
 
   276 
   290 
   277 text {* Bounded quantifiers for one and two arguments *}
 
   291 text {* Bounded quantifiers for one and two arguments *}
 
   278 
   292 
   279 definition
 
   293 definition
 
   280   "rec_all1 f = CN rec_sign [rec_accum1 f]"
 
   294   "rec_all1 f = CN rec_sign [rec_accum1 f]"
 
   289   "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
 
   303   "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
 
   290 
   304 
   291 text {* Dvd *}
 
   305 text {* Dvd *}
 
   292 
   306 
   293 definition 
   307 definition 
   294   "rec_dvd_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]"  
   308   "rec_dvd_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]"  
   295 
   309 
   296 definition 
   310 definition 
   297   "rec_dvd = rec_swap rec_dvd_swap" 
   311   "rec_dvd = rec_swap rec_dvd_swap" 
       
   312 
       
   313 
   298 
   314 
   299 section {* Correctness of Recursive Functions *}
 
   315 section {* Correctness of Recursive Functions *}
 
   300 
   316 
   301 lemma constn_lemma [simp]: 
   317 lemma constn_lemma [simp]: 
   302   "rec_eval (constn n) xs = n"
 
   318   "rec_eval (constn n) xs = n"
 
   372 
   388 
   373 lemma le_lemma [simp]: 
   389 lemma le_lemma [simp]: 
   374   "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
 
   390   "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
 
   375 by(simp add: rec_le_def)
 
   391 by(simp add: rec_le_def)
 
   376 
   392 
       
   393 lemma ifz_lemma [simp]:
 
       
   394   "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" 
       
   395 by (case_tac z) (simp_all add: rec_ifz_def)
 
   377 
   396 
   378 lemma sigma1_lemma [simp]: 
   397 lemma sigma1_lemma [simp]: 
   379   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
 
   398   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
 
   380 by (induct x) (simp_all add: rec_sigma1_def)
 
   399 by (induct x) (simp_all add: rec_sigma1_def)
 
   381 
   400 
   407  "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
 
   426  "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
 
   408 by (simp add: rec_all2_def)
 
   427 by (simp add: rec_all2_def)
 
   409 
   428 
   410 
   429 
   411 lemma dvd_alt_def:
 
   430 lemma dvd_alt_def:
 
   412   "(x dvd y) = (\<exists>k\<le>y. y = x * (k::nat))"
 
   431   fixes x y k:: nat
 
       
   432   shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)"
 
   413 apply(auto simp add: dvd_def)
 
   433 apply(auto simp add: dvd_def)
 
   414 apply(case_tac x)
 
   434 apply(case_tac x)
 
   415 apply(auto)
 
   435 apply(auto)
 
   416 done
 
   436 done
 
   417 
   437 
   422 
   442 
   423 lemma dvd_lemma [simp]:
 
   443 lemma dvd_lemma [simp]:
 
   424   "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
 
   444   "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
 
   425 by (simp add: rec_dvd_def)
 
   445 by (simp add: rec_dvd_def)
 
   426 
   446 
   427 definition 
   447 
   428   "rec_prime = 
   448 section {* Prime Numbers *}
 
   429     (let conj1 = CN rec_less [constn 1, id 1 0] in
 
       
   430      let disj  = CN rec_disj [CN rec_eq [id 2 0, constn 1], rec_eq] in
 
       
   431      let imp   = CN rec_imp [rec_dvd, disj] in
 
       
   432      let conj2 = CN (rec_all1 imp) [id 1 0, id 1 0] in
 
       
   433      CN rec_conj [conj1, conj2])"
 
       
   434 
   449 
   435 lemma prime_alt_def:
 
   450 lemma prime_alt_def:
 
   436   fixes p::nat
 
   451   fixes p::nat
 
   437   shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
 
   452   shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
 
   438 apply(auto simp add: prime_nat_def dvd_def)
 
   453 apply(auto simp add: prime_nat_def dvd_def)
 
   439 by (metis One_nat_def le_neq_implies_less less_SucI less_Suc_eq_0_disj less_Suc_eq_le mult_is_0 n_less_n_mult_m not_less_eq_eq)
 
   454 apply(drule_tac x="k" in spec)
 
       
   455 apply(auto)
 
       
   456 done
 
       
   457 
       
   458 definition 
       
   459   "rec_prime = 
       
   460     (let conj1 = CN rec_less [constn 1, Id 1 0] in
 
       
   461      let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
 
       
   462      let imp   = CN rec_imp [rec_dvd, disj] in
 
       
   463      let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
 
       
   464      CN rec_conj [conj1, conj2])"
 
   440 
   465 
   441 lemma prime_lemma [simp]: 
   466 lemma prime_lemma [simp]: 
   442   "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
 
   467   "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
 
   443 by (simp add: rec_prime_def Let_def prime_alt_def)
 
   468 by (auto simp add: rec_prime_def Let_def prime_alt_def)
 
       
   469 
       
   470 section {* Bounded Min and Maximisation *}
 
       
   471 
       
   472 fun BMax_rec where
 
       
   473   "BMax_rec R 0 = 0"
 
       
   474 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"
 
       
   475 
       
   476 definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
 
       
   477   where "BMax_set R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})"
 
       
   478 
       
   479 definition (in ord)
 
       
   480   Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
 
       
   481   "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"
 
       
   482 
       
   483 lemma Great_equality:
 
       
   484   fixes x::nat
 
       
   485   assumes "P x" "\<And>y. P y \<Longrightarrow> y \<le> x"
 
       
   486   shows "Great P = x"
 
       
   487 unfolding Great_def 
       
   488 using assms 
       
   489 by(rule_tac the_equality) (auto intro: le_antisym)
 
       
   490 
       
   491 lemma BMax_rec_eq1:
 
       
   492  "BMax_rec R x = (GREAT z. (R z \<and> z \<le> x) \<or> z = 0)"
 
       
   493 apply(induct x)
 
       
   494 apply(auto intro: Great_equality Great_equality[symmetric])
 
       
   495 apply(simp add: le_Suc_eq)
 
       
   496 by metis
 
       
   497 
       
   498 lemma BMax_rec_eq2:
 
       
   499   "BMax_rec R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})"
 
       
   500 apply(induct x)
 
       
   501 apply(auto intro: Max_eqI Max_eqI[symmetric])
 
       
   502 apply(simp add: le_Suc_eq)
 
       
   503 by metis
 
       
   504 
       
   505 definition 
       
   506   "rec_max1 f = PR (constn 0)
 
       
   507                    (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])"
 
       
   508  
       
   509 lemma max1_lemma [simp]:
 
       
   510   "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
 
       
   511 by (induct x) (simp_all add: rec_max1_def)
 
       
   512 
       
   513 definition 
       
   514   "rec_max2 f = PR (constn 0)
 
       
   515                    (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
 
       
   516  
       
   517 lemma max2_lemma [simp]:
 
       
   518   "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
 
       
   519 by (induct x) (simp_all add: rec_max2_def)
 
       
   520 
       
   521 definition
 
       
   522   "rec_lg = 
       
   523      (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in
 
       
   524       let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
 
       
   525       let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
       
   526       in CN rec_ifz [cond, Z, max])"
 
       
   527 
       
   528 definition
 
       
   529   "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)"
 
       
   530 
       
   531 lemma lg_lemma:
 
       
   532   "rec_eval rec_lg [x, y] = Lg x y"
 
       
   533 by (simp add: rec_lg_def Lg_def Let_def)
 
       
   534 
       
   535 
       
   536 
       
   537 
       
   538 
       
   539 fun mtest where
 
       
   540   "mtest R 0 = if R 0 then 0 else 1"
 
       
   541 | "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
 
       
   542 
       
   543 
       
   544 lemma 
       
   545   "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
 
       
   546 apply(simp only: rec_maxr2_def)
 
       
   547 apply(case_tac x)
 
       
   548 apply(clarify)
 
       
   549 apply(subst rec_eval.simps)
 
       
   550 apply(simp only: constn_lemma)
 
       
   551 defer
 
       
   552 apply(clarify)
 
       
   553 apply(subst rec_eval.simps)
 
       
   554 apply(simp only: rec_maxr2_def[symmetric])
 
       
   555 apply(subst rec_eval.simps)
 
       
   556 apply(simp only: map.simps nth)
 
       
   557 apply(subst rec_eval.simps)
 
       
   558 apply(simp only: map.simps nth)
 
       
   559 apply(subst rec_eval.simps)
 
       
   560 apply(simp only: map.simps nth)
 
       
   561 apply(subst rec_eval.simps)
 
       
   562 apply(simp only: map.simps nth)
 
       
   563 apply(subst rec_eval.simps)
 
       
   564 apply(simp only: map.simps nth)
 
       
   565 apply(subst rec_eval.simps)
 
       
   566 apply(simp only: map.simps nth)
 
       
   567 
   444 
   568 
   445 definition
 
   569 definition
 
   446   "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
 
   570   "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
 
   447 
   571 
   448 fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat"
 
   572 definition
 
   449   where "Minr2 R (x # ys) = Min ({z | z. z \<le> x \<and> R (z # ys)} \<union> {Suc x})"
 
   573   "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
 
       
   574 
       
   575 definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
 
       
   576   where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
 
       
   577 
       
   578 definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
 
       
   579   where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
 
       
   580 
       
   581 lemma rec_minr2_le_Suc:
 
       
   582   "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"
 
       
   583 apply(simp add: rec_minr2_def)
 
       
   584 apply(auto intro!: setsum_one_le setprod_one_le)
 
       
   585 done
 
       
   586 
       
   587 lemma rec_minr2_eq_Suc:
 
       
   588   assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
 
       
   589   shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
 
       
   590 using assms by (simp add: rec_minr2_def)
 
       
   591 
       
   592 lemma rec_minr2_le:
 
       
   593   assumes h1: "y \<le> x" 
       
   594   and     h2: "0 < rec_eval f [y, y1, y2]" 
       
   595   shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y"
 
       
   596 apply(simp add: rec_minr2_def)
 
       
   597 apply(subst setsum_cut_off_le[OF h1])
 
       
   598 using h2 apply(auto)
 
       
   599 apply(auto intro!: setsum_one_less setprod_one_le)
 
       
   600 done
 
       
   601 
       
   602 (* ??? *)
 
       
   603 lemma setsum_eq_one_le2:
 
       
   604   fixes n::nat
 
       
   605   assumes "\<forall>i \<le> n. f i \<le> 1" 
       
   606   shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)"  
       
   607 using assms
 
       
   608 apply(induct n)
 
       
   609 apply(simp add: One_nat_def)
 
       
   610 apply(simp)
 
       
   611 apply(auto simp add: One_nat_def)
 
       
   612 apply(drule_tac x="Suc n" in spec)
 
       
   613 apply(auto)
 
       
   614 by (metis le_Suc_eq)
 
       
   615 
       
   616 
       
   617 lemma rec_min2_not:
 
       
   618   assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
 
       
   619   shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
 
       
   620 using assms
 
       
   621 apply(simp add: rec_minr2_def)
 
       
   622 apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)")
 
       
   623 apply(simp)
 
       
   624 apply (metis atMost_iff le_refl zero_neq_one)
 
       
   625 apply(rule setsum_eq_one_le2)
 
       
   626 apply(auto)
 
       
   627 apply(rule setprod_one_le)
 
       
   628 apply(auto)
 
       
   629 done
 
       
   630 
       
   631 lemma disjCI2:
 
       
   632   assumes "~P ==> Q" shows "P|Q"
 
       
   633 apply (rule classical)
 
       
   634 apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
 
       
   635 done
 
   450 
   636 
   451 lemma minr_lemma [simp]:
 
   637 lemma minr_lemma [simp]:
 
   452 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr2 (\<lambda>xs. (0 < rec_eval f xs)) [x, y1, y2]"
 
   638 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
 
   453 apply(simp only: rec_minr2_def)
 
   639 apply(induct x)
 
   454 apply(simp)
 
   640 apply(rule Least_equality[symmetric])
 
       
   641 apply(simp add: rec_minr2_def)
 
       
   642 apply(erule disjE)
 
       
   643 apply(rule rec_minr2_le)
 
       
   644 apply(auto)[2]
 
       
   645 apply(simp)
 
       
   646 apply(rule rec_minr2_le_Suc)
 
       
   647 apply(simp)
 
       
   648 
       
   649 apply(rule rec_minr2_le)
 
       
   650 
       
   651 
       
   652 apply(rule rec_minr2_le_Suc)
 
       
   653 apply(rule disjCI)
 
       
   654 apply(simp add: rec_minr2_def)
 
       
   655 
       
   656 apply(ru le setsum_one_less)
 
       
   657 apply(clarify)
 
       
   658 apply(rule setprod_one_le)
 
       
   659 apply(auto)[1]
 
       
   660 apply(simp)
 
       
   661 apply(rule setsum_one_le)
 
       
   662 apply(clarify)
 
       
   663 apply(rule setprod_one_le)
 
       
   664 apply(auto)[1]
 
       
   665 thm disj_CE
 
       
   666 apply(auto)
 
       
   667 
       
   668 lemma minr_lemma:
 
       
   669 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
 
       
   670 apply(simp only: Minr_def)
 
   455 apply(rule sym)
 
   671 apply(rule sym)
 
   456 apply(rule Min_eqI)
 
   672 apply(rule Min_eqI)
 
   457 apply(auto)[1]
 
   673 apply(auto)[1]
 
   458 apply(simp)
 
   674 apply(simp)
 
   459 apply(erule disjE)
 
   675 apply(erule disjE)
 
   460 apply(simp)
 
   676 apply(simp)
 
       
   677 apply(rule rec_minr2_le_Suc)
 
       
   678 apply(rule rec_minr2_le)
 
       
   679 apply(auto)[2]
 
       
   680 apply(simp)
 
       
   681 apply(induct x)
 
       
   682 apply(simp add: rec_minr2_def)
 
       
   683 apply(
 
       
   684 apply(rule disjCI)
 
       
   685 apply(rule rec_minr2_eq_Suc)
 
       
   686 apply(simp)
 
       
   687 apply(auto)
 
       
   688 
   461 apply(rule setsum_one_le)
 
   689 apply(rule setsum_one_le)
 
   462 apply(auto)[1]
 
   690 apply(auto)[1]
 
   463 apply(rule setprod_one_le)
 
   691 apply(rule setprod_one_le)
 
   464 apply(auto)[1]
 
   692 apply(auto)[1]
 
   465 apply(subst setsum_cut_off_le)
 
   693 apply(subst setsum_cut_off_le)
 
   513 apply (metis neq0_conv not_less_Least)
 
   741 apply (metis neq0_conv not_less_Least)
 
   514 apply(auto)[1]
 
   742 apply(auto)[1]
 
   515 apply (metis (mono_tags) LeastI_ex)
 
   743 apply (metis (mono_tags) LeastI_ex)
 
   516 by (metis LeastI_ex)
 
   744 by (metis LeastI_ex)
 
   517 
   745 
       
   746 lemma minr_lemma:
 
       
   747 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
 
       
   748 apply(simp only: Minr_def rec_minr2_def)
 
       
   749 apply(simp)
 
       
   750 apply(rule sym)
 
       
   751 apply(rule Min_eqI)
 
       
   752 apply(auto)[1]
 
       
   753 apply(simp)
 
       
   754 apply(erule disjE)
 
       
   755 apply(simp)
 
       
   756 apply(rule setsum_one_le)
 
       
   757 apply(auto)[1]
 
       
   758 apply(rule setprod_one_le)
 
       
   759 apply(auto)[1]
 
       
   760 apply(subst setsum_cut_off_le)
 
       
   761 apply(auto)[2]
 
       
   762 apply(rule setsum_one_less)
 
       
   763 apply(auto)[1]
 
       
   764 apply(rule setprod_one_le)
 
       
   765 apply(auto)[1]
 
       
   766 apply(simp)
 
       
   767 thm setsum_eq_one_le
 
       
   768 apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>
 
       
   769                    (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))")
 
       
   770 prefer 2
 
       
   771 apply(auto)[1]
 
       
   772 apply(erule disjE)
 
       
   773 apply(rule disjI1)
 
       
   774 apply(rule setsum_eq_one_le)
 
       
   775 apply(simp)
 
       
   776 apply(rule disjI2)
 
       
   777 apply(simp)
 
       
   778 apply(clarify)
 
       
   779 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")
 
       
   780 defer
 
       
   781 apply metis
 
       
   782 apply(erule exE)
 
       
   783 apply(subgoal_tac "l \<le> x")
 
       
   784 defer
 
       
   785 apply (metis not_leE not_less_Least order_trans)
 
       
   786 apply(subst setsum_least_eq)
 
       
   787 apply(rotate_tac 4)
 
       
   788 apply(assumption)
 
       
   789 apply(auto)[1]
 
       
   790 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
 
       
   791 prefer 2
 
       
   792 apply(auto)[1]
 
       
   793 apply(rotate_tac 5)
 
       
   794 apply(drule not_less_Least)
 
       
   795 apply(auto)[1]
 
       
   796 apply(auto)
 
       
   797 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI)
 
       
   798 apply(simp)
 
       
   799 apply (metis LeastI_ex)
 
       
   800 apply(subst setsum_least_eq)
 
       
   801 apply(rotate_tac 3)
 
       
   802 apply(assumption)
 
       
   803 apply(simp)
 
       
   804 apply(auto)[1]
 
       
   805 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])")
 
       
   806 prefer 2
 
       
   807 apply(auto)[1]
 
       
   808 apply (metis neq0_conv not_less_Least)
 
       
   809 apply(auto)[1]
 
       
   810 apply (metis (mono_tags) LeastI_ex)
 
       
   811 by (metis LeastI_ex)
 
       
   812 
       
   813 lemma disjCI2:
 
       
   814   assumes "~P ==> Q" shows "P|Q"
 
       
   815 apply (rule classical)
 
       
   816 apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
 
       
   817 done
 
       
   818 
       
   819 
       
   820 lemma minr_lemma [simp]:
 
       
   821 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
 
       
   822 (*apply(simp add: rec_minr2_def)*)
 
       
   823 apply(rule Least_equality[symmetric])
 
       
   824 prefer 2
 
       
   825 apply(erule disjE)
 
       
   826 apply(rule rec_minr2_le)
 
       
   827 apply(auto)[2]
 
       
   828 apply(clarify)
 
       
   829 apply(rule rec_minr2_le_Suc)
 
       
   830 apply(rule disjCI)
 
       
   831 apply(simp add: rec_minr2_def)
 
       
   832 
       
   833 apply(ru le setsum_one_less)
 
       
   834 apply(clarify)
 
       
   835 apply(rule setprod_one_le)
 
       
   836 apply(auto)[1]
 
       
   837 apply(simp)
 
       
   838 apply(rule setsum_one_le)
 
       
   839 apply(clarify)
 
       
   840 apply(rule setprod_one_le)
 
       
   841 apply(auto)[1]
 
       
   842 thm disj_CE
 
       
   843 apply(auto)
 
       
   844 apply(auto)
 
       
   845 prefer 2
 
       
   846 apply(rule le_tran
 
       
   847 
       
   848 apply(rule le_trans)
 
       
   849 apply(simp)
 
       
   850 defer
 
       
   851 apply(auto)
 
       
   852 apply(subst setsum_cut_off_le)
 
       
   853 
       
   854 
       
   855 lemma 
       
   856   "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))" 
       
   857 apply(simp add: Minr_def)
 
       
   858 apply(rule Min_eqI)
 
       
   859 apply(auto)[1]
 
       
   860 apply(simp)
 
       
   861 apply(rule Least_le)
 
       
   862 apply(auto)[1]
 
       
   863 apply(rule LeastI2_wellorder)
 
       
   864 apply(auto)
 
       
   865 done
 
       
   866 
       
   867 definition (in ord)
 
       
   868   Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
 
       
   869   "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"
 
       
   870 
       
   871 (*
 
       
   872 lemma Great_equality:
 
       
   873   assumes "P x"
 
       
   874     and "\<And>y. P y \<Longrightarrow> y \<le> x"
 
       
   875   shows "Great P = x"
 
       
   876 unfolding Great_def 
       
   877 apply(rule the_equality)
 
       
   878 apply(blast intro: assms)
 
       
   879 *)
 
       
   880 
       
   881 
       
   882 
       
   883 lemma 
       
   884   "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))" 
       
   885 apply(simp add: Maxr_def)
 
       
   886 apply(rule Max_eqI)
 
       
   887 apply(auto)[1]
 
       
   888 apply(simp)
 
       
   889 thm Least_le Greatest_le
 
       
   890 oops
 
       
   891 
       
   892 lemma
 
       
   893   "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys"
 
       
   894 apply(simp add: Maxr_def Minr_def)
 
       
   895 apply(rule Max_eqI)
 
       
   896 apply(auto)[1]
 
       
   897 apply(simp)
 
       
   898 apply(erule disjE)
 
       
   899 apply(simp)
 
       
   900 apply(auto)[1]
 
       
   901 defer
 
       
   902 apply(simp)
 
       
   903 apply(auto)[1]
 
       
   904 thm Min_insert
 
       
   905 defer
 
       
   906 oops
 
       
   907 
       
   908 
       
   909 
   518 definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 
   910 definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 
   519   where
 
   911   where
 
   520   "quo x y = (if y = 0 then 0 else x div y)"
 
   912   "quo x y = (if y = 0 then 0 else x div y)"
 
   521 
   913 
   522 
   914 
   523 definition 
   915 definition 
   524   "rec_quo = CN rec_mult [CN rec_sign [id 2 1],  
   916   "rec_quo = CN rec_mult [CN rec_sign [Id 2 1],  
   525       CN (rec_minr2 (CN rec_less [id 3 1, CN rec_mult [CN s [id 3 0], id 3 2]])) 
   917       CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]])) 
   526                 [id 2 0, id 2 0, id 2 1]]"
 
   918                 [Id 2 0, Id 2 0, Id 2 1]]"
 
   527 
   919 
   528 lemma div_lemma [simp]:
 
   920 lemma div_lemma [simp]:
 
   529   "rec_eval rec_quo [x, y] = quo x y"
 
   921   "rec_eval rec_quo [x, y] = quo x y"
 
   530 apply(simp add: rec_quo_def quo_def)
 
   922 apply(simp add: rec_quo_def quo_def)
 
   531 apply(rule impI)
 
   923 apply(rule impI)
tm