theory Recs

imports Main Fact "~~/src/HOL/Number_Theory/Primes"

begin

lemma if_zero_one [simp]:

  "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"

  "(if P then 0 else 1) = (0::nat) \<longleftrightarrow> P"

  "(0::nat) < (if P then 1 else 0) = P"

by (simp_all)

lemma nth:

  "(x # xs) ! 0 = x"

  "(x # y # xs) ! 1 = y"

  "(x # y # z # xs) ! 2 = z"

  "(x # y # z # u # xs) ! 3 = u"

by (simp_all)

lemma setprod_atMost_Suc[simp]: "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"

by(simp add:atMost_Suc mult_ac)

lemma setprod_lessThan_Suc[simp]: "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"

by (simp add:lessThan_Suc mult_ac)

lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>

  setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"

apply(subst setsum_Un_disjoint[symmetric])

apply(auto simp add: ivl_disj_un_one)

done

lemma setsum_eq_zero [simp]:

  fixes n::nat

  shows "(\<Sum>i < n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i < n. f i = 0)" 

        "(\<Sum>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 

by (auto)

lemma setprod_eq_zero [simp]:

  fixes n::nat

  shows "(\<Prod>i < n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i < n. f i = 0)" 

        "(\<Prod>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 

by (auto)

lemma setsum_one_less:

  fixes n::nat

  assumes "\<forall>i < n. f i \<le> 1" 

  shows "(\<Sum>i < n. f i) \<le> n"  

using assms

by (induct n) (auto)

lemma setsum_least_eq:

  fixes n p::nat

  assumes h0: "p \<le> n"

  assumes h1: "\<forall>i \<in> {..<p}. f i = 1"

  assumes h2: "\<forall>i \<in> {p..n}. f i = 0"

  shows "(\<Sum>i \<le> n. f i) = p"  

proof -

  have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" 

    using h1 by (induct p) (simp_all)

  have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" 

    using h2 by auto

  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)"

    using h0 by (simp add: setsum_add_nat_ivl2) 

  also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp

  finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp

qed

lemma setprod_one_le:

  fixes n::nat

  assumes "\<forall>i \<le> n. f i \<le> (1::nat)" 

  shows "(\<Prod>i \<le> n. f i) \<le> 1" 

using assms

apply(induct n) 

apply(auto)

by (metis One_nat_def eq_iff le_0_eq le_SucE mult_0 nat_mult_1)

lemma setprod_greater_zero:

  fixes n::nat

  assumes "\<forall>i \<le> n. f i \<ge> (0::nat)" 

  shows "(\<Prod>i \<le> n. f i) \<ge> 0" 

using assms

by (induct n) (auto)

lemma setprod_eq_one:

  fixes n::nat

  assumes "\<forall>i \<le> n. f i = Suc 0" 

  shows "(\<Prod>i \<le> n. f i) = Suc 0" 

using assms

by (induct n) (auto)

lemma setsum_cut_off_less:

  fixes n::nat

  assumes h1: "m \<le> n"

  and     h2: "\<forall>i \<in> {m..<n}. f i = 0"

  shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"

proof -

  have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 

    using h2 by auto

  have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)"

    using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) 

  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp

  finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp

qed

lemma setsum_cut_off_le:

  fixes n::nat

  assumes h1: "m \<le> n"

  and     h2: "\<forall>i \<in> {m..n}. f i = 0"

  shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"

proof -

  have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" 

    using h2 by auto

  have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)"

    using h1 by (simp add: setsum_add_nat_ivl2)

  also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp

  finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp

qed

lemma setprod_one [simp]:

  fixes n::nat

  shows "(\<Prod>i < n. Suc 0) = Suc 0"

        "(\<Prod>i \<le> n. Suc 0) = Suc 0"

by (induct n) (simp_all)

datatype recf =  z

              |  s

              |  id nat nat

              |  Cn nat recf "recf list"

              |  Pr nat recf recf

              |  Mn nat recf 

fun arity :: "recf \<Rightarrow> nat"

  where

  "arity z = 1" 

| "arity s = 1"

| "arity (id m n) = m"

| "arity (Cn n f gs) = n"

| "arity (Pr n f g) = Suc n"

| "arity (Mn n f) = n"

abbreviation

  "CN f gs \<equiv> Cn (arity (hd gs)) f gs"

abbreviation

  "PR f g \<equiv> Pr (arity f) f g"

fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"

  where

  "rec_eval z xs = 0" 

| "rec_eval s xs = Suc (xs ! 0)" 

| "rec_eval (id m n) xs = xs ! n" 

| "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 

| "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"

| "rec_eval (Pr n f g) (Suc x # xs) = 

     rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)"

| "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)"

inductive 

  terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"

where

  termi_z: "terminates z [n]"

| termi_s: "terminates s [n]"

| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"

| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 

              \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"

| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));

              terminates f xs;

              length xs = n\<rbrakk> 

              \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"

| termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 

              rec_eval f (r # xs) = 0;

              \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"

section {* Recursive Function Definitions *}

text {*

  @{text "constn n"} is the recursive function which computes 

  natural number @{text "n"}.

*}

fun constn :: "nat \<Rightarrow> recf"

  where

  "constn 0 = z"  |

  "constn (Suc n) = CN s [constn n]"

definition

  "rec_swap f = CN f [id 2 1, id 2 0]"

definition

  "rec_add = PR (id 1 0) (CN s [id 3 1])"

definition 

  "rec_mult = PR z (CN rec_add [id 3 1, id 3 2])"

definition 

  "rec_power_swap = PR (constn 1) (CN rec_mult [id 3 1, id 3 2])"

definition

  "rec_power = rec_swap rec_power_swap"

definition

  "rec_fact = PR (constn 1) (CN rec_mult [CN s [id 3 0], id 3 1])"

definition 

  "rec_pred = CN (PR z (id 3 0)) [id 1 0, id 1 0]"

definition 

  "rec_minus_swap = (PR (id 1 0) (CN rec_pred [id 3 1]))"

definition

  "rec_minus = rec_swap rec_minus_swap"

text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}

definition 

  "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, id 1 0]]"

definition 

  "rec_not = CN rec_minus [constn 1, id 1 0]"

text {*

  @{text "rec_eq"} compares two arguments: returns @{text "1"}

  if they are equal; @{text "0"} otherwise. *}

definition 

  "rec_eq = CN rec_minus 

             [CN (constn 1) [id 2 0], 

              CN rec_add [rec_minus, rec_swap rec_minus]]"

definition 

  "rec_noteq = CN rec_not [rec_eq]"

definition 

  "rec_conj = CN rec_sign [rec_mult]"

definition 

  "rec_disj = CN rec_sign [rec_add]"

definition 

  "rec_imp = CN rec_disj [CN rec_not [id 2 0], id 2 1]"

text {*

  @{text "rec_less"} compares two arguments and returns @{text "1"} if

  the first is less than the second; otherwise returns @{text "0"}. *}

definition 

  "rec_less = CN rec_sign [rec_swap rec_minus]"

definition 

  "rec_le = CN rec_disj [rec_less, rec_eq]"

text {* Sigma and Accum for function with one and two arguments *}

definition 

  "rec_sigma1 f = PR (CN f [z, id 1 0]) (CN rec_add [id 3 1, CN f [s, id 3 2]])"

definition 

  "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]])"

definition 

  "rec_accum1 f = PR (CN f [z, id 1 0]) (CN rec_mult [id 3 1, CN f [s, id 3 2]])"

definition 

  "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]])"

text {* Bounded quantifiers for one and two arguments *}

definition

  "rec_all1 f = CN rec_sign [rec_accum1 f]"

definition

  "rec_all2 f = CN rec_sign [rec_accum2 f]"

definition

  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"

definition

  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"

text {* Dvd *}

definition 

  "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]"  

definition 

  "rec_dvd = rec_swap rec_dvd_swap" 

section {* Correctness of Recursive Functions *}

lemma constn_lemma [simp]: 

  "rec_eval (constn n) xs = n"

by (induct n) (simp_all)

lemma swap_lemma [simp]:

  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"

by (simp add: rec_swap_def)

lemma add_lemma [simp]: 

  "rec_eval rec_add [x, y] =  x + y"

by (induct x) (simp_all add: rec_add_def)

lemma mult_lemma [simp]: 

  "rec_eval rec_mult [x, y] = x * y"

by (induct x) (simp_all add: rec_mult_def)

lemma power_swap_lemma [simp]: 

  "rec_eval rec_power_swap [y, x] = x ^ y"

by (induct y) (simp_all add: rec_power_swap_def)

lemma power_lemma [simp]: 

  "rec_eval rec_power [x, y] = x ^ y"

by (simp add: rec_power_def)

lemma fact_lemma [simp]: 

  "rec_eval rec_fact [x] = fact x"

by (induct x) (simp_all add: rec_fact_def)

lemma pred_lemma [simp]: 

  "rec_eval rec_pred [x] =  x - 1"

by (induct x) (simp_all add: rec_pred_def)

lemma minus_swap_lemma [simp]: 

  "rec_eval rec_minus_swap [x, y] = y - x"

by (induct x) (simp_all add: rec_minus_swap_def)

lemma minus_lemma [simp]: 

  "rec_eval rec_minus [x, y] = x - y"

by (simp add: rec_minus_def)

lemma sign_lemma [simp]: 

  "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"

by (simp add: rec_sign_def)

lemma not_lemma [simp]: 

  "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"

by (simp add: rec_not_def)

lemma eq_lemma [simp]: 

  "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"

by (simp add: rec_eq_def)

lemma noteq_lemma [simp]: 

  "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"

by (simp add: rec_noteq_def)

lemma conj_lemma [simp]: 

  "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"

by (simp add: rec_conj_def)

lemma disj_lemma [simp]: 

  "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"

by (simp add: rec_disj_def)

lemma imp_lemma [simp]: 

  "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"

by (simp add: rec_imp_def)

lemma less_lemma [simp]: 

  "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"

