--- a/thys/Recs.thy Tue Apr 30 12:53:11 2013 +0100
+++ b/thys/Recs.thy Wed May 01 15:56:57 2013 +0100
@@ -2,6 +2,18 @@
imports Main Fact "~~/src/HOL/Number_Theory/Primes"
begin
+(*
+ some definitions from
+
+ A Course in Formal Languages, Automata and Groups
+ I M Chiswell
+
+ and
+
+ Lecture on undecidability
+ Michael M. Wolf
+*)
+
lemma if_zero_one [simp]:
"(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
"(0::nat) < (if P then 1 else 0) = P"
@@ -166,6 +178,9 @@
abbreviation
"PR f g \<equiv> Pr (arity f) f g"
+abbreviation
+ "MN f \<equiv> Mn (arity f - 1) f"
+
fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
where
"rec_eval Z xs = 0"
@@ -302,7 +317,7 @@
definition
"rec_ex2 f = CN rec_sign [rec_sigma2 f]"
-text {* Dvd *}
+text {* Dvd, Quotient, Reminder *}
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]"
@@ -310,7 +325,15 @@
definition
"rec_dvd = rec_swap rec_dvd_swap"
+definition
+ "rec_quo = (let lhs = CN S [Id 3 0] in
+ let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
+ let cond = CN rec_noteq [lhs, rhs] in
+ let ifz = CN rec_ifz [cond, CN S [Id 3 1], Id 3 1]
+ in PR Z ifz)"
+definition
+ "rec_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
section {* Correctness of Recursive Functions *}
@@ -445,6 +468,59 @@
by (simp add: rec_dvd_def)
+fun Quo where
+ "Quo x 0 = 0"
+| "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)"
+
+lemma Quo0:
+ shows "Quo 0 y = 0"
+apply(induct y)
+apply(auto)
+done
+
+lemma Quo1:
+ "x * (Quo x y) \<le> y"
+by (induct y) (simp_all)
+
+lemma Quo2:
+ "b * (Quo b a) + a mod b = a"
+by (induct a) (auto simp add: mod_Suc)
+
+lemma Quo3:
+ "n * (Quo n m) = m - m mod n"
+using Quo2[of n m] by (auto)
+
+lemma Quo4:
+ assumes h: "0 < x"
+ shows "y < x + x * Quo x y"
+proof -
+ have "x - (y mod x) > 0" using mod_less_divisor assms by auto
+ then have "y < y + (x - (y mod x))" by simp
+ then have "y < x + (y - (y mod x))" by simp
+ then show "y < x + x * (Quo x y)" by (simp add: Quo3)
+qed
+
+lemma Quo_div:
+ shows "Quo x y = y div x"
+apply(case_tac "x = 0")
+apply(simp add: Quo0)
+apply(subst split_div_lemma[symmetric])
+apply(auto intro: Quo1 Quo4)
+done
+
+lemma Quo_rec_quo:
+ shows "rec_eval rec_quo [y, x] = Quo x y"
+by (induct y) (simp_all add: rec_quo_def)
+
+lemma quo_lemma [simp]:
+ shows "rec_eval rec_quo [y, x] = y div x"
+by (simp add: Quo_div Quo_rec_quo)
+
+lemma rem_lemma [simp]:
+ shows "rec_eval rec_rem [y, x] = y mod x"
+by (simp add: rec_rem_def mod_div_equality' nat_mult_commute)
+
+
section {* Prime Numbers *}
lemma prime_alt_def:
@@ -518,6 +594,9 @@
"rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
by (induct x) (simp_all add: rec_max2_def)
+
+section {* Discrete Logarithms *}
+
definition
"rec_lg =
(let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in
@@ -528,11 +607,42 @@
definition
"Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)"
-lemma lg_lemma:
+lemma lg_lemma [simp]:
"rec_eval rec_lg [x, y] = Lg x y"
by (simp add: rec_lg_def Lg_def Let_def)
+section {* Universal Function *}
+
+text {*
+ @{text "Nstd c"} returns true if the configuration coded
+ by @{text "c"} is not a stardard final configuration.
+ *}
+fun Nstd :: "nat \<Rightarrow> bool"
+ where
+ "Nstd c = (stat c \<noteq> 0 \<or> left c \<noteq> 0 \<or>
+ right c \<noteq> 2 ^ (Lg (Suc (right c)) 2) - 1 \<or>
+ right c = 0)"
+
+
+definition
+ "value x = (Lg (Suc x) 2) - 1"
+
+definition
+ "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
+
+lemma value_lemma [simp]:
+ "rec_eval rec_value [x] = value x"
+by (simp add: rec_value_def value_def)
+
+definition
+ where
+ "rec_UF = CN rec_valu [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]"
+
+end
+
+
+(*
@@ -1019,5 +1129,4 @@
apply(subst Min_le_iff)
apply(auto)
done
-
-end
\ No newline at end of file
+ *)
\ No newline at end of file