# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268988057 -3600
# Node ID c8c2f83fadb47f3092a0ffa5d2c501146380421d
# Parent  a37c65fe10de5a216c6903fd5f629482956d95f9# Parent  984ea1299cd71d669712c62233dd15195c2730b7
merged

diff -r a37c65fe10de -r c8c2f83fadb4 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Mar 19 09:40:34 2010 +0100
+++ b/Nominal/FSet.thy	Fri Mar 19 09:40:57 2010 +0100
@@ -66,7 +66,9 @@
 section {* Augmenting a set -- @{const finsert} *}
 
 lemma nil_not_cons:
-  shows "\<not>[] \<approx> x # xs"
+  shows
+  "\<not>[] \<approx> x # xs"
+  "\<not>x # xs \<approx> []"
   by auto
 
 lemma memb_cons_iff:
@@ -132,7 +134,7 @@
   apply(metis)
   apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)
   apply(simp add: fcard_raw_delete_one)
-  apply(metis Suc_pred' fcard_raw_gt_0 fcard_raw_delete_one memb_def)
+  apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def)
   done
 
 lemma fcard_raw_rsp[quot_respect]:
@@ -253,11 +255,23 @@
   "a @ b \<approx> b @ a"
   by auto
 
-
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (auto)
 
+lemma set_cong: "(set x = set y) = (x \<approx> y)"
+  apply rule
+  apply simp_all
+  apply (induct x y rule: list_induct2')
+  apply simp_all
+  apply auto
+  done
+
+lemma inj_map_eq_iff:
+  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
+  by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
+
+
 
 
 section {* lifted part *}
@@ -277,7 +291,8 @@
   by (lifting memb_absorb)
 
 lemma fempty_not_finsert[simp]:
-  shows "{||} \<noteq> finsert x S"
+  "{||} \<noteq> finsert x S"
+  "finsert x S \<noteq> {||}"
   by (lifting nil_not_cons)
 
 lemma finsert_left_comm:
@@ -294,7 +309,7 @@
 
 text {* fset_to_set *}
 
-lemma fset_to_set_simps:
+lemma fset_to_set_simps[simp]:
   "fset_to_set {||} = {}"
   "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)"
   by (lifting list2set_thm)
@@ -307,6 +322,10 @@
   "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"
   by (lifting none_mem_nil)
 
+lemma fset_cong:
+  "(fset_to_set x = fset_to_set y) = (x = y)"
+  by (lifting set_cong)
+
 text {* fcard *}
 
 lemma fcard_fempty [simp]:
@@ -345,15 +364,15 @@
   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by (lifting list.exhaust)
 
-lemma fset_induct[case_names fempty finsert]:
+lemma fset_induct_weak[case_names fempty finsert]:
   shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
   by (lifting list.induct)
 
-lemma fset_induct2[case_names fempty finsert, induct type: fset]:
+lemma fset_induct[case_names fempty finsert, induct type: fset]:
   assumes prem1: "P {||}" 
   and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
   shows "P S"
-proof(induct S rule: fset_induct)
+proof(induct S rule: fset_induct_weak)
   case fempty
   show "P {||}" by (rule prem1)
 next
@@ -371,6 +390,38 @@
   qed
 qed
 
+lemma fset_induct2:
+  "P {||} {||} \<Longrightarrow>
+  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
+  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
+  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
+  P xsa ysa"
+  apply (induct xsa arbitrary: ysa)
+  apply (induct_tac x rule: fset_induct)
+  apply simp_all
+  apply (induct_tac xa rule: fset_induct)
+  apply simp_all
+  done
 
+(* fmap *)
+lemma fmap_simps[simp]:
+  "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
+  "fmap f (finsert x xs) = finsert (f x) (fmap f xs)"
+  by (lifting map.simps)
+
+lemma fmap_set_image:
+  "fset_to_set (fmap f fs) = f ` (fset_to_set fs)"
+  apply (induct fs)
+  apply (simp_all)
+done
+
+lemma inj_fmap_eq_iff:
+  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
+  by (lifting inj_map_eq_iff)
+
+ML {*
+fun dest_fsetT (Type ("FSet.fset", [T])) = T
+  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+*}
 
 end
diff -r a37c65fe10de -r c8c2f83fadb4 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Fri Mar 19 09:40:34 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 19 09:40:57 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
+imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" "Nominal2_FSet"
 begin
 
 (* The bindings data structure:
@@ -141,10 +141,16 @@
 
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
   | is_atom_set thy _ = false;
+
+fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
+  | is_atom_fset thy _ = false;
+
+val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 *}
 
 
 
+
 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []
@@ -201,7 +207,7 @@
     if b = noatoms then a else
     if b = a then noatoms else
     HOLogic.mk_binop @{const_name minus} (a, b);
-  fun mk_atoms t =
+  fun mk_atom_set t =
     let
       val ty = fastype_of t;
       val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
@@ -209,6 +215,14 @@
     in
       (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
     end;
+  fun mk_atom_fset t =
+    let
+      val ty = fastype_of t;
+      val atom_ty = dest_fsetT ty --> @{typ atom};
+      val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+    in
+      fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
+    end;
   (* Similar to one in USyntax *)
   fun mk_pair (fst, snd) =
     let val ty1 = fastype_of fst
@@ -288,7 +302,8 @@
             (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")
           else @{term "{} :: atom set"}) else
         if is_atom thy ty then mk_single_atom x else
-        if is_atom_set thy ty then mk_atoms x else
+        if is_atom_set thy ty then mk_atom_set x else
+        if is_atom_fset thy ty then mk_atom_fset x else
         if is_rec_type dt then nth fv_frees (body_index dt) $ x else
         @{term "{} :: atom set"}
       end;
@@ -402,7 +417,8 @@
       fun fv_bind args (NONE, i, _) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
-            if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else
+            if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
+            if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
             (* TODO we do not know what to do with non-atomizable things *)
             @{term "{} :: atom set"}
         | fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
@@ -420,7 +436,8 @@
               val arg =
                 if is_rec_type dt then nth fv_frees (body_index dt) $ x else
                 if ((is_atom thy) o fastype_of) x then mk_single_atom x else
-                if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
+                if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else
+                if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else
                 (* TODO we do not know what to do with non-atomizable things *)
                 @{term "{} :: atom set"};
               (* If i = j then we generate it only once *)
@@ -836,7 +853,8 @@
   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
     REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
-      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh}))
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
+      supp_fset_to_set supp_fmap_atom}))
 *}
 
 ML {*
@@ -854,7 +872,8 @@
 
   fun mk_supp_arg (x, ty) =
     if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
-    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atoms x)
+    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
+    if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
     else mk_supp ty x
   val lhss = map mk_supp_arg (frees ~~ tys)
   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
@@ -888,7 +907,8 @@
 ML {*
 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image finite_insert finite.emptyI finite_Un})
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
+    supp_fmap_atom finite_insert finite.emptyI finite_Un})
 *}
 
 ML {*
diff -r a37c65fe10de -r c8c2f83fadb4 Nominal/Nominal2_FSet.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Nominal2_FSet.thy	Fri Mar 19 09:40:57 2010 +0100
@@ -0,0 +1,107 @@
+theory Nominal2_FSet
+imports FSet Nominal2_Supp
+begin
+
+lemma permute_rsp_fset[quot_respect]:
+  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
+  apply (simp add: eqvts[symmetric])
+  apply clarify
+  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
+  apply (subst mem_eqvt[symmetric])
+  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
+  apply (subst mem_eqvt[symmetric])
+  apply (erule_tac x="- x \<bullet> xb" in allE)
+  apply simp
+  done
+
+instantiation FSet.fset :: (pt) pt
+begin
+
+term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+quotient_definition
+  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
+  by (rule permute_zero)
+
+lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
+  by (lifting permute_list_zero)
+
+lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
+  by (rule permute_plus)
+
+lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
+  by (lifting permute_list_plus)
+
+instance
+  apply default
+  apply (rule permute_fset_zero)
+  apply (rule permute_fset_plus)
+  done
+
+end
+
+lemma permute_fset[simp,eqvt]:
+  "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
+  "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
+  by (lifting permute_list.simps)
+
+lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
+  apply (induct l)
+  apply (simp_all)
+  apply (simp only: eqvt_apply)
+  done
+
+lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
+  by (lifting map_eqvt)
+
+lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
+  by (lifting set_eqvt)
+
+lemma supp_fset_to_set:
+  "supp (fset_to_set x) = supp x"
+  apply (simp add: supp_def)
+  apply (simp add: eqvts)
+  apply (simp add: fset_cong)
+  done
+
+lemma atom_fmap_cong:
+  shows "(fmap atom x = fmap atom y) = (x = y)"
+  apply(rule inj_fmap_eq_iff)
+  apply(simp add: inj_on_def)
+  done
+
+lemma supp_fmap_atom:
+  "supp (fmap atom x) = supp x"
+  apply (simp add: supp_def)
+  apply (simp add: eqvts eqvts_raw atom_fmap_cong)
+  done
+
+(*lemma "\<not> (memb x S) \<Longrightarrow> \<not> (memb y T) \<Longrightarrow> ((x # S) \<approx> (y # T)) = (x = y \<and> S \<approx> T)"*)
+
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
+lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \<union> supp xs"
+  oops
+
+lemma supp_finsert:
+  "supp (finsert (x :: 'a :: fs) S) = supp x \<union> supp S"
+  apply (subst supp_fset_to_set[symmetric])
+  apply simp
+  (* apply (simp add: supp_insert supp_fset_to_set) *)
+  oops
+
+instance fset :: (fs) fs
+  apply (default)
+  apply (induct_tac x rule: fset_induct)
+  apply (simp add: supp_def eqvts)
+  (* apply (simp add: supp_finsert) *)
+  (* apply default ? *)
+  oops
+
+end
diff -r a37c65fe10de -r c8c2f83fadb4 Nominal/TySch.thy
--- a/Nominal/TySch.thy	Fri Mar 19 09:40:34 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 09:40:57 2010 +0100
@@ -10,60 +10,6 @@
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = cheat_alpha_eqvt := false *}
 
-lemma permute_rsp_fset[quot_respect]:
-  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
-  apply (simp add: eqvts[symmetric])
-  apply clarify
-  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (erule_tac x="- x \<bullet> xb" in allE)
-  apply simp
-  done
-
-instantiation FSet.fset :: (pt) pt
-begin
-
-term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-quotient_definition
-  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
-by (rule permute_zero)
-
-lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
-by (lifting permute_list_zero)
-
-lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
-by (rule permute_plus)
-
-lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
-by (lifting permute_list_plus)
-
-instance
-apply default
-apply (rule permute_fset_zero)
-apply (rule permute_fset_plus)
-done
-
-end
-
-lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
-by (lifting set_eqvt)
-
-lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
-apply (induct l)
-apply (simp_all)
-apply (simp only: eqvt_apply)
-done
-
-lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
-by (lifting map_eqvt)
-
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
@@ -76,42 +22,39 @@
 thm t_tyS.perm
 thm t_tyS.inducts
 thm t_tyS.distinct
+ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
 lemma finite_fv_t_tyS:
   shows "finite (fv_t t)" "finite (fv_tyS ts)"
   by (induct rule: t_tyS.inducts) (simp_all)
 
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 lemma supp_fv_t_tyS:
   shows "fv_t t = supp t" "fv_tyS ts = supp ts"
-apply(induct rule: t_tyS.inducts)
-apply(simp_all only: t_tyS.fv)
-prefer 3
-apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
-prefer 2
-apply(subst finite_supp_Abs)
-apply(drule sym)
-apply(simp add: finite_fv_t_tyS(1))
-apply(simp)
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: t_tyS.perm)
-apply(simp_all only: permute_ABS)
-apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
-apply(simp_all only: alpha_gen)
-apply(simp_all only: eqvts[symmetric])
-apply(simp_all only: eqvts eqvts_raw)
-apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-apply(simp_all only: de_Morgan_conj[symmetric])
-done
+  apply(induct rule: t_tyS.inducts)
+  apply(simp_all only: t_tyS.fv)
+  prefer 3
+  apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
+  prefer 2
+  apply(subst finite_supp_Abs)
+  apply(drule sym)
+  apply(simp add: finite_fv_t_tyS(1))
+  apply(simp)
+  apply(simp_all (no_asm) only: supp_def)
+  apply(simp_all only: t_tyS.perm)
+  apply(simp_all only: permute_ABS)
+  apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
+  apply(simp_all only: alpha_gen)
+  apply(simp_all only: eqvts[symmetric])
+  apply(simp_all only: eqvts eqvts_raw)
+  apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
+  apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+  apply(simp_all only: de_Morgan_conj[symmetric])
+  done
 
 instance t and tyS :: fs
-apply default
-apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
-done
+  apply default
+  apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
+  done
 
 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
 
@@ -120,7 +63,7 @@
   \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2);
   \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)
  \<rbrakk> \<Longrightarrow> P a t"
-
+  oops
 
 
 lemma