47 "primerec f (length ns) \<Longrightarrow> eval_dom (f, (ns::nat list))" |
48 "primerec f (length ns) \<Longrightarrow> eval_dom (f, (ns::nat list))" |
48 apply(induct arbitrary: ns rule: primerec.induct) |
49 apply(induct arbitrary: ns rule: primerec.induct) |
49 apply(auto intro: eval.domintros) |
50 apply(auto intro: eval.domintros) |
50 ???? |
51 ???? |
51 |
52 |
52 |
53 *) |
53 |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 |
|
59 |
|
60 |
|
61 |
|
62 |
|
63 |
54 |
64 partial_function (option) |
55 partial_function (option) |
65 eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option" |
56 eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option" |
66 where |
57 where |
67 "eval f i gs ns = (case (i, gs, f, ns) of |
58 "eval f i gs ns = (case (i, gs, f, ns) of |
84 | (_, _) \<Rightarrow> None)" |
75 | (_, _) \<Rightarrow> None)" |
85 |
76 |
86 abbreviation |
77 abbreviation |
87 "eval0 f ns \<equiv> eval f None None ns" |
78 "eval0 f ns \<equiv> eval f None None ns" |
88 |
79 |
89 abbreviation |
80 lemma "eval0 Zero [n] = Some 0" |
90 "eval1 f ns \<equiv> if (\<exists>x. eval0 f ns = Some x) then the (eval0 f ns) else undefined" |
81 apply(subst eval.simps) |
91 |
|
92 lemma "eval1 Zero [n] = 0" |
|
93 apply(subst (1 2) eval.simps) |
|
94 apply(simp) |
82 apply(simp) |
95 done |
83 done |
96 |
84 |
97 lemma "eval1 Succ [n] = n + 1" |
85 lemma "eval0 Succ [n] = Some (n + 1)" |
98 apply(subst (1 2) eval.simps) |
86 apply(subst eval.simps) |
99 apply(simp) |
87 apply(simp) |
100 done |
88 done |
101 |
89 |
102 lemma "j < i \<Longrightarrow> eval1 (Id i j) ns = ns ! j" |
90 lemma "j < i \<Longrightarrow> eval0 (Id i j) ns = Some (ns ! j)" |
103 apply(subst (1 2) eval.simps) |
91 apply(subst eval.simps) |
104 apply(simp) |
92 apply(simp) |
105 done |
93 done |
106 |
94 |
107 lemma "eval1 (Pr n f g) (0 # ns) = eval1 f ns" |
95 lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns" |
108 apply(subst (1 2) eval.simps) |
96 apply(subst eval.simps) |
109 apply(simp) |
97 apply(simp) |
110 done |
98 done |
111 |
99 |
112 lemma "eval1 (Pr n f g) (Suc k # ns) = eval1 g ((eval1 (Pr n f g) (k # ns)) # k # ns)" |
100 lemma "eval0 (Pr n f g) (Suc k # ns) = |
113 apply(subst (1 2) eval.simps) |
101 do { r \<leftarrow> eval0 (Pr n f g) (k # ns); eval0 g (r # k # ns) }" |
|
102 apply(subst eval.simps) |
114 apply(simp) |
103 apply(simp) |
115 apply(auto) |
|
116 done |
104 done |
117 |
105 |
118 |
106 |
119 |
107 |
|
108 lemma |
|
109 "eval0 (Mn n f) ns = Some (LEAST r. eval0 f (r # ns) = Some 0)" |
|
110 apply(subst eval.simps) |
|
111 apply(simp) |
|
112 apply(subst eval.simps) |
|
113 apply(simp) |
|
114 done |
120 |
115 |
121 end |
116 end |