292
293e9c6f22e1
Added myself to the comments at the start of all files
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
1 |
(* Title: thys/Rec_Def.thy
|
293e9c6f22e1
Added myself to the comments at the start of all files
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
2 |
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
|
293e9c6f22e1
Added myself to the comments at the start of all files
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
3 |
Modifications: Sebastiaan Joosten
|
293e9c6f22e1
Added myself to the comments at the start of all files
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
4 |
*)
|
293e9c6f22e1
Added myself to the comments at the start of all files
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
5 |
|
163
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
theory Rec_Def
|
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
imports Main
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
|
229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
datatype recf = z
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
| s
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
| id nat nat
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
| Cn nat recf "recf list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
| Pr nat recf recf
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
| Mn nat recf
|
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
definition pred_of_nl :: "nat list \<Rightarrow> nat list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
"pred_of_nl xs = butlast xs @ [last xs - 1]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
|
229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
"rec_exec z xs = 0" |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
"rec_exec s xs = (Suc (xs ! 0))" |
|
229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
"rec_exec (id m n) xs = (xs ! n)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
"rec_exec (Cn n f gs) xs =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
"rec_exec (Pr n f g) xs =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
(if last xs = 0 then rec_exec f (butlast xs)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
"rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
by pat_completeness auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
termination
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")
|
288
a9003e6d0463
Up to date for Isabelle 2018. Gave names to simp rules in UF and UTM
Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
diff
changeset
|
36 |
apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 size_list_estimation'[THEN trans_le_add1])
|
229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
done
|
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
termi_z: "terminate z [n]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
| termi_s: "terminate s [n]"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
| termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
\<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
| termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
terminate f xs;
|
229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
length xs = n\<rbrakk>
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
\<Longrightarrow> terminate (Pr n f g) (xs @ [x])"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
| termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]);
|
229
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
rec_exec f (xs @ [r]) = 0;
|
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
\<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
|
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
end |