--- a/src/HOL/List.thy Wed Aug 17 11:15:23 2005 +0200
+++ b/src/HOL/List.thy Wed Aug 17 11:44:02 2005 +0200
@@ -1243,13 +1243,13 @@
"list_all2 P xs ys ==> length xs = length ys"
by (simp add: list_all2_def)
-lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
+lemma list_all2_Nil [iff,code]: "list_all2 P [] ys = (ys = [])"
by (simp add: list_all2_def)
lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs = [])"
by (simp add: list_all2_def)
-lemma list_all2_Cons [iff]:
+lemma list_all2_Cons [iff,code]:
"list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
by (auto simp add: list_all2_def)
@@ -1413,8 +1413,8 @@
subsubsection {* @{text upto} *}
-lemma upt_rec: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
--- {* Does not terminate! *}
+lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
+-- {* simp does not terminate! *}
by (induct j) auto
lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
@@ -1934,10 +1934,8 @@
use @{prop"x : set xs"} instead --- it is much easier to reason about.
The same is true for @{const list_all} and @{const list_ex}: write
@{text"\<forall>x\<in>set xs"} and @{text"\<exists>x\<in>set xs"} instead because the HOL
-quantifiers are aleady known to the automatic provers. For the purpose
-of generating executable code use the theorems @{text mem_iff},
-@{text list_all_iff} and @{text list_ex_iff} to get rid off or
-introduce the combinators.
+quantifiers are aleady known to the automatic provers. In fact, the declarations in the Code subsection make sure that @{text"\<in>"}, @{text"\<forall>x\<in>set xs"}
+and @{text"\<exists>x\<in>set xs"} are implemented efficiently.
The functions @{const itrev}, @{const filtermap} and @{const
map_filter} are just there to generate efficient code. Do not use them
@@ -1977,32 +1975,27 @@
text{* Defaults for generating efficient code for some standard functions. *}
-lemma [code]: "rev xs = itrev xs []"
+lemmas in_set_code[code unfold] = mem_iff[symmetric, THEN eq_reflection]
+
+lemma rev_code[code unfold]: "rev xs == itrev xs []"
by simp
-declare upt_rec[code]
-
-lemma [code]: "distinct (x#xs) = (~(x mem xs) \<and> distinct xs)"
+lemma distinct_Cons_mem[code]: "distinct (x#xs) = (~(x mem xs) \<and> distinct xs)"
by (simp add:mem_iff)
-lemma [code]:
+lemma remdups_Cons_mem[code]:
"remdups (x#xs) = (if x mem xs then remdups xs else x # remdups xs)"
by (simp add:mem_iff)
-lemma [code]:
- "list_all2 P xs ys =
- (length xs = length ys \<and> (list_all (%(x, y). P x y) (zip xs ys)))"
-by (simp add:list_all2_def list_all_iff)
-
-lemma [code]: "list_inter (a#as) bs =
+lemma list_inter_Cons_mem[code]: "list_inter (a#as) bs =
(if a mem bs then a#(list_inter as bs) else list_inter as bs)"
by(simp add:mem_iff)
-(* If you want to replace bounded quantifiers over lists by list_ex/all:
-
-declare list_ex_iff[symmetric, THEN eq_reflection, code unfold]
-declare list_all_iff[symmetric, THEN eq_reflection, code unfold]
-*)
+text{* For implementing bounded quantifiers over lists by
+@{const list_ex}/@{const list_all}: *}
+
+lemmas list_bex_code[code unfold] = list_ex_iff[symmetric, THEN eq_reflection]
+lemmas list_ball_code[code unfold] = list_all_iff[symmetric, THEN eq_reflection]
subsubsection{* Inductive definition for membership *}
@@ -2136,7 +2129,7 @@
text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
This ordering does \emph{not} preserve well-foundedness.
- Author: N. Voelker, March 2005 *}
+ Author: N. Voelker, March 2005. *}
constdefs
lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
--- a/src/HOL/MicroJava/BV/Effect.thy Wed Aug 17 11:15:23 2005 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy Wed Aug 17 11:44:02 2005 +0200
@@ -401,10 +401,6 @@
by (auto simp add: eff_def xcpt_eff_def norm_eff_def)
-text {* some helpers to make the specification directly executable: *}
-declare list_all2_Nil [code]
-declare list_all2_Cons [code]
-
lemma xcpt_app_lemma [code]:
"xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
by (simp add: list_all_iff)
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Wed Aug 17 11:15:23 2005 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Wed Aug 17 11:44:02 2005 +0200
@@ -6,7 +6,9 @@
header {* \isaheader{Completeness of the LBV} *}
-theory LBVComplete imports LBVSpec Typing_Framework begin
+theory LBVComplete
+imports LBVSpec Typing_Framework
+begin
constdefs
is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool"
@@ -17,19 +19,11 @@
"make_cert step phi B \<equiv>
map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
-constdefs
- list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
- "list_ex P xs \<equiv> \<exists>x \<in> set xs. P x"
-
-lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def)
-lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def)
-
lemma [code]:
"is_target step phi pc' =
list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
- apply (simp add: list_ex_def is_target_def mem_iff)
- apply force
- done
+by (force simp: list_ex_iff is_target_def mem_iff)
+
locale (open) lbvc = lbv +
fixes phi :: "'a list" ("\<phi>")
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Wed Aug 17 11:15:23 2005 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Wed Aug 17 11:44:02 2005 +0200
@@ -6,7 +6,9 @@
header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
-theory LBVJVM imports LBVCorrect LBVComplete Typing_Framework_JVM begin
+theory LBVJVM
+imports LBVCorrect LBVComplete Typing_Framework_JVM
+begin
types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> state list"
@@ -65,7 +67,7 @@
lemma check_certD:
"check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states G mxs mxr)"
apply (unfold cert_ok_def check_cert_def check_types_def)
- apply (auto simp add: list_all_ball)
+ apply (auto simp add: list_all_iff)
done
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Aug 17 11:15:23 2005 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Aug 17 11:44:02 2005 +0200
@@ -42,15 +42,11 @@
"list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
by (unfold list_all'_def) (simp add: list_all'_rec)
-lemma list_all_ball:
- "list_all P xs = (\<forall>x \<in> set xs. P x)"
- by (induct xs) auto
-
lemma [code]:
"check_bounded ins et =
(list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and>
list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
- by (simp add: list_all_ball check_bounded_def)
+ by (simp add: list_all_iff check_bounded_def)
section {* Connecting JVM and Framework *}