tm: thys/Rec_Def.thy@696081f445c2 (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
229 d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	12	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	13	where
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	14	"rec_exec z xs = 0" \|
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	15	"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	16	"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	17	"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	18	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	19	"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	20	(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	21	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	22	"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	23	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	24
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	25	termination
d8e6f0798e23 much simplified version of Recursive.thy Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	26	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	27	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	28	done
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	30	inductive
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	31	terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	32	where
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	33	termi_z: "terminates z [n]"
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	34	\| termi_s: "terminates s [n]"
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	35	\| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	36	\| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_exec g xs) gs);
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	37	\<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	38	\| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	39	terminates 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	40	length xs = n\<rbrakk>
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	41	\<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	42	\| termi_mn: "\<lbrakk>length xs = n; terminates 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	43	rec_exec f (xs @ [r]) = 0;
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	44	\<forall> i < r. terminates f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45
2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	47	inductive_cases terminates_pr_reverse: "terminates (Pr n f g) xs"
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 229 diff changeset	48
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	49	inductive_cases terminates_z_reverse[elim!]: "terminates z xs"
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 229 diff changeset	50
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	51	inductive_cases terminates_s_reverse[elim!]: "terminates s xs"
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 229 diff changeset	52
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	53	inductive_cases terminates_id_reverse[elim!]: "terminates (id m n) xs"
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 229 diff changeset	54
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	55	inductive_cases terminates_cn_reverse[elim!]: "terminates (Cn n f gs) xs"
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 229 diff changeset	56
240 696081f445c2 added improved Recsursive function theory (not yet finished) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	57	inductive_cases terminates_mn_reverse[elim!]:"terminates (Mn n f) xs"
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 229 diff changeset	58
70 2363eb91d9fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 25 Apr 2013 21:37:05 +0100
changeset 240	696081f445c2
parent 237	06a6db387cd2
child 248	aea02b5a58d2
permissions	-rwxr-xr-x