# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1367420217 -3600
# Node ID 8dba6ae39bf0c6740bf66ba8c8ac05e452f16ed6
# Parent  ac32cc069e3082ae4853ef12e5b266d9252fe0ab
started with UF

diff -r ac32cc069e30 -r 8dba6ae39bf0 thys/Recs.thy
--- 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