# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369478785 -3600
# Node ID fa3c214559b0dabd7d71057f234586e968d61850
# Parent  bc2df9620f26f02d8a0facec46b9bc539d1ca3be
finished recusive version of the UF

diff -r bc2df9620f26 -r fa3c214559b0 thys2/Recs.thy
--- a/thys2/Recs.thy	Sat May 25 01:33:31 2013 +0100
+++ b/thys2/Recs.thy	Sat May 25 11:46:25 2013 +0100
@@ -310,6 +310,11 @@
 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]])"
 
+definition 
+  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
+                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
+
+
 text {* Bounded quantifiers for one and two arguments *}
 
 definition
@@ -319,6 +324,17 @@
   "rec_all2 f = CN rec_sign [rec_accum2 f]"
 
 definition
+  "rec_all3 f = CN rec_sign [rec_accum3 f]"
+
+definition
+  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
+                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
+
+definition
+  "rec_all2_less f = (let f' = CN rec_disj [CN rec_eq [Id 4 0, Id 4 1], CN f [Id 4 0, Id 4 2, Id 4 3]] 
+                      in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
+
+definition
   "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
 
 definition
@@ -452,6 +468,10 @@
   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 accum3_lemma [simp]: 
+  shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
+by (induct x) (simp_all add: rec_accum3_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)
@@ -468,6 +488,22 @@
  "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 all3_lemma [simp]:
+ "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
+by (simp add: rec_all3_def)
+
+lemma all1_less_lemma [simp]:
+  "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)"
+apply(auto simp add: Let_def rec_all1_less_def)
+apply (metis nat_less_le)+
+done
+
+lemma all2_less_lemma [simp]:
+  "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+apply(auto simp add: Let_def rec_all2_less_def)
+apply(metis nat_less_le)+
+done
+
 
 lemma dvd_alt_def:
   fixes x y k:: nat
diff -r bc2df9620f26 -r fa3c214559b0 thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Sat May 25 01:33:31 2013 +0100
+++ b/thys2/UF_Rec.thy	Sat May 25 11:46:25 2013 +0100
@@ -162,6 +162,11 @@
   "Steps cf p 0  = cf"
 | "Steps cf p (Suc n) = Steps (Step cf p) p n"
 
+lemma Step_Steps_comm:
+  "Step (Steps cf p n) p = Steps (Step cf p) p n"
+by (induct n arbitrary: cf) (simp_all only: Steps.simps)
+
+
 text {*
   Decoding tapes into binary or stroke numbers.
 *}
@@ -310,6 +315,8 @@
   where
   "Halt m cf = (LEAST k. Stop m cf k)"
 
+thm Steps.simps
+
 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
@@ -567,139 +574,101 @@
   "rec_eval rec_right [cf] = Right cf"
 by (simp add: rec_right_def)
 
-(* HERE *)
+definition 
+  "rec_step = (let left = CN rec_left [Id 2 0] in
+               let right = CN rec_right [Id 2 0] in
+               let state = CN rec_state [Id 2 0] in
+               let read = CN rec_read [right] in
+               let action = CN rec_action [Id 2 1, state, read] in
+               let newstate = CN rec_newstate [Id 2 1, state, read] in
+               let newleft = CN rec_newleft [left, right, action] in
+               let newright = CN rec_newright [left, right, action] 
+               in CN rec_conf [newstate, newleft, newright])" 
 
-definition 
-  "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
-                  let left = CN rec_left [Id 2 1] in
-                  let right = CN rec_right [Id 2 1] in
-                  let stat = CN rec_stat [Id 2 1] in
-                  let one = CN rec_newleft [left, right, act] in
-                  let two = CN rec_newstat [Id 2 0, stat, right] in
-                  let three = CN rec_newright [left, right, act]
-                  in CN rec_trpl [one, two, three])" 
-
-definition 
-  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
-                 (CN rec_newconf [Id 4 2 , Id 4 1])"
+lemma step_lemma [simp]:
+  "rec_eval rec_step [cf, m] = Step cf m"
+by (simp add: Let_def rec_step_def)
 
 definition 
-  "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in
-               let disj2 = CN rec_noteq [rec_left, constn 0] in
-               let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in
-               let disj3 = CN rec_noteq [rec_right, rhs] in
-               let disj4 = CN rec_eq [rec_right, constn 0] in
-               CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"
-
-definition 
-  "rec_nostop = CN rec_nstd [rec_conf]"
+  "rec_steps = PR (Id 3 0)
+                  (CN rec_step [Id 4 1, Id 4 3])"
 
