--- a/thys/uncomputable.thy	Mon Jan 28 02:38:57 2013 +0000
+++ b/thys/uncomputable.thy	Tue Jan 29 12:37:06 2013 +0000
@@ -103,47 +103,47 @@
 apply(rule_tac inv_begin_step, simp_all)
 done
 
-fun init_state :: "config \<Rightarrow> nat"
+fun begin_state :: "config \<Rightarrow> nat"
   where
-  "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
+  "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 
-fun init_step :: "config \<Rightarrow> nat"
+fun begin_step :: "config \<Rightarrow> nat"
   where
-  "init_step (s, l, r) = 
+  "begin_step (s, l, r) = 
         (if s = 2 then length r else
          if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
          if s = 4 then length l 
          else 0)"
 
-fun init_measure :: "config \<Rightarrow> nat \<times> nat"
+fun begin_measure :: "config \<Rightarrow> nat \<times> nat"
   where
-  "init_measure c = (init_state c, init_step c)"
+  "begin_measure c = (begin_state c, begin_step c)"
 
 
 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
   where
   "lex_pair \<equiv> less_than <*lex*> less_than"
 
-definition init_LE :: "(config \<times> config) set"
+definition begin_LE :: "(config \<times> config) set"
   where
-  "init_LE \<equiv> (inv_image lex_pair init_measure)"
+  "begin_LE \<equiv> (inv_image lex_pair begin_measure)"
 
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
 by (case_tac r, auto, case_tac a, auto)
 
 
-lemma wf_begin_le: "wf init_LE"
-by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
+lemma wf_begin_le: "wf begin_LE"
+by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
 
-lemma init_halt: 
+lemma begin_halt: 
   "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
-proof(rule_tac LE = init_LE in halt_lemma) 
-  show "wf init_LE" by(simp add: wf_begin_le)
+proof(rule_tac LE = begin_LE in halt_lemma) 
+  show "wf begin_LE" by(simp add: wf_begin_le)
 next
   assume h: "0 < x"
   show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
         (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-            steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+            steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
   proof(rule_tac allI, rule_tac impI)
     fix n
     assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
@@ -157,25 +157,25 @@
     moreover hence "inv_begin x (s, l, r)" 
       using c b by simp
     ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-      steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+      steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
       using a 
     proof(simp del: inv_begin.simps)
       assume "inv_begin x (s, l, r)" "0 < s"
-      thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> init_LE"
-        apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
+      thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
+        apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
   qed
 qed
     
-lemma init_correct: 
+lemma begin_correct: 
   "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
 proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x" "inv_begin1 x (l, r)"
   hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
-    by (rule_tac init_halt)    
+    by (rule_tac begin_halt)    
   then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
   moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
     apply(rule_tac inv_begin_steps)
@@ -913,7 +913,7 @@
   shows "{inv_begin1 x} tcopy {inv_end0 x}"
 proof -
   have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
-    by (metis assms init_correct) 
+    by (metis assms begin_correct) 
   moreover
   have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
     by (metis assms loop_correct) 
@@ -970,10 +970,10 @@
   "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
 
 (* invariants of dither *)
-abbreviation
+abbreviation (input)
   "dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
 
-abbreviation
+abbreviation (input)
   "dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
 
 lemma dither_loops_aux: 
@@ -1083,7 +1083,7 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
+  def P3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1136,7 +1136,7 @@
   (* invariants *)
   def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
   def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
-  def Q3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
+  def Q3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
 
   (*
   {P1} tcopy {P2}  {P2} H {Q3}