# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1401447889 -3600
# Node ID e04123f4bacc84f908948c9feb6a5192ed88d4eb
# Parent  087d826328521ac507faa9e86ac896b664939984
soem more work

diff -r 087d82632852 -r e04123f4bacc thys/FMap.thy
--- a/thys/FMap.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/FMap.thy	Fri May 30 12:04:49 2014 +0100
@@ -15,6 +15,8 @@
 
 lift_definition lookup :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value option" is "(\<lambda> x. x)" ..
 
+notation lookup (infixl "$" 999)
+
 abbreviation the_lookup (infix "f!" 55)
   where "m f! x \<equiv> the (lookup m x)"
 
@@ -23,7 +25,7 @@
 lemma fempty_fdom[simp]: "fdom f\<emptyset> = {}"
   by (transfer, auto)
 
-lemma fdomIff: "(a : fdom m) = (lookup m a \<noteq> None)"
+lemma fdomIff: "a \<in> fdom m \<longleftrightarrow> lookup m a \<noteq> None"
  by (transfer, auto)
 
 lemma lookup_not_fdom: "x \<notin> fdom m \<Longrightarrow> lookup m x = None"
@@ -345,14 +347,44 @@
       by simp
   qed
 qed
+
+fun alookup
+where
+  "alookup k [] = None"
+| "alookup k ((x, y) # xs) = (if (k = x) then Some y else alookup k xs)"
+
   
-definition fmapdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list"
+definition fdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list"
 where
-  "fmapdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)"
+  "fdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)"
+
+lemma
+  "fdom f = set (fdom_to_list f)"
+unfolding fdom_to_list_def
+apply(subgoal_tac "finite (fdom f)")
+apply(drule finite_sorted_distinct_unique)
+apply(drule theI')
+apply(simp_all)
+done
+
+
 
 definition fmap_to_alist :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> ('a \<times> 'b) list"
 where
-  "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fmapdom_to_list f]"
+  "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fdom_to_list f]"
+
+lemma
+  shows "(f $ k) = alookup k (fmap_to_alist f)" 
+thm finite_dom_map_of
 
+apply(transfer)
+apply(simp add: fmap_to_alist_def)
+
+thm lookup_def
+
+apply(rule theI2)
+apply(induct k xs\<equiv>"fmap_to_alist f" rule: alookup.induct)
+apply(simp add: fmap_to_alist_def fmapdom_to_list_def)
+thm theD1
 
 end
diff -r 087d82632852 -r e04123f4bacc thys/Hoare_tm3.thy
--- a/thys/Hoare_tm3.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/Hoare_tm3.thy	Fri May 30 12:04:49 2014 +0100
@@ -47,26 +47,27 @@
 
 section {* Operational Semantics of TM *}
 
-datatype taction = W0 | W1 | L | R
-
-type_synonym tstate = nat
-
+datatype action = W0 | W1 | L | R
+
+type_synonym state = nat
+
+(* FIXME: I think Block should be changed to cell *)
 datatype Block = Oc | Bk
 
 (* the successor state when tape symbol is Bk or Oc, respectively *)
-type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
+type_synonym tm_inst = "(action \<times> state) \<times> (action \<times> state)"
 
 (* - number of faults (nat)
-   - TM program (nat \<rightharpoonup> tm_inst)
+   - TM program (nat f\<rightharpoonup> tm_inst)
    - current state (nat)
    - position of head (int)
-   - tape (int \<rightharpoonup> Block)
+   - tape (int f\<rightharpoonup> Block)
 *)
 type_synonym tconf = "nat \<times> (nat f\<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int f\<rightharpoonup> Block)"
 
 (* updates the position/tape according to an action *)
 fun 
-  next_tape :: "taction \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block))"
+  next_tape :: "action \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block))"
 where 
   "next_tape W0 (pos, m) = (pos, m(pos f\<mapsto> Bk))" |
   "next_tape W1 (pos, m) = (pos, m(pos f\<mapsto> Oc))" |
diff -r 087d82632852 -r e04123f4bacc thys/Recs.thy
--- a/thys/Recs.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/Recs.thy	Fri May 30 12:04:49 2014 +0100
@@ -222,9 +222,9 @@
 section {* Arithmetic Functions *}
 
 text {*
-  @{text "constn n"} is the recursive function which computes 
-  natural number @{text "n"}.
-*}
+  @{text "constn n"} is the recursive function which generates
+  the natural number @{text "n"}. *}
+
 fun constn :: "nat \<Rightarrow> recf"
   where
   "constn 0 = Z"  |
