merged

--- a/src/HOL/IMP/Sec_Typing.thy	Wed Mar 13 21:25:08 2013 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Wed Mar 13 22:46:28 2013 +0100
@@ -5,6 +5,7 @@
 
 subsection "Syntax Directed Typing"
 
+text_raw{*\snip{sectypeDef}{0}{2}{% *}
 inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
 Skip:
   "l \<turnstile> SKIP" |
@@ -16,6 +17,7 @@
   "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
 While:
   "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
+text_raw{*}%endsnip*}
 
 code_pred (expected_modes: i => i => bool) sec_type .
 
@@ -181,6 +183,7 @@
 computation by an antimonotonicity rule. We introduce the standard system now
 and show the equivalence with our formulation. *}
 
+text_raw{*\snip{sectypepDef}{0}{2}{% *}
 inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
 Skip':
   "l \<turnstile>' SKIP" |
@@ -194,6 +197,7 @@
   "\<lbrakk> sec b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
 anti_mono':
   "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
+text_raw{*}%endsnip*}
 
 lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
 apply(induction rule: sec_type.induct)
@@ -215,6 +219,7 @@
 
 subsection "A Bottom-Up Typing System"
 
+text_raw{*\snip{sectypebDef}{0}{2}{% *}
 inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
 Skip2:
   "\<turnstile> SKIP : l" |
@@ -227,6 +232,7 @@
   \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
 While2:
   "\<lbrakk> sec b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
+text_raw{*}%endsnip*}
 
 
 lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"

--- a/src/HOL/Library/Nat_Bijection.thy	Wed Mar 13 21:25:08 2013 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Wed Mar 13 22:46:28 2013 +0100
@@ -368,4 +368,20 @@
   "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set_encode A = set_encode B \<longleftrightarrow> A = B"
 by (rule iffI, simp add: inj_onD [OF inj_on_set_encode], simp)
 
+lemma subset_decode_imp_le: assumes "set_decode m \<subseteq> set_decode n" shows "m \<le> n"
+proof -
+  have "n = m + set_encode (set_decode n - set_decode m)"
+  proof -
+    obtain A B where "m = set_encode A" "finite A" 
+                     "n = set_encode B" "finite B"
+      by (metis finite_set_decode set_decode_inverse)
+  thus ?thesis using assms
+    apply auto
+    apply (simp add: set_encode_def nat_add_commute setsum.F_subset_diff)
+    done
+  qed
+  thus ?thesis
+    by (metis le_add1)
+qed
+
 end

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Mar 13 21:25:08 2013 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Mar 13 22:46:28 2013 +0100
@@ -93,18 +93,23 @@
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
 
-lift_definition fset_member :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
-   by simp
+lemma member_transfer:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
+by transfer_prover
+
+lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
+   parametric member_transfer by simp
 
 abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
-lemma fset_member_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
+lemma fmember_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
   by transfer auto
 
 text {* We can export code: *}
 
-export_code fnil fcons fappend fmap ffilter fset in SML
+export_code fnil fcons fappend fmap ffilter fset fmember in SML
 
 subsection {* Using transfer with type @{text "fset"} *}