by (simp add: rec_less_def)

lemma le_lemma [simp]: 

  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"

by(simp add: rec_le_def)

lemma sigma1_lemma [simp]: 

  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"

by (induct x) (simp_all add: rec_sigma1_def)

lemma sigma2_lemma [simp]: 

  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"

by (induct x) (simp_all add: rec_sigma2_def)

lemma accum1_lemma [simp]: 

  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"

by (induct x) (simp_all add: rec_accum1_def)

lemma accum2_lemma [simp]: 

  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"

by (induct x) (simp_all add: rec_accum2_def)

lemma ex1_lemma [simp]:

 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"

by (simp add: rec_ex1_def)

lemma ex2_lemma [simp]:

 "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"

by (simp add: rec_ex2_def)

lemma all1_lemma [simp]:

 "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"

by (simp add: rec_all1_def)

lemma all2_lemma [simp]:

 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"

by (simp add: rec_all2_def)

lemma dvd_alt_def:

  "(x dvd y) = (\<exists>k\<le>y. y = x * (k::nat))"

apply(auto simp add: dvd_def)

apply(case_tac x)

apply(auto)

done

lemma dvd_swap_lemma [simp]:

  "rec_eval rec_dvd_swap [x, y] = (if y dvd x then 1 else 0)"

unfolding dvd_alt_def

by (auto simp add: rec_dvd_swap_def)

lemma dvd_lemma [simp]:

  "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"

by (simp add: rec_dvd_def)

definition 

  "rec_prime = 

    (let conj1 = CN rec_less [constn 1, id 1 0] in

     let disj  = CN rec_disj [CN rec_eq [id 2 0, constn 1], rec_eq] in

     let imp   = CN rec_imp [rec_dvd, disj] in

     let conj2 = CN (rec_all1 imp) [id 1 0, id 1 0] in

     CN rec_conj [conj1, conj2])"

lemma prime_alt_def:

  fixes p::nat

  shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"

apply(auto simp add: prime_nat_def dvd_def)

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)

lemma prime_lemma [simp]: 

  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"

by (simp add: rec_prime_def Let_def prime_alt_def)

fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 

                        if (setx = {}) then (Suc x) else (Min setx))"

definition

  "rec_minr f = rec_sigma (rec_accum (CN rec_not [f]))"

lemma minr_lemma [simp]:

shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y"

apply(simp only: rec_minr_def)

apply(simp only: sigma_lemma)

apply(simp only: accum_lemma)

apply(subst rec_eval.simps)

apply(simp only: map.simps nth)

apply(simp only: Minr.simps Let_def)

apply(auto simp del: not_lemma)

apply(simp)

apply(simp only: not_lemma sign_lemma)

apply(rule sym)

apply(rule Min_eqI)

apply(auto)[1]

apply(simp)

apply(subst setsum_cut_off_le[where m="ya"])

apply(simp)

apply(simp)

apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)

apply(rule setsum_one_less)

apply(default)

apply(rule impI)

apply(rule setprod_one_le)

apply(auto split: if_splits)[1]

apply(simp)

apply(rule conjI)

apply(subst setsum_cut_off_le[where m="xa"])

apply(simp)

apply(simp)

apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)

apply(rule le_trans)

apply(rule setsum_one_less)

apply(default)

apply(rule impI)

apply(rule setprod_one_le)

apply(auto split: if_splits)[1]

apply(simp)

apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])")

defer

apply metis

apply(erule exE)

apply(subgoal_tac "l \<le> x")

defer

apply (metis not_leE not_less_Least order_trans)

apply(subst setsum_least_eq)

apply(rotate_tac 3)

apply(assumption)

prefer 3

apply (metis LeastI_ex)

apply(auto)[1]

apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])")

prefer 2

apply(auto)[1]

apply(rotate_tac 5)

apply(drule not_less_Least)

apply(auto)[1]

apply(auto)

by (metis (mono_tags) LeastI_ex)

(*

lemma prime_alt_iff:

  fixes x::nat

  shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u < x. \<forall>v < x. x \<noteq> u * v)"

unfolding prime_nat_simp dvd_def

apply(auto)

by (smt n_less_m_mult_n nat_mult_commute)

lemma prime_alt2_iff:

  fixes x::nat

  shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u \<le> x - 1. \<forall>v \<le> x - 1. x \<noteq> u * v)"

unfolding prime_alt_iff

sorry

*)

definition

  "rec_prime = CN rec_conj 

                 [CN rec_less [constn 1, id 1 0], 

                  CN (rec_all (CN (rec_all2 (CN rec_noteq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) 

                                   [CN rec_pred [id 2 1], id 2 0, id 2 1]))

                      [CN rec_pred [id 1 0], id 1 0]]"

lemma prime_lemma [simp]: 

  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"

apply(rule trans)

apply(simp add: rec_prime_def)

apply(simp only: prime_nat_def dvd_def)

apply(auto)

apply(drule_tac x="m" in spec)

apply(auto)

apply(case_tac m)

apply(auto)