@@ -254,6 +254,7 @@
 definition 
   "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
+
 lemma constn_lemma [simp]: 
   "rec_eval (constn n) xs = n"
 by (induct n) (simp_all)
@@ -283,7 +284,7 @@
 by (simp add: rec_fact_def)
 
 lemma pred_lemma [simp]: 
-  "rec_eval rec_pred [x] =  x - 1"
+  "rec_eval rec_pred [x] = x - 1"
 by (induct x) (simp_all add: rec_pred_def)
 
 lemma minus_lemma [simp]: 
@@ -291,7 +292,7 @@
 by (induct y) (simp_all add: rec_minus_def)
 
 
-section {* Logical functions *}
+section {* Logical Functions *}
 
 text {* 
   The @{text "sign"} function returns 1 when the input argument 
@@ -321,9 +322,9 @@
 definition 
   "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
 
-text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
-  y otherwise;  @{term "rec_if [z, x, y]"} returns x if z is *not*
-  zero, y otherwise *}
+text {* @{term "rec_ifz [z, x, y]"} returns @{text x} if @{text z} is zero, and
+  @{text y} otherwise;  @{term "rec_if [z, x, y]"} returns @{text x} if @{text z} 
+  is *not* zero, and @{text y} otherwise. *}
 
 definition 
   "rec_ifz = PR (Id 2 0) (Id 4 3)"
@@ -368,11 +369,12 @@
   "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
 by (simp add: rec_if_def)
 
-section {* Less and Le Relations *}
+
+section {* The Less and Less-Equal Relations *}
 
 text {*
   @{text "rec_less"} compares two arguments and returns @{text "1"} if
-  the first is less than the second; otherwise returns @{text "0"}. *}
+  the first is less than the second; otherwise it returns @{text "0"}. *}
 
 definition 
   "rec_less = CN rec_sign [rec_swap rec_minus]"
@@ -385,8 +387,8 @@
 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)
+  "rec_eval rec_le [x, y] = (if x \<le> y then 1 else 0)"
+by (simp add: rec_le_def)
 
 
 section {* Summation and Product Functions *}
@@ -435,6 +437,11 @@
 
 section {* Bounded Quantifiers *}
 
+text {* Instead of defining quantifiers taking an aritrary 
+  list of arguments, we define the simpler quantifiers taking
+  one, two and three extra arguments besides the argument
+  that is quantified over. *}
+
 definition
   "rec_all1 f = CN rec_sign [rec_accum1 f]"
 
@@ -484,7 +491,7 @@
 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)+
+apply(metis nat_less_le)+
 done
 
 lemma all2_less_lemma [simp]:
@@ -493,60 +500,61 @@
 apply(metis nat_less_le)+
 done
 
-section {* Quotients *}
+
+section {* Natural Number Division *}
 
 definition
-  "rec_quo = (let lhs = CN S [Id 3 0] in
+  "rec_div = (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_eq [lhs, rhs] in
               let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
               in PR Z if_stmt)"
 
-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)"
+fun Div where
+  "Div x 0 = 0"
+| "Div x (Suc y) = (if (Suc y = x * (Suc (Div x y))) then Suc (Div x y) else Div x y)"
 
-lemma Quo0:
-  shows "Quo 0 y = 0"
+lemma Div0:
+  shows "Div 0 y = 0"
 by (induct y) (auto)
 
-lemma Quo1:
-  "x * (Quo x y) \<le> y"
+lemma Div1:
+  "x * (Div 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 Div2: 
+  "x * (Div x y) + y mod x = y"
+by (induct y) (auto simp add: mod_Suc)
 
-lemma Quo3:
-  "n * (Quo n m) = m - m mod n"
-using Quo2[of n m] by (auto)
+lemma Div3:
+  "x * (Div x y) = y - y mod x"
+using Div2[of x y] by (auto)
 
-lemma Quo4:
+lemma Div4:
   assumes h: "0 < x"
-  shows "y < x + x * Quo x y"
+  shows "y < x + x * Div 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) 
+  then show "y < x + x * (Div x y)" by (simp add: Div3) 
 qed
 
-lemma Quo_div: 
-  shows "Quo x y = y div x"
+lemma Div_div: 
+  shows "Div x y = y div x"
 apply(case_tac "x = 0")
