tm: comparison thys/UF.thy

equal deleted inserted replaced

-:6b6d71d14e75
+:06a6db387cd2
 [Cn (vl - 1) (constn 0) [id (vl - 1) 0]]))
 (Cn (Suc vl) rec_add [id (Suc vl) vl,
 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"}.
+section {* Correctness of various recursive functions *}
-*}
-lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] =  x + y"
+lemma add_lemma: "rec_exec rec_add [x, y] =  x + y"
 by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-text {*
+lemma mult_lemma: "rec_exec rec_mult [x, y] = x * y"
-Correctness of @{text "rec_mult"}.
-*}
-lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"
 by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-text {*
+lemma pred_lemma: "rec_exec rec_pred [x] =  x - 1"
-Correctness of @{text "rec_pred"}.
-*}
-lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] =  x - 1"
 by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
-text {*
+lemma minus_lemma: "rec_exec rec_minus [x, y] = x - y"
-Correctness of @{text "rec_minus"}.
-*}
-lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"
 by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
-text {*
+lemma sg_lemma: "rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
-Correctness of @{text "rec_sg"}.
-*}
-lemma sg_lemma: "\<And> x. 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 {*
+lemma less_lemma: "rec_exec rec_less [x, y] = (if x < y then 1 else 0)"
-Correctness of @{text "rec_less"}.
-*}
-lemma less_lemma: "\<And> x y. 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 {*
+lemma not_lemma: "rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
-Correctness of @{text "rec_not"}.
-*}
-lemma not_lemma:
-"\<And> x. 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)
-text {*
+lemma eq_lemma: "rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-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 {*
+lemma conj_lemma: "rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
-Correctness of @{text "rec_conj"}.
-*}
-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 {*
+lemma disj_lemma: "rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
-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)
+declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
-text {*
+minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
-@{text "primrec recf n"} is true iff
+less_lemma[simp] not_lemma[simp] eq_lemma[simp]
-@{text "recf"} is a primitive recursive function
+conj_lemma[simp] disj_lemma[simp]
-with arity @{text "n"}.
-*}
+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)" |
 prime_s[intro]:  "primerec s (Suc 0)" |
 prime_id[intro!]: "\<lbrakk>n < m\<rbrakk> \<Longrightarrow> primerec (id m n) m" |
 inductive_cases prime_s_reverse[elim]: "primerec s n"
 inductive_cases prime_id_reverse[elim]: "primerec (id m n) k"
 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
 the recursive function @{text "rec_sigma"}.
 *}
 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]) +
+else (Sigma g (butlast xs @ [last xs - 1]) + g xs)) "
-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)
+thus "((g, butlast xs @ [last xs - 1]), g, xs) \<in> measure (\<lambda>(f, xs). last xs)"
-\<in> measure (\<lambda>(f, xs). last xs)"
 by auto
 qed
 declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]
 arity.simps[simp del] Sigma.simps[simp del]
 rec_sigma.simps[simp del]
 lemma [simp]: "arity z = 1"
 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)
 lemma rec_pr_0_simp_rewrite_single_param: "
 rec_exec (Pr n f g) [0] = rec_exec f []"
+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])])"
 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])])"
-by(simp add: rec_exec.simps)
 lemma rec_pr_Suc_simp_rewrite_single_param:
-"rec_exec (Pr n f g) ([Suc x]) =
+"rec_exec (Pr n f g) ([Suc x]) = rec_exec g ([x] @ [rec_exec (Pr n f g) ([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:
 "Sigma f [0] = f [0]"
 by(simp add: Sigma.simps)
 qed
 text {*
 The correctness of @{text "rec_Minr"}.
 *}
-lemma Minr_lemma: "
+lemma Minr_lemma:
-\<lbrakk>primerec rf (Suc (length xs))\<rbrakk>
+assumes h: "primerec rf (Suc (length xs))"
-\<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) =
+shows "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) 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)))
 rec_not [Cn (Suc (Suc (length xs))) rf
 (get_fstn_args (Suc (Suc (length xs))) (length xs) @
 [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]) =
+ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) 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)
 apply(simp add: h)
 done
 text {*
 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 {*
 Definition of @{text "Max[Rr]"} on page 77 of Boolos's book.
 *}
 apply(rule_tac prime_cn, auto)
 apply(case_tac i, auto)
 done
 lemma [simp]:
-"length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =
+"length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) = ys @ [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)
 apply(case_tac "ys = []", simp_all)
 done

changeset 237	06a6db387cd2
parent 229	d8e6f0798e23
child 238	6ea1062da89a