-definition 
-  "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
-
-definition 
-  "rec_halt = MN rec_nostop" 
-
-definition 
-  "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
-
+lemma steps_lemma [simp]:
+  "rec_eval rec_steps [n, cf, p] = Steps cf p n"
+by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
 
 
-section {* Correctness Proofs for Recursive Functions *}
-
-lemma entry_lemma [simp]:
-  "rec_eval rec_entry [sr, i] = Entry sr i"
-by(simp add: rec_entry_def)
+definition
+  "rec_stknum = CN rec_minus 
+                  [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
+                   CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"
 
-lemma listsum2_lemma [simp]: 
-  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
-by (induct n) (simp_all)
-
-lemma strt'_lemma [simp]:
-  "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"
-by (induct n) (simp_all add: Let_def)
+lemma stknum_lemma [simp]:
+  "rec_eval rec_stknum [z] = Stknum z"
+by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
 
-lemma map_suc:
-  "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"
-proof -
-  have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)
-  then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp
-  also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp
-  also have "... = map Suc xs" by (simp add: map_nth)
-  finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .
-qed
+definition
+  "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
+                    let cond1 = CN rec_le [constn 1, Id 2 0] in
+                    let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
+                    let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
+                    let cond3 = CN (rec_all2_less 
+                                     (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) 
+                                [bound2, Id 2 0, Id 2 1] in
+                    CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])"
 
-lemma strt_lemma [simp]: 
-  "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"
-by (simp add: comp_def map_suc[symmetric])
-
-lemma scan_lemma [simp]: 
-  "rec_eval rec_scan [r] = r mod 2"
-by(simp add: rec_scan_def)
+definition
+  "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
+                   in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"
 
-lemma newleft_lemma [simp]:
-  "rec_eval rec_newleft [p, r, a] = Newleft p r a"
-by (simp add: rec_newleft_def Let_def)
-
-lemma newright_lemma [simp]:
-  "rec_eval rec_newright [p, r, a] = Newright p r a"
-by (simp add: rec_newright_def Let_def)
+lemma left_std_lemma [simp]:
+  "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
+by (simp add: Let_def rec_left_std_def left_std_def)
 
-lemma actn_lemma [simp]:
-  "rec_eval rec_actn [m, q, r] = Actn m q r"
-by (simp add: rec_actn_def)
-
-lemma newstat_lemma [simp]: 
-  "rec_eval rec_newstat [m, q, r] = Newstat m q r"
-by (simp add: rec_newstat_def)
+lemma right_std_lemma [simp]:
+  "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
+by (simp add: Let_def rec_right_std_def right_std_def)
 
-lemma trpl_lemma [simp]: 
-  "rec_eval rec_trpl [p, q, r] = Trpl p q r"
-apply(simp)
-apply (simp add: rec_trpl_def)
+definition
+  "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
+                          CN rec_right_std [CN rec_right [Id 1 0]]]"
 
-lemma left_lemma [simp]:
-  "rec_eval rec_left [c] = Left c" 
-by(simp add: rec_left_def)
+definition 
+  "rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]"
 
-lemma right_lemma [simp]:
-  "rec_eval rec_right [c] = Right c" 
-by(simp add: rec_right_def)
+definition 
+  "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
+               CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"
 
-lemma stat_lemma [simp]:
-  "rec_eval rec_stat [c] = Stat c" 
-by(simp add: rec_stat_def)
-
-lemma newconf_lemma [simp]: 
-  "rec_eval rec_newconf [m, c] = Newconf m c"
-by (simp add: rec_newconf_def Let_def)
-
-lemma conf_lemma [simp]: 
-  "rec_eval rec_conf [k, m, r] = Conf k m r"
-by(induct k) (simp_all add: rec_conf_def)
+lemma std_lemma [simp]:
+  "rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
+by (simp add: rec_std_def)
 
-lemma nstd_lemma [simp]:
-  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
-by(simp add: rec_nstd_def)
+lemma final_lemma [simp]:
+  "rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
+by (simp add: rec_final_def)
 
-lemma nostop_lemma [simp]:
-  "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" 
-by (simp add: rec_nostop_def)
+lemma stop_lemma [simp]:
+  "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
+by (simp add: Let_def rec_stop_def)
 
-lemma value_lemma [simp]:
-  "rec_eval rec_value [x] = Value x"
-by (simp add: rec_value_def)
+definition
+  "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
 
 lemma halt_lemma [simp]:
-  "rec_eval rec_halt [m, r] = Halt m r"
-by (simp add: rec_halt_def)
+  "rec_eval rec_halt [m, cf] = Halt m cf"
+by (simp add: rec_halt_def del: Stop.simps)
+
+definition 
+  "rec_uf = CN rec_pred 
+              [CN rec_stknum 
+                  [CN rec_right 
+                     [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
 
 lemma uf_lemma [simp]:
-  "rec_eval rec_uf [m, r] = UF m r"
+  "rec_eval rec_uf [m, cf] = UF m cf"
 by (simp add: rec_uf_def)
 
 
-
-
 end