--- a/Nominal/Ex/TypeSchemes.thy Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy Sun Nov 14 11:46:39 2010 +0000
@@ -66,7 +66,6 @@
apply(clarify)
apply(drule supp_perm_eq[symmetric])
apply(simp)
-thm at_set_avoiding
apply(rule at_set_avoiding2)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
@@ -90,85 +89,87 @@
done
-text {* *}
-
-(*
-lemma strong_induct:
- assumes a1: "\<And>name b. P b (Var name)"
- and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
- and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
- shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
-proof -
- have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
- apply (rule ty_tys.induct)
- apply (simp add: a1)
- apply (simp)
- apply (rule allI)+
- apply (rule a2)
- apply simp
- apply simp
- apply (rule allI)
- apply (rule allI)
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)")
- apply clarify
- apply(rule_tac t="p \<bullet> All fset ty" and
- s="pa \<bullet> (p \<bullet> All fset ty)" in subst)
- apply (rule supp_perm_eq)
- apply assumption
- apply (simp only: ty_tys.perm_simps)
- apply (rule a3)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2)
- apply (simp add: fin_fset)
- apply (simp add: finite_supp)
- apply (simp add: eqvts finite_supp)
- apply (rule_tac p=" -p" in permute_boolE)
- apply(simp add: eqvts)
- apply(simp add: permute_fun_def atom_eqvt)
- apply (simp add: fresh_star_def)
- apply clarify
- apply (simp add: fresh_def)
- apply(auto)
- apply (simp add: ty_tys.supp)
- done
- then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
- then show ?thesis by simp
-qed
+text {* Some Tests *}
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)
+ apply(simp add: Abs_eq_iff)
apply(rule_tac x="0::perm" in exI)
apply(simp add: alphas)
apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)
+ apply(simp add: 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)
+ 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 eqvts supp_at_base)
+ 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)
+ 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 eqvts ty_tys.eq_iff supp_at_base)
+ 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)
+ apply(simp add: ty_tys.eq_iff Abs_eq_iff)
apply(clarify)
- apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
+ apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
apply auto
done
+
+text {* Some lemmas about fsets *}
+
+lemma atom_map_fset_cong:
+ shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
+ apply(rule inj_map_fset_cong)
+ apply(simp add: inj_on_def)
+ done
+
+lemma supp_map_fset_atom:
+ shows "supp (map_fset atom S) = supp S"
+ unfolding supp_def
+ apply(perm_simp)
+ apply(simp add: atom_map_fset_cong)
+ done
+
+lemma supp_at_fset:
+ fixes S::"('a::at_base) fset"
+ shows "supp S = fset (map_fset atom S)"
+ apply (induct S)
+ apply (simp add: supp_empty_fset)
+ apply (simp add: supp_insert_fset)
+ apply (simp add: supp_at_base)
+ done
+
+lemma fresh_star_atom:
+ fixes a::"'a::at_base"
+ shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
+ apply (induct S)
+ apply (simp add: fresh_set_empty)
+ apply simp
+ apply (unfold fresh_def)
+ apply (simp add: supp_of_finite_insert)
+ apply (rule conjI)
+ apply (unfold fresh_star_def)
+ apply simp
+ apply (unfold fresh_def)
+ apply (simp add: supp_at_base supp_atom)
+ apply clarify
+ apply auto
+ done
+
+
+
+(*
fun
lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
where
--- a/Nominal/Nominal2.thy Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Nominal2.thy Sun Nov 14 11:46:39 2010 +0000
@@ -2,7 +2,6 @@
imports
"../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
- "Nominal2_FSet"
"Abs"
uses ("nominal_dt_rawperm.ML")
("nominal_dt_rawfuns.ML")
--- a/Nominal/Nominal2_FSet.thy Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Nominal2_FSet.thy Sun Nov 14 11:46:39 2010 +0000
@@ -4,43 +4,6 @@
begin
-lemma atom_map_fset_cong:
- shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
- apply(rule inj_map_fset_cong)
- apply(simp add: inj_on_def)
- done
-lemma supp_map_fset_atom:
- shows "supp (map_fset atom S) = supp S"
- unfolding supp_def
- apply(perm_simp)
- apply(simp add: atom_map_fset_cong)
- done
-
-lemma supp_at_fset:
- fixes S::"('a::at_base) fset"
- shows "supp S = fset (map_fset atom S)"
- apply (induct S)
- apply (simp add: supp_empty_fset)
- apply (simp add: supp_insert_fset)
- apply (simp add: supp_at_base)
- done
-
-lemma fresh_star_atom:
- fixes a::"'a::at_base"
- shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
- apply (induct S)
- apply (simp add: fresh_set_empty)
- apply simp
- apply (unfold fresh_def)
- apply (simp add: supp_of_finite_insert)
- apply (rule conjI)
- apply (unfold fresh_star_def)
- apply simp
- apply (unfold fresh_def)
- apply (simp add: supp_at_base supp_atom)
- apply clarify
- apply auto
- done
end