diff -r ac3309722536 -r 696081f445c2 thys/Recs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Recs.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -0,0 +1,549 @@
+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)
+apply(case_tac nat)
+apply(auto)
+apply(case_tac k)
+apply(auto)
+apply(case_tac nat)
+apply(auto)
+done
+
+lemma if_zero [simp]:
+  "(0::nat) < (if P then 1 else 0) = P"
+by (simp)
+
+lemma if_cong:
+  "P = Q \<Longrightarrow> (if P then 1 else (0::nat)) = (if Q then 1 else 0)"
+by simp
+
+
+
+
+end
\ No newline at end of file