
diff -r 5317c92ff2a7 -r bd320b5365e2 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Tue Jan 29 13:00:51 2013 +0000
+++ b/thys/uncomputable.thy	Tue Jan 29 16:37:38 2013 +0000
@@ -9,14 +9,6 @@
 imports Main turing_hoare
 begin
 
-declare tm_comp.simps [simp del] 
-declare adjust.simps[simp del] 
-declare shift.simps[simp del]
-declare tm_wf.simps[simp del]
-declare step.simps[simp del]
-declare steps.simps[simp del]
-
-
 lemma numeral:
   shows "1 = Suc 0"
   and "2 = Suc 1"
@@ -92,9 +84,11 @@
 using assms
 unfolding tcopy_begin_def
 apply(case_tac cf)
-apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
-apply(case_tac "hd c", auto simp: inv_begin.simps)
-apply(case_tac c, simp_all)
+apply(auto simp: numeral split: if_splits)
+apply(case_tac "hd c")
+apply(auto)
+apply(case_tac c)
+apply(simp_all)
 done
 
 lemma inv_begin_steps: 
@@ -102,48 +96,34 @@
   and "x > 0"
   shows "inv_begin x (steps0 cf tcopy_begin stp)"
 apply(induct stp)
-apply(simp add: steps.simps assms)
-apply(auto simp: step_red)
+apply(simp add: assms)
+apply(auto simp del: steps.simps)
 apply(rule_tac inv_begin_step)
 apply(simp_all add: assms)
 done
 
-fun begin_state :: "config \<Rightarrow> nat"
+fun measure_begin_state :: "config \<Rightarrow> nat"
   where
-  "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
+  "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 
-fun begin_step :: "config \<Rightarrow> nat"
+fun measure_begin_step :: "config \<Rightarrow> nat"
   where
-  "begin_step (s, l, r) = 
+  "measure_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 begin_measure :: "config \<Rightarrow> nat \<times> nat"
-  where
-  "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 begin_LE :: "(config \<times> config) set"
-  where
-  "begin_LE \<equiv> (inv_image lex_pair begin_measure)"
+definition
+  "begin_LE = measures [measure_begin_state, measure_begin_step]"
 
 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 begin_LE"
-by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
-
 lemma begin_halt: 
   "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)"
 proof(rule_tac LE = begin_LE in halt_lemma) 
-  show "wf begin_LE" by(simp add: wf_begin_le)
+  show "wf begin_LE" unfolding begin_LE_def by (auto) 
 next
   assume h: "0 < x"
   show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
@@ -164,10 +144,10 @@
     ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
       steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
       using a 
-    proof(simp del: inv_begin.simps)
+    proof(simp del: inv_begin.simps step.simps steps.simps)
       assume "inv_begin x (s, l, r)" "0 < s"
       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(auto simp: begin_LE_def step.simps tcopy_begin_def numeral split: if_splits)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
@@ -194,6 +174,13 @@
     done
 qed
 
+declare tm_comp.simps [simp del] 
+declare adjust.simps[simp del] 
+declare shift.simps[simp del]
+declare tm_wf.simps[simp del]
+declare step.simps[simp del]
+declare steps.simps[simp del]
+
 
 (* tcopy_loop *)
 
@@ -477,25 +464,13 @@
                           else if s = 6 then length l
                           else 0)"
 
-definition lex_triple :: 
- "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
-  where
-  "lex_triple \<equiv> less_than <*lex*> lex_pair"
-
-lemma wf_lex_triple: "wf lex_triple"
-  by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
-
-fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
-  where
-  "loop_measure c = 
-   (loop_stage c, loop_state c, loop_step c)"
-
 definition loop_LE :: "(config \<times> config) set"
   where
-   "loop_LE \<equiv> (inv_image lex_triple loop_measure)"
+   "loop_LE = measures [loop_stage, loop_state, loop_step]"
 
 lemma wf_loop_le: "wf loop_LE"
-by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
+unfolding loop_LE_def
+by (auto)
 
 lemma [simp]: "inv_loop2 x ([], b) = False"
 by (auto simp: inv_loop2.simps)
@@ -615,8 +590,7 @@
     hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE"
       using h 
       apply(case_tac r', case_tac [2] a)
-      apply(auto simp: inv_loop.simps step.simps tcopy_loop_def 
-                       numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits)
+      apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral loop_LE_def split: if_splits)
       done
     thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), 
           steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
@@ -833,17 +807,13 @@
           else if s = 3 then 0
           else 0)"
 
-fun end_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"
-  where
-  "end_measure c = 
-   (end_state c, end_stage c, end_step c)"
-
 definition end_LE :: "(config \<times> config) set"
   where
-   "end_LE \<equiv> (inv_image lex_triple end_measure)"
+   "end_LE = measures [end_state, end_stage, end_step]"
 
 lemma wf_end_le: "wf end_LE"
-by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple)
+unfolding end_LE_def
+by (auto)
 
 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
 by (auto simp: inv_end5.simps inv_end5_loop.simps)
@@ -870,8 +840,7 @@
       done
     hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
       apply(case_tac r', case_tac [2] a)
-      apply(auto simp: inv_end.simps step.simps tcopy_end_def 
-                       numeral end_LE_def lex_triple_def lex_pair_def split: if_splits)
+      apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_def split: if_splits)
       done
     thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 
       steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"




