9 | Succ |
9 | Succ |
10 | Id nat nat --"Projection" |
10 | Id nat nat --"Projection" |
11 | Cn nat recf "recf list" --"Composition" |
11 | Cn nat recf "recf list" --"Composition" |
12 | Pr nat recf recf --"Primitive recursion" |
12 | Pr nat recf recf --"Primitive recursion" |
13 | Mn nat recf --"Minimisation" |
13 | Mn nat recf --"Minimisation" |
|
14 |
|
15 primrec hd0 :: "nat list => nat" where |
|
16 "hd0 [] = 0" | |
|
17 "hd0 (m # ms) = m" |
|
18 |
|
19 fun |
|
20 primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool" |
|
21 where |
|
22 "primerec Zero m = (m = 1)" | |
|
23 "primerec Succ m = (m = 1)" | |
|
24 "primerec (Id i j) m = (j < i \<and> i = m) " | |
|
25 "primerec (Cn n f gs) m = (primerec f (length gs) \<and> (\<forall>g \<in> set gs. primerec g m))" | |
|
26 "primerec (Pr n f g) m = (0 < m \<and> primerec f (m - 1) \<and> primerec g (m + 2))" | |
|
27 "primerec (Mn n f) m = False" |
|
28 |
|
29 function (domintros) eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
|
30 where |
|
31 "eval Zero ns = 0" | |
|
32 "eval Succ ns = (Suc (hd0 ns))" | |
|
33 "eval (Id m n) ns = (ns ! n)" | |
|
34 "eval (Cn n f gs) ns = |
|
35 (let ys = (map (\<lambda>a. eval a ns) gs) in eval f ys)" | |
|
36 "eval (Pr n f g) [] = eval f []" | |
|
37 "eval (Pr n f g) (0#ns) = eval f ns" | |
|
38 "eval (Pr n f g) (Suc m#ns) = eval g (eval (Pr n f g) (m # ns) # m # ns)" | |
|
39 "eval (Mn n f) ns = (LEAST x. eval f (x # ns) = 0)" |
|
40 by pat_completeness auto |
|
41 |
|
42 thm eval.psimps |
|
43 thm eval.pinduct |
|
44 thm eval.domintros |
|
45 |
|
46 lemma |
|
47 "primerec f (length ns) \<Longrightarrow> eval_dom (f, (ns::nat list))" |
|
48 apply(induct arbitrary: ns rule: primerec.induct) |
|
49 apply(auto intro: eval.domintros) |
|
50 ???? |
|
51 |
|
52 |
|
53 |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 |
|
59 |
|
60 |
|
61 |
|
62 |
14 |
63 |
15 partial_function (option) |
64 partial_function (option) |
16 eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option" |
65 eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option" |
17 where |
66 where |
18 "eval f i gs ns = (case (i, gs, f, ns) of |
67 "eval f i gs ns = (case (i, gs, f, ns) of |
35 | (_, _) \<Rightarrow> None)" |
84 | (_, _) \<Rightarrow> None)" |
36 |
85 |
37 abbreviation |
86 abbreviation |
38 "eval0 f ns \<equiv> eval f None None ns" |
87 "eval0 f ns \<equiv> eval f None None ns" |
39 |
88 |
40 lemma "eval0 Zero [n] = Some 0" |
89 abbreviation |
41 apply(subst eval.simps) |
90 "eval1 f ns \<equiv> if (\<exists>x. eval0 f ns = Some x) then the (eval0 f ns) else undefined" |
|
91 |
|
92 lemma "eval1 Zero [n] = 0" |
|
93 apply(subst (1 2) eval.simps) |
42 apply(simp) |
94 apply(simp) |
43 done |
95 done |
44 |
96 |
45 lemma "eval0 Succ [n] = Some (n + 1)" |
97 lemma "eval1 Succ [n] = n + 1" |
46 apply(subst eval.simps) |
98 apply(subst (1 2) eval.simps) |
47 apply(simp) |
99 apply(simp) |
48 done |
100 done |
49 |
101 |
50 lemma "eval0 (Id i j) ns = (if (j < i) then Some (ns ! j) else None)" |
102 lemma "j < i \<Longrightarrow> eval1 (Id i j) ns = ns ! j" |
51 apply(subst eval.simps) |
103 apply(subst (1 2) eval.simps) |
52 apply(simp) |
104 apply(simp) |
53 done |
105 done |
54 |
106 |
55 lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns" |
107 lemma "eval1 (Pr n f g) (0 # ns) = eval1 f ns" |
56 apply(subst eval.simps) |
108 apply(subst (1 2) eval.simps) |
57 apply(simp) |
109 apply(simp) |
58 done |
110 done |
59 |
111 |
60 lemma "eval0 (Pr n f g) (Suc k # ns) = |
112 lemma "eval1 (Pr n f g) (Suc k # ns) = eval1 g ((eval1 (Pr n f g) (k # ns)) # k # ns)" |
61 do { r \<leftarrow> eval0 (Pr n f g) (k # ns); eval0 g (r # k # ns) }" |
113 apply(subst (1 2) eval.simps) |
62 apply(subst eval.simps) |
|
63 apply(simp) |
114 apply(simp) |
|
115 apply(auto) |
64 done |
116 done |
65 |
117 |
66 |
118 |
67 |
119 |
68 |
120 |