--- a/LMCS-Paper/Paper.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/LMCS-Paper/Paper.thy Mon Jan 09 10:45:12 2012 +0000
@@ -114,7 +114,11 @@
and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
type-variables. While it is possible to implement this kind of more general
binders by iterating single binders, this leads to a rather clumsy
- formalisation of W. The need of iterating single binders is also one reason
+ formalisation of W.
+
+ {\bf add example about W}
+
+ The need of iterating single binders is also one reason
why Nominal Isabelle and similar theorem provers that only provide
mechanisms for binding single variables have not fared extremely well with
the more advanced tasks in the POPLmark challenge \cite{challenge05},
--- a/LMCS-Review Mon Jan 09 10:12:46 2012 +0000
+++ b/LMCS-Review Mon Jan 09 10:45:12 2012 +0000
@@ -49,7 +49,11 @@
> algorithm W [...]." But there is no analysis in the paper of what was
> hard in algorithm W coded with single binders, or explanation of how
> it would be done in the new system reported in this paper showing why
-> the new approach works better in practice. Although this example is
+> the new approach works better in practice.
+
+Added
+
+> Although this example is
> one of the main motivations given for the work, there is apparently no
> formalization of algorithm W in the library of examples that comes
> with Nominal2 described in this paper. I think that should be
@@ -59,24 +63,35 @@
> binding single variables have not fared extremely well with the more
> advanced tasks in the POPLmark challenge [2], because also there one
> would like to bind multiple variables at once.").
->
+
+No time to provide full examples yet. They will be provided
+once Nominal2 becomes more mature and people are using it
+and help to provide theories.
+
> The new Isabelle package "Nominal2", described in this paper, is not
> ready for users without a lot of hand-holding from the Nominal2
> developers. This paper would have more impact if interested users
> could try the tool without so much difficulty.
->
+
+The plan is to have Nominal Isabelle be part of the next stable
+release of Isabelle, which should be out before the summer 2012.
+At the moment it can be downloaded as a bundle and is ready
+to be used (we have confirmation from two groups for this).
+
> A few more specific points:
>
> Bottom of p.7: I don't understand the paragraph containing equations
> (2.4) and (2.5).
->
+
+
> Bottom of p.9: The parameters R and fa of the alpha equivalence
> relation are dropped in the examples, so the examples are not clear.
> I think there is a typo in the first example: "It can be easily
> checked that ({x,y},x->y) and ({y,x},y->x) are alpha-equivalent [...]"
> Did you mean "({x,y},x->y) and ({y,x},x->y) are alpha-equivalent"?
->
->
+
+
+
> Referee no 2:
>
> * The paper can be accepted for Logical Methods in Computer Science
@@ -188,6 +203,18 @@
> of pairs. I think that the system should at the very least allow encoding
> this example, otherwise set-abstractions will not be very useful in
> practice.
+
+>> datatype trm =
+>> Var string
+>> | App trm trm
+>> | Lam string trm
+>> | Let "(string * trm) fset" trm
+>> Not a problem. Both finite sets and bags should be possible as
+>> constructors within the new package.
+>> Best regards and a happy new year!
+>> Andrei Popescu
+
+
>
> Detailed comments
>
--- a/Nominal/Ex/LamTest.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/Nominal/Ex/LamTest.thy Mon Jan 09 10:45:12 2012 +0000
@@ -1658,7 +1658,7 @@
and S::"'a::at set"
assumes a: "a \<notin> S" "b \<notin> S"
shows "(a \<leftrightarrow> b) \<bullet> S = S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: permute_flip_at)
lemma removeAll_eqvt[eqvt]:
--- a/Nominal/Ex/TypeSchemes.thy Mon Jan 09 10:12:46 2012 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,441 +0,0 @@
-theory TypeSchemes
-imports "../Nominal2"
-begin
-
-section {*** Type Schemes ***}
-
-atom_decl name
-
-(* defined as a single nominal datatype *)
-
-nominal_datatype ty =
- Var "name"
-| Fun "ty" "ty"
-and tys =
- All xs::"name fset" ty::"ty" binds (set+) xs in ty
-
-ML {*
-get_all_info @{context}
-*}
-
-ML {*
-get_info @{context} "TypeSchemes.ty"
-*}
-
-ML {*
-#strong_exhaust (the_info @{context} "TypeSchemes.tys")
-*}
-
-thm ty_tys.distinct
-thm ty_tys.induct
-thm ty_tys.inducts
-thm ty_tys.exhaust
-thm ty_tys.strong_exhaust
-thm ty_tys.fv_defs
-thm ty_tys.bn_defs
-thm ty_tys.perm_simps
-thm ty_tys.eq_iff
-thm ty_tys.fv_bn_eqvt
-thm ty_tys.size_eqvt
-thm ty_tys.supports
-thm ty_tys.supp
-thm ty_tys.fresh
-
-fun
- lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
-where
- "lookup [] Y = Var Y"
-| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
-
-lemma lookup_eqvt[eqvt]:
- shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
-apply(simp_all)
-done
-
-lemma TEST1:
- assumes "x = Inl y"
- shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"
-using assms by simp
-
-lemma TEST2:
- assumes "x = Inr y"
- shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"
-using assms by simp
-
-lemma test:
- assumes a: "\<exists>y. f x = Inl y"
- shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
-using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
-
-lemma test2:
- assumes a: "\<exists>y. f x = Inl y"
- shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
-using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
-
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
- subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
-and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
-where
- "subst \<theta> (Var X) = lookup \<theta> X"
-| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
-| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
-(*unfolding subst_substs_graph_def eqvt_def
-apply rule
-apply perm_simp
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply rule*)
-thm subst_substs_graph.intros
-apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
-apply(simp add: eqvt_def)
-apply(rule allI)
-apply(simp add: permute_fun_def permute_bool_def)
-apply(rule ext)
-apply(rule ext)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp)
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply(simp)
---"Eqvt One way"
-apply(erule subst_substs_graph.induct)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp)
---"Eqvt done"
-apply(rule TrueI)
-apply (case_tac x)
-apply simp apply clarify
-apply (rule_tac y="b" in ty_tys.exhaust(1))
-apply (auto)[1]
-apply (auto)[1]
-apply simp apply clarify
-apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
-apply (auto)[1]
-apply (auto)[5]
---"LAST GOAL"
-apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
-apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
-apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))")
-prefer 2
-apply (simp add: eqvt_at_def subst_def)
-apply rule
-apply (subst test2)
-apply (simp add: subst_substs_sumC_def)
-apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))")
-prefer 2
-apply simp
-apply (simp add: the1_equality)
-apply auto[1]
-apply (erule_tac x="x" in allE)
-apply simp
-apply(cases rule: subst_substs_graph.cases)
-apply assumption
-apply (rule_tac x="lookup \<theta> X" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
- (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply clarify
-apply simp
---"-"
-apply clarify
- apply (frule supp_eqvt_at)
- apply (simp add: finite_supp)
- apply (erule Abs_res_fcb)
- apply (simp add: Abs_fresh_iff)
- apply (simp add: Abs_fresh_iff)
- apply auto[1]
- apply (simp add: fresh_def fresh_star_def)
- apply (erule contra_subsetD)
- apply (simp add: supp_Pair)
- apply blast
- apply clarify
- apply (simp)
- apply (simp add: eqvt_at_def)
- apply (subst Abs_eq_iff)
- apply (rule_tac x="0::perm" in exI)
- apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
- apply (simp add: alphas fresh_star_zero)
- apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
- apply blast
- apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
- apply (simp add: supp_Pair eqvts eqvts_raw)
- apply auto[1]
- apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
- apply (simp add: fresh_star_def fresh_def)
- apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
- apply (simp add: eqvts eqvts_raw)
- apply (simp add: fresh_star_def fresh_def)
- apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])
- apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
- apply (erule subsetD)
- apply (simp add: supp_eqvt)
- apply (metis le_eqvt permute_boolI)
- apply (rule perm_supp_eq)
- apply (simp add: fresh_def fresh_star_def)
- apply blast
- done
-
-
-termination (eqvt) by lexicographic_order
-
-
-section {* defined as two separate nominal datatypes *}
-
-nominal_datatype ty2 =
- Var2 "name"
-| Fun2 "ty2" "ty2"
-
-nominal_datatype tys2 =
- All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty
-
-thm tys2.distinct
-thm tys2.induct tys2.strong_induct
-thm tys2.exhaust tys2.strong_exhaust
-thm tys2.fv_defs
-thm tys2.bn_defs
-thm tys2.perm_simps
-thm tys2.eq_iff
-thm tys2.fv_bn_eqvt
-thm tys2.size_eqvt
-thm tys2.supports
-thm tys2.supp
-thm tys2.fresh
-
-fun
- lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
-where
- "lookup2 [] Y = Var2 Y"
-| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
-
-lemma lookup2_eqvt[eqvt]:
- shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
- by (induct Ts T rule: lookup2.induct) simp_all
-
-nominal_primrec
- subst2 :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
-where
- "subst2 \<theta> (Var2 X) = lookup2 \<theta> X"
-| "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)"
- unfolding eqvt_def subst2_graph_def
- apply (rule, perm_simp, rule)
- apply(rule TrueI)
- apply(case_tac x)
- apply(rule_tac y="b" in ty2.exhaust)
- apply(blast)
- apply(blast)
- apply(simp_all add: ty2.distinct)
- done
-
-termination (eqvt)
- by lexicographic_order
-
-
-lemma supp_fun_app2_eqvt:
- assumes e: "eqvt f"
- shows "supp (f a b) \<subseteq> supp a \<union> supp b"
- using supp_fun_app_eqvt[OF e] supp_fun_app
- by blast
-
-lemma supp_subst:
- "supp (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
- apply (rule supp_fun_app2_eqvt)
- unfolding eqvt_def by (simp add: eqvts_raw)
-
-lemma fresh_star_inter1:
- "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
- unfolding fresh_star_def by blast
-
-nominal_primrec
- substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
-where
- "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)"
- unfolding eqvt_def substs2_graph_def
- apply (rule, perm_simp, rule)
- apply auto[2]
- apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
- apply auto[1]
- apply(simp)
- apply(erule conjE)
- apply (erule Abs_res_fcb)
- apply (simp add: Abs_fresh_iff)
- apply(simp add: fresh_def)
- apply(simp add: supp_Abs)
- apply(rule impI)
- apply(subgoal_tac "x \<notin> supp \<theta>")
- prefer 2
- apply(auto simp add: fresh_star_def fresh_def)[1]
- apply(subgoal_tac "x \<in> supp t")
- using supp_subst
- apply(blast)
- using supp_subst
- apply(blast)
- apply clarify
- apply (simp add: subst2.eqvt)
- apply (subst Abs_eq_iff)
- apply (rule_tac x="0::perm" in exI)
- apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
- apply (simp add: alphas fresh_star_zero)
- apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
- apply blast
- apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
- apply (simp add: supp_Pair eqvts eqvts_raw)
- apply auto[1]
- apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
- apply (simp add: fresh_star_def fresh_def)
- apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
- apply (simp add: eqvts eqvts_raw)
- apply (simp add: fresh_star_def fresh_def)
- apply (drule subsetD[OF supp_subst])
- apply (simp add: supp_Pair)
- apply (rule perm_supp_eq)
- apply (simp add: fresh_def fresh_star_def)
- apply blast
- done
-
-text {* Some Tests about Alpha-Equality *}
-
-lemma
- shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
- apply(simp add: ty_tys.eq_iff Abs_eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
- done
-
-lemma
- shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
- apply(simp add: ty_tys.eq_iff Abs_eq_iff)
- apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)
- done
-
-lemma
- shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
- apply(simp add: ty_tys.eq_iff Abs_eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
-done
-
-lemma
- assumes a: "a \<noteq> b"
- shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
- using a
- apply(simp add: ty_tys.eq_iff Abs_eq_iff)
- apply(clarify)
- apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
- apply auto
- done
-
-
-
-
-end
--- a/Nominal/Ex/TypeSchemes1.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy Mon Jan 09 10:45:12 2012 +0000
@@ -2,16 +2,16 @@
imports "../Nominal2"
begin
-section {*** Type Schemes defined as two separate nominal datatypes ***}
+section {* Type Schemes defined as two separate nominal datatypes *}
atom_decl name
nominal_datatype ty =
Var "name"
-| Fun "ty" "ty"
+| Fun "ty" "ty" ("_ \<rightarrow> _")
nominal_datatype tys =
- All xs::"name fset" ty::"ty" binds (set+) xs in ty
+ All xs::"name fset" ty::"ty" binds (set+) xs in ty ("All [_]._")
thm tys.distinct
thm tys.induct tys.strong_induct
@@ -26,25 +26,60 @@
thm tys.supp
thm tys.fresh
+subsection {* Some Tests about Alpha-Equality *}
+
+lemma
+ shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
+ apply(simp add: Abs_eq_iff)
+ apply(rule_tac x="0::perm" in exI)
+ apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+ done
+
+lemma
+ shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
+ apply(simp add: Abs_eq_iff)
+ apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+ apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
+ done
+
+lemma
+ shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
+ apply(simp add: Abs_eq_iff)
+ apply(rule_tac x="0::perm" in exI)
+ apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+done
+
+lemma
+ assumes a: "a \<noteq> b"
+ shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
+ using a
+ apply(simp add: Abs_eq_iff)
+ apply(clarify)
+ apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+ apply auto
+ done
+
+
+subsection {* Substitution function for types and type schemes *}
+
+type_synonym
+ Subst = "(name \<times> ty) list"
fun
- lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+ lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"
where
"lookup [] Y = Var Y"
| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
lemma lookup_eqvt[eqvt]:
shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
-apply(simp_all)
-done
-
+ by (induct Ts T rule: lookup.induct) (simp_all)
nominal_primrec
- subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+ subst :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
where
- "subst \<theta> (Var X) = lookup \<theta> X"
-| "subst \<theta> (Fun T1 T) = Fun (subst \<theta> T1) (subst \<theta> T)"
+ "\<theta><Var X> = lookup \<theta> X"
+| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
unfolding eqvt_def subst_graph_def
apply (rule, perm_simp, rule)
apply(rule TrueI)
@@ -58,7 +93,6 @@
termination (eqvt)
by lexicographic_order
-
lemma supp_fun_app_eqvt:
assumes e: "eqvt f"
shows "supp (f a b) \<subseteq> supp a \<union> supp b"
@@ -71,14 +105,10 @@
unfolding eqvt_def
by (simp add: permute_fun_def subst.eqvt)
-lemma fresh_star_inter1:
- "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
- unfolding fresh_star_def by blast
-
nominal_primrec
- substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+ substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
where
- "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
+ "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
unfolding eqvt_def substs_graph_def
apply (rule, perm_simp, rule)
apply auto[2]
@@ -94,7 +124,7 @@
apply(subgoal_tac "x \<notin> supp \<theta>")
prefer 2
apply(auto simp add: fresh_star_def fresh_def)[1]
- apply(subgoal_tac "x \<in> supp t")
+ apply(subgoal_tac "x \<in> supp T")
using supp_subst
apply(blast)
using supp_subst
@@ -105,12 +135,12 @@
apply (rule_tac x="0::perm" in exI)
apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
apply (simp add: alphas fresh_star_zero)
- apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+ apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa")
apply blast
- apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
+ apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
apply (simp add: supp_Pair eqvts eqvts_raw)
apply auto[1]
- apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
+ apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'")
apply (simp add: fresh_star_def fresh_def)
apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
apply (simp add: eqvts eqvts_raw)
@@ -122,40 +152,227 @@
apply blast
done
-text {* Some Tests about Alpha-Equality *}
+termination (eqvt)
+ by (lexicographic_order)
+
+
+subsection {* Generalisation of types and type-schemes*}
+
+fun
+ subst_dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_|_")
+where
+ "[]|p = []"
+| "((X,T)#\<theta>)|p = (p \<bullet> X, T)#(\<theta>|p)"
+
+fun
+ subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>" [100,60] 120)
+where
+ "\<theta><[]> = []"
+| "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"
+
+fun
+ dom :: "Subst \<Rightarrow> name fset"
+where
+ "dom [] = {||}"
+| "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"
+
+lemma dom_eqvt[eqvt]:
+ shows "p \<bullet> (dom \<theta>) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
+
+lemma dom_subst:
+ fixes \<theta>1 \<theta>2::"Subst"
+ shows "dom (\<theta>2<\<theta>1>) = (dom \<theta>1)"
+by (induct \<theta>1) (auto)
+
+lemma dom_pi:
+ shows "dom (\<theta>|p) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
+
+lemma dom_fresh_lookup:
+ fixes \<theta>::"Subst"
+ assumes "\<forall>Y \<in> fset (dom \<theta>). atom Y \<sharp> X"
+ shows "lookup \<theta> X = Var X"
+using assms
+by (induct \<theta>) (auto simp add: fresh_at_base)
+
+lemma dom_fresh_ty:
+ fixes \<theta>::"Subst"
+ and T::"ty"
+ assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> T"
+ shows "\<theta><T> = T"
+using assms
+by (induct T rule: ty.induct) (auto simp add: ty.fresh dom_fresh_lookup)
-lemma
- shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
- apply(simp add: Abs_eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+lemma dom_fresh_subst:
+ fixes \<theta> \<theta>'::"Subst"
+ assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> \<theta>'"
+ shows "\<theta><\<theta>'> = \<theta>'"
+using assms
+by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
+
+
+definition
+ generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
+where
+ "T \<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
+
+
+lemma lookup_fresh:
+ fixes X::"name"
+ assumes a: "atom X \<sharp> \<theta>"
+ shows "lookup \<theta> X = Var X"
+ using a
+ by (induct \<theta>) (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
+
+lemma lookup_dom:
+ fixes X::"name"
+ assumes "X |\<notin>| dom \<theta>"
+ shows "lookup \<theta> X = Var X"
+ using assms
+ by (induct \<theta>) (auto)
+
+lemma w1:
+ shows "\<theta><\<theta>'|p> = (\<theta><\<theta>'>)|p"
+ by (induct \<theta>')(auto)
+
+lemma w2:
+ assumes "name |\<in>| dom \<theta>'"
+ shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
+using assms
+apply(induct \<theta>')
+apply(auto simp add: notin_empty_fset)
+done
+
+lemma w3:
+ assumes "name |\<in>| dom \<theta>"
+ shows "lookup \<theta> name = lookup (\<theta>|p) (p \<bullet> name)"
+using assms
+apply(induct \<theta>)
+apply(auto simp add: notin_empty_fset)
+done
+
+lemma fresh_lookup:
+ fixes X Y::"name"
+ and \<theta>::"Subst"
+ assumes asms: "atom X \<sharp> Y" "atom X \<sharp> \<theta>"
+ shows "atom X \<sharp> (lookup \<theta> Y)"
+ using assms
+ apply (induct \<theta>)
+ apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
done
-lemma
- shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
- apply(simp add: Abs_eq_iff)
- apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
- done
-
-lemma
- shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
- apply(simp add: Abs_eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+lemma test:
+ fixes \<theta> \<theta>'::"Subst"
+ and T::"ty"
+ assumes "(p \<bullet> atom ` fset (dom \<theta>')) \<sharp>* \<theta>" "supp All [dom \<theta>'].T \<sharp>* p"
+ shows "\<theta><\<theta>'<T>> = \<theta><\<theta>'|p><\<theta><p \<bullet> T>>"
+using assms
+apply(induct T rule: ty.induct)
+defer
+apply(auto simp add: tys.supp ty.supp fresh_star_def)[1]
+apply(auto simp add: tys.supp ty.supp fresh_star_def supp_at_base)[1]
+apply(case_tac "name |\<in>| dom \<theta>'")
+apply(subgoal_tac "atom (p \<bullet> name) \<sharp> \<theta>")
+apply(subst (2) lookup_fresh)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(simp)
+apply(simp add: w1)
+apply(simp add: w2)
+apply(subst w3[symmetric])
+apply(simp add: dom_subst)
+apply(simp)
+apply(perm_simp)
+apply(rotate_tac 2)
+apply(drule_tac p="p" in permute_boolI)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(metis notin_fset)
+apply(simp add: lookup_dom)
+apply(perm_simp)
+apply(subst dom_fresh_ty)
+apply(auto)[1]
+apply(rule fresh_lookup)
+apply(simp add: dom_subst)
+apply(simp add: dom_pi)
+apply(perm_simp)
+apply(rotate_tac 2)
+apply(drule_tac p="p" in permute_boolI)
+apply(perm_simp)
+apply(simp add: fresh_at_base)
+apply (metis in_fset)
+apply(simp add: dom_subst)
+apply(simp add: dom_pi[symmetric])
+apply(perm_simp)
+apply(subst supp_perm_eq)
+apply(simp add: supp_at_base fresh_star_def)
+apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)
+apply(simp)
done
lemma
- assumes a: "a \<noteq> b"
- shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
- using a
- apply(simp add: Abs_eq_iff)
- apply(clarify)
- apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
- apply auto
- done
+ shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"
+unfolding generalises_def
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac t="S" and s="All [Xs].T'" in subst)
+apply(simp)
+using at_set_avoiding3
+apply -
+apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)
+apply(drule_tac x="\<theta>" in meta_spec)
+apply(drule_tac x="All [Xs].T'" in meta_spec)
+apply(drule meta_mp)
+apply(simp)
+apply(drule meta_mp)
+apply(simp add: finite_supp)
+apply(drule meta_mp)
+apply(simp add: finite_supp)
+apply(drule meta_mp)
+apply(simp add: tys.fresh fresh_star_def)
+apply(erule exE)
+apply(erule conjE)+
+apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)
+apply(rule supp_perm_eq)
+apply(assumption)
+apply(perm_simp)
+apply(subst substs.simps)
+apply(perm_simp)
+apply(simp)
+apply(rule_tac x="\<theta><\<theta>'|p>" in exI)
+apply(rule_tac x="p \<bullet> Xs" in exI)
+apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)
+apply(rule conjI)
+apply(simp)
+apply(rule conjI)
+defer
+apply(simp add: dom_subst)
+apply(simp add: dom_pi dom_eqvt[symmetric])
+apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)
+apply(simp)
+apply(simp)
+apply(rule test)
+apply(perm_simp)
+apply(rotate_tac 2)
+apply(drule_tac p="p" in permute_boolI)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)
+done
-
-
+lemma
+ "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> dom \<theta> = Xs)"
+apply(auto)
+defer
+unfolding generalises_def
+apply(auto)[1]
+apply(auto)[1]
+apply(drule sym)
+apply(simp add: Abs_eq_iff2)
+apply(simp add: alphas)
+apply(auto)
+apply(rule_tac x="map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>" in exI)
+apply(auto)
+oops
end
--- a/Nominal/Ex/TypeSchemes2.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy Mon Jan 09 10:45:12 2012 +0000
@@ -265,7 +265,7 @@
apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
apply (erule subsetD)
apply (simp add: supp_eqvt)
- apply (metis le_eqvt permute_boolI)
+ apply (metis permute_pure subset_eqvt)
apply (rule perm_supp_eq)
apply (simp add: fresh_def fresh_star_def)
apply blast
@@ -307,7 +307,4 @@
apply auto
done
-
-
-
end
--- a/Nominal/Nominal2_Abs.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/Nominal/Nominal2_Abs.thy Mon Jan 09 10:45:12 2012 +0000
@@ -365,7 +365,7 @@
then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
then have zb: "p \<bullet> as = p' \<bullet> as"
- apply(auto simp add: permute_set_eq)
+ apply(auto simp add: permute_set_def)
apply(rule_tac x="xa" in exI)
apply(simp)
done
@@ -800,7 +800,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)
+ have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_set {b} y"
by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
also have "\<dots> = Abs_set {a} x" using ** by simp
@@ -809,7 +809,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)
+ also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_set {b} y"
by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
finally have "Abs_set {a} x = Abs_set {b} y" .
@@ -824,7 +824,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)
+ have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_res {b} y"
by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
also have "\<dots> = Abs_res {a} x" using ** by simp
@@ -833,7 +833,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)
+ also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_res {b} y"
by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
finally have "Abs_res {a} x = Abs_res {b} y" .
--- a/Nominal/Nominal2_Base.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/Nominal/Nominal2_Base.thy Mon Jan 09 10:45:12 2012 +0000
@@ -430,25 +430,33 @@
subsection {* Permutations for sets *}
+instantiation "set" :: (pt) pt
+begin
+
+definition
+ "p \<bullet> X = {p \<bullet> x | x. x \<in> X}"
+
+instance
+apply default
+apply (auto simp add: permute_set_def)
+done
+
+end
+
lemma permute_set_eq:
- fixes x::"'a::pt"
- shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
- unfolding permute_fun_def
- unfolding permute_bool_def
- apply(auto simp add: mem_def)
- apply(rule_tac x="- p \<bullet> x" in exI)
- apply(simp)
- done
+ shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}"
+unfolding permute_set_def
+by (auto) (metis permute_minus_cancel(1))
lemma permute_set_eq_image:
shows "p \<bullet> X = permute p ` X"
- unfolding permute_set_eq by auto
+ unfolding permute_set_def by auto
lemma permute_set_eq_vimage:
shows "p \<bullet> X = permute (- p) -` X"
- unfolding permute_fun_def permute_bool_def
- unfolding vimage_def Collect_def mem_def ..
-
+ unfolding permute_set_eq vimage_def
+ by simp
+
lemma permute_finite [simp]:
shows "finite (p \<bullet> X) = finite X"
unfolding permute_set_eq_vimage
@@ -457,36 +465,36 @@
lemma swap_set_not_in:
assumes a: "a \<notin> S" "b \<notin> S"
shows "(a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma swap_set_in:
assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma swap_set_in_eq:
assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma swap_set_both_in:
assumes a: "a \<in> S" "b \<in> S"
shows "(a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma mem_permute_iff:
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
- unfolding mem_def permute_fun_def permute_bool_def
- by simp
+ unfolding permute_set_def
+ by auto
lemma empty_eqvt:
shows "p \<bullet> {} = {}"
- unfolding empty_def Collect_def
- by (simp add: permute_fun_def permute_bool_def)
+ unfolding permute_set_def
+ by (simp)
lemma insert_eqvt:
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
@@ -665,6 +673,9 @@
instance "fun" :: (pure, pure) pure
by default (simp add: permute_fun_def permute_pure)
+instance set :: (pure) pure
+by default (simp add: permute_set_def permute_pure)
+
instance prod :: (pure, pure) pure
by default (induct_tac x, simp add: permute_pure)
@@ -879,12 +890,13 @@
lemma mem_eqvt [eqvt]:
shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_def
- by (rule permute_fun_app_eq)
+ unfolding permute_bool_def permute_set_def
+ by (auto)
lemma Collect_eqvt [eqvt]:
shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
+ unfolding permute_set_eq permute_fun_def
+ by (auto simp add: permute_bool_def)
lemma inter_eqvt [eqvt]:
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
@@ -1871,7 +1883,7 @@
proof -
{ fix a b
have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq by force
+ unfolding permute_set_def by force
}
then show "(\<Union>x \<in> S. supp x) supports S"
unfolding supports_def
@@ -2491,7 +2503,7 @@
using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
have c: "(p \<bullet> a) \<sharp> c" using p1
unfolding fresh_star_def Ball_def
- by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
+ by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_def)
hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
qed
@@ -2506,7 +2518,7 @@
proof (induct)
case empty
have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
- by (simp add: permute_set_eq supp_perm)
+ by (simp add: permute_set_def supp_perm)
then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
next
case (insert a bs)
--- a/Nominal/Nominal2_FCB.thy Mon Jan 09 10:12:46 2012 +0000
+++ b/Nominal/Nominal2_FCB.thy Mon Jan 09 10:45:12 2012 +0000
@@ -212,67 +212,107 @@
qed
-text {* NOT DONE
lemma Abs_res_fcb2:
fixes as bs :: "atom set"
and x y :: "'b :: fs"
and c::"'c::fs"
assumes eq: "[as]res. x = [bs]res. y"
and fin: "finite as" "finite bs"
- and fcb1: "as \<sharp>* f as x c"
+ and fcb1: "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c"
and fresh1: "as \<sharp>* c"
and fresh2: "bs \<sharp>* c"
- and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
- and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
- shows "f as x c = f bs y c"
+ and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f (as \<inter> supp x) x c) = f (p \<bullet> (as \<inter> supp x)) (p \<bullet> x) c"
+ and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f (bs \<inter> supp y) y c) = f (p \<bullet> (bs \<inter> supp y)) (p \<bullet> y) c"
+ shows "f (as \<inter> supp x) x c = f (bs \<inter> supp y) y c"
proof -
- have "supp (as, x, c) supports (f as x c)"
+ have "supp (as, x, c) supports (f (as \<inter> supp x) x c)"
unfolding supports_def fresh_def[symmetric]
- by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)
- then have fin1: "finite (supp (f as x c))"
+ by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh inter_eqvt supp_eqvt)
+ then have fin1: "finite (supp (f (as \<inter> supp x) x c))"
using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)
- have "supp (bs, y, c) supports (f bs y c)"
+ have "supp (bs, y, c) supports (f (bs \<inter> supp y) y c)"
unfolding supports_def fresh_def[symmetric]
- by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)
- then have fin2: "finite (supp (f bs y c))"
+ by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh inter_eqvt supp_eqvt)
+ then have fin2: "finite (supp (f (bs \<inter> supp y) y c))"
using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)
obtain q::"perm" where
- fr1: "(q \<bullet> as) \<sharp>* (x, c, f as x c, f bs y c)" and
- fr2: "supp q \<sharp>* ([as]res. x)" and
- inc: "supp q \<subseteq> as \<union> (q \<bullet> as)"
- using at_set_avoiding3[where xs="as" and c="(x, c, f as x c, f bs y c)" and x="[as]res. x"]
+ fr1: "(q \<bullet> (as \<inter> supp x)) \<sharp>* (x, c, f (as \<inter> supp x) x c, f (bs \<inter> supp y) y c)" and
+ fr2: "supp q \<sharp>* ([as \<inter> supp x]set. x)" and
+ inc: "supp q \<subseteq> (as \<inter> supp x) \<union> (q \<bullet> (as \<inter> supp x))"
+ using at_set_avoiding3[where xs="as \<inter> supp x" and c="(x, c, f (as \<inter> supp x) x c, f (bs \<inter> supp y) y c)"
+ and x="[as \<inter> supp x]set. x"]
fin1 fin2 fin
- by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
- have "[q \<bullet> as]res. (q \<bullet> x) = q \<bullet> ([as]res. x)" by simp
- also have "\<dots> = [as]res. x"
+ apply (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
+ done
+ have "[q \<bullet> (as \<inter> supp x)]set. (q \<bullet> x) = q \<bullet> ([as \<inter> supp x]set. x)" by simp
+ also have "\<dots> = [as \<inter> supp x]set. x"
by (simp only: fr2 perm_supp_eq)
- finally have "[q \<bullet> as]res. (q \<bullet> x) = [bs]res. y" using eq by simp
+ finally have "[q \<bullet> (as \<inter> supp x)]set. (q \<bullet> x) = [bs \<inter> supp y]set. y" using eq
+ by(simp add: Abs_eq_res_set)
then obtain r::perm where
qq1: "q \<bullet> x = r \<bullet> y" and
qq2: "(q \<bullet> as \<inter> supp (q \<bullet> x)) = r \<bullet> (bs \<inter> supp y)" and
- qq3: "supp r \<subseteq> bs \<inter> supp y \<union> q \<bullet> as \<inter> supp (q \<bullet> x)"
+ qq3: "supp r \<subseteq> (bs \<inter> supp y) \<union> q \<bullet> (as \<inter> supp x)"
apply(drule_tac sym)
- apply(subst(asm) Abs_eq_res_set)
apply(simp only: Abs_eq_iff2 alphas)
apply(erule exE)
apply(erule conjE)+
apply(drule_tac x="p" in meta_spec)
- apply(simp add: set_eqvt)
+ apply(simp add: set_eqvt inter_eqvt supp_eqvt)
done
- have "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c" sorry (* FCB? *)
+ have "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c" by (rule fcb1)
then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)"
by (simp add: permute_bool_def)
then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"
apply(simp add: fresh_star_eqvt set_eqvt)
- sorry (* perm? *)
- then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2
- apply (simp add: inter_eqvt)
- sorry
- (* rest similar reversing it other way around... *)
- show ?thesis sorry
+ apply(subst (asm) perm1)
+ using inc fresh1 fr1
+ apply(auto simp add: fresh_star_def fresh_Pair)
+ done
+ then have "(r \<bullet> (bs \<inter> supp y)) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq1 qq2
+ apply(perm_simp)
+ apply simp
+ done
+ then have "r \<bullet> ((bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c)"
+ apply(simp add: fresh_star_eqvt set_eqvt)
+ apply(subst (asm) perm2[symmetric])
+ using qq3 fresh2 fr1
+ apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
+ done
+ then have fcb2: "(bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c" by (simp add: permute_bool_def)
+ have "f (as \<inter> supp x) x c = q \<bullet> (f (as \<inter> supp x) x c)"
+ apply(rule perm_supp_eq[symmetric])
+ using inc fcb1 fr1
+ apply (auto simp add: fresh_star_def)
+ done
+ also have "\<dots> = f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"
+ apply(rule perm1)
+ using inc fresh1 fr1 by (auto simp add: fresh_star_def)
+ also have "\<dots> = f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq1 qq2
+ apply(perm_simp)
+ apply simp
+ done
+ also have "\<dots> = r \<bullet> (f (bs \<inter> supp y) y c)"
+ apply(rule perm2[symmetric])
+ using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)
+ also have "... = f (bs \<inter> supp y) y c"
+ apply(rule perm_supp_eq)
+ using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)
+ finally show ?thesis by simp
qed
-*}
+typedef ('a::fs, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}"
+apply(subgoal_tac "\<exists>x::'b::fs. x \<in> (UNIV::('b::fs) set)")
+apply(erule exE)
+apply(rule_tac x="\<lambda>_. x" in exI)
+apply(auto)
+apply(rule_tac S="supp x" in supports_finite)
+apply(simp add: supports_def)
+apply(perm_simp)
+apply(simp add: fresh_def[symmetric])
+apply(simp add: swap_fresh_fresh)
+apply(simp add: finite_supp)
+done
lemma Abs_lst_fcb2:
fixes as bs :: "atom list"