# HG changeset patch
# User nipkow
# Date 1124271842 -7200
# Node ID 603f23d71ada7e5a0c3c2bc45e8115fe1369af83
# Parent  f708a31fa8bb62fc2506fdb2d9d0369ea8e924e8
small mods to code lemmas

diff -r f708a31fa8bb -r 603f23d71ada src/HOL/List.thy
--- 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" 
diff -r f708a31fa8bb -r 603f23d71ada src/HOL/MicroJava/BV/Effect.thy
--- 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)
diff -r f708a31fa8bb -r 603f23d71ada src/HOL/MicroJava/BV/LBVComplete.thy
--- 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>")
diff -r f708a31fa8bb -r 603f23d71ada src/HOL/MicroJava/BV/LBVJVM.thy
--- 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
 
 
diff -r f708a31fa8bb -r 603f23d71ada src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- 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 *}