--- a/thys/UF.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/UF.thy Mon Apr 22 08:26:16 2013 +0100
@@ -152,93 +152,58 @@
Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1)
@ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"
-text {*
- @{text "rec_exec"} is the interpreter function for
- reursive functions. The function is defined such that
- it always returns meaningful results for primitive recursive
- functions.
- *}
declare rec_exec.simps[simp del] constn.simps[simp del]
-text {*
- Correctness of @{text "rec_add"}.
- *}
-lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] = x + y"
+
+section {* Correctness of various recursive functions *}
+
+
+lemma add_lemma: "rec_exec rec_add [x, y] = x + y"
by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-text {*
- Correctness of @{text "rec_mult"}.
- *}
-lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"
+lemma mult_lemma: "rec_exec rec_mult [x, y] = x * y"
by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-text {*
- Correctness of @{text "rec_pred"}.
- *}
-lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] = x - 1"
+lemma pred_lemma: "rec_exec rec_pred [x] = x - 1"
by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
-text {*
- Correctness of @{text "rec_minus"}.
- *}
-lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"
+lemma minus_lemma: "rec_exec rec_minus [x, y] = x - y"
by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
-text {*
- Correctness of @{text "rec_sg"}.
- *}
-lemma sg_lemma: "\<And> x. rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
+lemma sg_lemma: "rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)
-text {*
- Correctness of @{text "constn"}.
- *}
lemma constn_lemma: "rec_exec (constn n) [x] = n"
by(induct n, auto simp: rec_exec.simps constn.simps)
-text {*
- Correctness of @{text "rec_less"}.
- *}
-lemma less_lemma: "\<And> x y. rec_exec rec_less [x, y] =
- (if x < y then 1 else 0)"
+lemma less_lemma: "rec_exec rec_less [x, y] = (if x < y then 1 else 0)"
by(induct_tac y, auto simp: rec_exec.simps
rec_less_def minus_lemma sg_lemma)
-text {*
- Correctness of @{text "rec_not"}.
- *}
-lemma not_lemma:
- "\<And> x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
+lemma not_lemma: "rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
by(induct_tac x, auto simp: rec_exec.simps rec_not_def
constn_lemma minus_lemma)
+lemma eq_lemma: "rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
+by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
+
+lemma conj_lemma: "rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
+
+lemma disj_lemma: "rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
+
+declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
+ minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
+ less_lemma[simp] not_lemma[simp] eq_lemma[simp]
+ conj_lemma[simp] disj_lemma[simp]
+
text {*
- Correctness of @{text "rec_eq"}.
- *}
-lemma eq_lemma: "\<And> x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-
-text {*
- Correctness of @{text "rec_conj"}.
+ @{text "primrec recf n"} is true iff @{text "recf"} is a primitive
+ recursive function with arity @{text "n"}.
*}
-lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0
- else 1)"
-by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
-text {*
- Correctness of @{text "rec_disj"}.
- *}
-lemma disj_lemma: "\<And> x y. rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0
- else 1)"
-by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
-
-
-text {*
- @{text "primrec recf n"} is true iff
- @{text "recf"} is a primitive recursive function
- with arity @{text "n"}.
- *}
+
inductive primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
where
prime_z[intro]: "primerec z (Suc 0)" |
@@ -259,10 +224,7 @@
inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m"
inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m"
-declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
- minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
- less_lemma[simp] not_lemma[simp] eq_lemma[simp]
- conj_lemma[simp] disj_lemma[simp]
+
text {*
@{text "Sigma"} is the logical specification of
@@ -271,17 +233,16 @@
function Sigma :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"
where
"Sigma g xs = (if last xs = 0 then g xs
- else (Sigma g (butlast xs @ [last xs - 1]) +
- g xs)) "
+ else (Sigma g (butlast xs @ [last xs - 1]) + g xs)) "
by pat_completeness auto
+
termination
proof
show "wf (measure (\<lambda> (f, xs). last xs))" by auto
next
fix g xs
assume "last (xs::nat list) \<noteq> 0"
- thus "((g, butlast xs @ [last xs - 1]), g, xs)
- \<in> measure (\<lambda>(f, xs). last xs)"
+ thus "((g, butlast xs @ [last xs - 1]), g, xs) \<in> measure (\<lambda>(f, xs). last xs)"
by auto
qed
@@ -290,25 +251,22 @@
rec_sigma.simps[simp del]
lemma [simp]: "arity z = 1"
- by(simp add: arity.simps)
+ by(simp add: arity.simps)
lemma rec_pr_0_simp_rewrite: "
rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_exec.simps)
+ by(simp add: rec_exec.simps)
lemma rec_pr_0_simp_rewrite_single_param: "
rec_exec (Pr n f g) [0] = rec_exec f []"
-by(simp add: rec_exec.simps)
+ by(simp add: rec_exec.simps)
lemma rec_pr_Suc_simp_rewrite:
- "rec_exec (Pr n f g) (xs @ [Suc x]) =
- rec_exec g (xs @ [x] @
- [rec_exec (Pr n f g) (xs @ [x])])"
+ "rec_exec (Pr n f g) (xs @ [Suc x]) = rec_exec g (xs @ [x] @ [rec_exec (Pr n f g) (xs @ [x])])"
by(simp add: rec_exec.simps)
lemma rec_pr_Suc_simp_rewrite_single_param:
- "rec_exec (Pr n f g) ([Suc x]) =
- rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
+ "rec_exec (Pr n f g) ([Suc x]) = rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
by(simp add: rec_exec.simps)
lemma Sigma_0_simp_rewrite_single_param:
@@ -748,10 +706,9 @@
text {*
The correctness of @{text "rec_Minr"}.
*}
-lemma Minr_lemma: "
- \<lbrakk>primerec rf (Suc (length xs))\<rbrakk>
- \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) =
- Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+lemma Minr_lemma:
+ assumes h: "primerec rf (Suc (length xs))"
+ shows "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
proof -
let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
let ?rf = "(Cn (Suc (Suc (length xs)))
@@ -760,15 +717,13 @@
[recf.id (Suc (Suc (length xs)))
(Suc ((length xs)))])])"
let ?rq = "(rec_all ?rt ?rf)"
- assume h: "primerec rf (Suc (length xs))"
have h1: "primerec ?rq (Suc (length xs))"
apply(rule_tac primerec_all_iff)
apply(auto simp: h nth_append)+
done
moreover have "arity rf = Suc (length xs)"
using h by auto
- ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) =
- Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+ ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def
sigma_lemma all_lemma)
apply(rule_tac sigma_minr_lemma)
@@ -789,7 +744,7 @@
The correctness of @{text "rec_le"}.
*}
lemma le_lemma:
- "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+ "rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
by(auto simp: rec_le_def rec_exec.simps)
text {*
@@ -857,8 +812,7 @@
done
lemma [simp]:
- "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =
- ys @ [ys ! n]"
+ "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) = ys @ [ys ! n]"
apply(simp)
apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)
apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)