equal
deleted
inserted
replaced
69 "read r == if (r = []) then Bk else hd r" |
69 "read r == if (r = []) then Bk else hd r" |
70 |
70 |
71 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config" |
71 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config" |
72 where |
72 where |
73 "step (s, l, r) (p, off) = |
73 "step (s, l, r) (p, off) = |
74 (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" |
74 (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" |
75 |
75 |
76 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
76 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
77 where |
77 where |
78 "steps c p 0 = c" | |
78 "steps c p 0 = c" | |
79 "steps c p (Suc n) = steps (step c p) p n" |
79 "steps c p (Suc n) = steps (step c p) p n" |
91 where |
91 where |
92 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
92 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
93 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 |
93 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 |
94 + off \<and> s \<ge> off))" |
94 + off \<and> s \<ge> off))" |
95 |
95 |
96 (* FIXME: needed? *) |
|
97 lemma halt_lemma: |
96 lemma halt_lemma: |
98 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
97 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
99 by (metis wf_iff_no_infinite_down_chain) |
98 by (metis wf_iff_no_infinite_down_chain) |
100 |
99 |
101 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
100 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |