--- 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
--- 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 {*
--- /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
--- 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