tm: thys/Rec_Def.thy@aea02b5a58d2 (annotated)

163 67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	1	theory Rec_Def
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	imports Main
2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	begin
2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
229 d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	5	datatype recf = z
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	6	\| s
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	7	\| id nat nat
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	8	\| Cn nat recf "recf list"
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	9	\| Pr nat recf recf
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	10	\| Mn nat recf
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11
248 aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	12	definition pred_of_nl :: "nat list \<Rightarrow> nat list"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	13	where
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	14	"pred_of_nl xs = butlast xs @ [last xs - 1]"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	15
229 d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	16	function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	17	where
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	18	"rec_exec z xs = 0" \|
248 aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	19	"rec_exec s xs = (Suc (xs ! 0))" \|
229 d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	20	"rec_exec (id m n) xs = (xs ! n)" \|
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	21	"rec_exec (Cn n f gs) xs =
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	22	rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" \|
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	23	"rec_exec (Pr n f g) xs =
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	24	(if last xs = 0 then rec_exec f (butlast xs)
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	25	else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" \|
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	26	"rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	27	by pat_completeness auto
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	28
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	29	termination
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	30	apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	31	apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	32	done
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33
248 aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	34	inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	35	where
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	36	termi_z: "terminate z [n]"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	37	\| termi_s: "terminate s [n]"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	38	\| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	39	\| termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs);
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	40	\<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	41	\| termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	42	terminate f xs;
229 d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	43	length xs = n\<rbrakk>
248 aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	44	\<Longrightarrow> terminate (Pr n f g) (xs @ [x])"
aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	45	\| termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]);
229 d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	46	rec_exec f (xs @ [r]) = 0;
248 aea02b5a58d2 repaired old files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 240 diff changeset	47	\<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48
2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49
2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 02 May 2013 12:49:33 +0100
changeset 248	aea02b5a58d2
parent 240	696081f445c2
child 288	a9003e6d0463
permissions	-rwxr-xr-x