-apply(simp add: Quo0)
+apply(simp add: Div0)
 apply(subst split_div_lemma[symmetric])
-apply(auto intro: Quo1 Quo4)
+apply(auto intro: Div1 Div4)
 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 Div_rec_div:
+  shows "rec_eval rec_div [y, x] = Div x y"
+by (induct y) (simp_all add: rec_div_def)
 
-lemma quo_lemma [simp]:
-  shows "rec_eval rec_quo [y, x] = y div x"
-by (simp add: Quo_div Quo_rec_quo)
+lemma div_lemma [simp]:
+  shows "rec_eval rec_div [y, x] = y div x"
+by (simp add: Div_div Div_rec_div)
 
 
 section {* Iteration *}
@@ -569,6 +577,9 @@
 
 section {* Bounded Maximisation *}
 
+text {* Computes the greatest number below a bound @{text n}
+  such that a predicate holds. If such a maximum does not exist,
+  then @{text 0} is returned. *}
 
 fun BMax_rec where
   "BMax_rec R 0 = 0"
@@ -594,7 +605,7 @@
 by metis
 
 lemma BMax_rec_eq3:
-  "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
+  "BMax_rec R x = Max (Set.filter R {..x} \<union> {0})"
 by (simp add: BMax_rec_eq2 Set.filter_def)
 
 definition 
@@ -612,12 +623,11 @@
 by (induct x) (simp_all add: rec_max2_def)
 
 
-section {* Encodings using Cantor's pairing function *}
+section {* Encodings using Cantor's Pairing Function *}
 
-text {*
-  We use Cantor's pairing function from Nat_Bijection.
-  However, we need to prove that the formulation of the
-  decoding function there is recursive. For this we first 
+text {* We use Cantor's pairing function from the theory 
+  Nat_Bijection. However, we need to prove that the formulation 
+  of the decoding function there is recursive. For this we first 
   prove that we can extract the maximal triangle number 
   using @{term prod_decode}.
 *}
@@ -699,7 +709,7 @@
 
 
 definition 
-  "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]"
+  "rec_triangle = CN rec_div [CN rec_mult [Id 1 0, S], constn 2]"
 
 definition
   "rec_max_triangle = 
@@ -716,7 +726,7 @@
 by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) 
 
 
-text {* Encodings for Products *}
+text {* Encodings for Pairs of Natural Numbers *}
 
 definition
   "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
@@ -740,7 +750,7 @@
 by (simp add: rec_penc_def prod_encode_def)
 
 
-text {* Encodings of Lists *}
+text {* Encodings of Lists of Natural Numbers *}
 
 fun 
   lenc :: "nat list \<Rightarrow> nat" 
@@ -772,8 +782,7 @@
   "length xs \<le> lenc xs"  
 by (induct xs) (simp_all add: prod_encode_def)
 
-
-text {* Membership for the List Encoding *}
+text {* The membership predicate for an encoded list. *}
 
 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "within z 0 = (0 < z)"
@@ -795,7 +804,7 @@
 apply(simp_all)
 done
 
-text {* Length of Encoded Lists *}
+text {* The length of an encoded list. *}
 
 lemma enclen_length [simp]:
   "enclen (lenc xs) = length xs"
diff -r 087d82632852 -r e04123f4bacc thys/UF_Rec.thy
--- a/thys/UF_Rec.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/UF_Rec.thy	Fri May 30 12:04:49 2014 +0100
@@ -1,110 +1,60 @@
 theory UF_Rec
-imports Recs Hoare_tm2
+imports Recs Hoare_tm3
 begin
 
 section {* Coding of Turing Machines and Tapes*}
 
 
-fun actnum :: "taction \<Rightarrow> nat"
+fun actenc :: "action \<Rightarrow> nat"
   where
-  "actnum W0 = 0"
-| "actnum W1 = 1"
-| "actnum L  = 2"
-| "actnum R  = 3"
-
-fun cellnum :: "Block \<Rightarrow> nat" where
-  "cellnum Bk = 0"
-| "cellnum Oc = 1"
-
-
-(* coding programs *)
-
-thm finfun_comp_def
-term finfun_rec
+  "actenc W0 = 0"
+| "actenc W1 = 1"
+| "actenc L  = 2"
+| "actenc R  = 3"
 
-definition code_finfun :: "(nat \<Rightarrow>f tm_inst option) \<Rightarrow> (nat \<times> tm_inst option) list"
-  where
-  "code_finfun f = ([(x, f $ x). x \<leftarrow> finfun_to_list f])"
-
-fun lookup where
-  "lookup [] c = None"
-| "lookup ((a, b)#xs) c = (if a = c then b else lookup xs c)"
-
-lemma
-  "f $ n = lookup (code_finfun f) n"
-apply(induct f rule: finfun_weak_induct)
-apply(simp add: code_finfun_def)
-apply(simp add: finfun_to_list_const)
-thm finfun_rec_const
-apply(finfun_rec_const)
-apply(simp add: finfun_rec_def)
-apply(auto)
-thm finfun_rec_unique
-apply(rule finfun_rec_unique)
+fun cellenc :: "Block \<Rightarrow> nat" where
+  "cellenc Bk = 0"
+| "cellenc Oc = 1"
 
 
 text {* Coding tapes *}
 
-fun code_tp :: "() \<Rightarrow> nat list"
-  where
-  "code_tp [] = []"
-| "code_tp (c # tp) = (cellnum c) # code_tp tp"
+definition 
+  "intenc i \<equiv> (if (0 \<le> i) then penc 0 (nat i) else penc 1 (nat (-i)))" 
 
-fun Code_tp where
-  "Code_tp tp = lenc (code_tp tp)"
-
-lemma code_tp_append [simp]:
-  "code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2"
-by(induct tp1) (simp_all)
+definition
+  "intdec n \<equiv> (if (0 = pdec1 n) then (int (pdec2 n)) else -(int (pdec2 n)))"
 
-lemma code_tp_length [simp]:
-  "length (code_tp tp) = length tp"
-by (induct tp) (simp_all)
+definition 
+  tapeenc :: "(int f\<rightharpoonup> Block) \<Rightarrow> nat"
+where
+  "tapeenc tp = lenc (map (\<lambda>(x, y). penc (intenc x) (cellenc y)) (fmap_to_alist tp))"
 
-lemma code_tp_nth [simp]:
-  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"
-apply(induct n arbitrary: tp) 
-apply(simp_all)
-apply(case_tac [!] tp)
-apply(simp_all)
-done
-
-lemma code_tp_replicate [simp]:
-  "code_tp (c \<up> n) = (cellnum c) \<up> n"
-by(induct n) (simp_all)
+fun 
+  instenc :: "tm_inst \<Rightarrow> nat"
+where
+  "instenc ((a1, s1), (a2, s2)) = lenc [actenc a1, s1, actenc a2, s2]"
 
-text {* Coding Configurations and TMs *}
+definition 
+  progenc :: "(nat f\<rightharpoonup> tm_inst) \<Rightarrow> nat"
+where
+  "progenc p = lenc (map (\<lambda>(x, y). penc x (instenc y)) (fmap_to_alist p))"
 
-fun Code_conf where
-  "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
+text {* Coding Configurations of TMs *}
 
-fun code_instr :: "instr \<Rightarrow> nat" where
-  "code_instr i = penc (actnum (fst i)) (snd i)"
-  
-fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where
-  "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"
+fun confenc where
+  "confenc (faults, prog, s, pos, tp) = lenc [faults, progenc prog, s, intenc pos, tapeenc tp]"
 
-fun code_tprog :: "tprog \<Rightarrow> nat list"
+section {* A Universal Function in HOL *}
+
+fun Step :: "nat \<Rightarrow> nat"
   where
-  "code_tprog [] =  []"
-| "code_tprog (i # tm) = Code_instr i # code_tprog tm"
-
-lemma code_tprog_length [simp]:
-  "length (code_tprog tp) = length tp"
-by (induct tp) (simp_all)
-
-lemma code_tprog_nth [simp]:
-  "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)"
-by (induct tp arbitrary: n) (simp_all add: nth_Cons')
-
-fun Code_tprog :: "tprog \<Rightarrow> nat"
-  where 
-  "Code_tprog tm = lenc (code_tprog tm)"
+  "Step cf = Conf (Newstate m (State cf) (Read (Right cf)), 
+                     Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
+                     Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"
 
 
-section {* An Universal Function in HOL *}
-
-text {* Reading and writing the encoded tape *}
+text {* Reading and Writing the Encoded Tape *}
 
 fun Read where
   "Read tp = ldec tp 0"