--- a/Nominal/Abs.thy Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Abs.thy Tue Sep 28 08:21:47 2010 -0400
@@ -293,7 +293,13 @@
unfolding fun_rel_def
by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
-lemma abs_exhausts:
+lemma Abs_eq_iff:
+ shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
+ and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ by (lifting alphas_abs)
+
+lemma Abs_exhausts:
shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
@@ -301,12 +307,6 @@
prod.exhaust[where 'a="atom set" and 'b="'a"]
prod.exhaust[where 'a="atom list" and 'b="'a"])
-lemma abs_eq_iff:
- shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (cs, y)"
- and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
- and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
- unfolding alphas_abs by (lifting alphas_abs)
-
instantiation abs_set :: (pt) pt
begin
@@ -315,14 +315,14 @@
is
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
-lemma permute_Abs[simp]:
+lemma permute_Abs_set[simp]:
fixes x::"'a::pt"
shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
apply(default)
- apply(case_tac [!] x rule: abs_exhausts(1))
+ apply(case_tac [!] x rule: Abs_exhausts(1))
apply(simp_all)
done
@@ -343,7 +343,7 @@
instance
apply(default)
- apply(case_tac [!] x rule: abs_exhausts(2))
+ apply(case_tac [!] x rule: Abs_exhausts(2))
apply(simp_all)
done
@@ -364,22 +364,21 @@
instance
apply(default)
- apply(case_tac [!] x rule: abs_exhausts(3))
+ apply(case_tac [!] x rule: Abs_exhausts(3))
apply(simp_all)
done
end
-lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst
-lemma abs_swap1:
+lemma Abs_swap1:
assumes a1: "a \<notin> (supp x) - bs"
and a2: "b \<notin> (supp x) - bs"
shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- unfolding abs_eq_iff
- unfolding alphas_abs
+ unfolding Abs_eq_iff
unfolding alphas
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
unfolding fresh_star_def fresh_def
@@ -388,12 +387,11 @@
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
(auto simp add: supp_perm swap_atom)
-lemma abs_swap2:
+lemma Abs_swap2:
assumes a1: "a \<notin> (supp x) - (set bs)"
and a2: "b \<notin> (supp x) - (set bs)"
shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- unfolding abs_eq_iff
- unfolding alphas_abs
+ unfolding Abs_eq_iff
unfolding alphas
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
unfolding fresh_star_def fresh_def
@@ -402,21 +400,21 @@
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
(auto simp add: supp_perm swap_atom)
-lemma abs_supports:
+lemma Abs_supports:
shows "((supp x) - as) supports (Abs_set as x)"
and "((supp x) - as) supports (Abs_res as x)"
and "((supp x) - set bs) supports (Abs_lst bs x)"
unfolding supports_def
- unfolding permute_abs
- by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
+ unfolding permute_Abs
+ by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
function
supp_set :: "('a::pt) abs_set \<Rightarrow> atom set"
where
"supp_set (Abs_set as x) = supp x - as"
-apply(case_tac x rule: abs_exhausts(1))
+apply(case_tac x rule: Abs_exhausts(1))
apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
done
termination supp_set
@@ -426,9 +424,9 @@
supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
where
"supp_res (Abs_res as x) = supp x - as"
-apply(case_tac x rule: abs_exhausts(2))
+apply(case_tac x rule: Abs_exhausts(2))
apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
done
termination supp_res
@@ -438,9 +436,9 @@
supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
where
"supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-apply(case_tac x rule: abs_exhausts(3))
+apply(case_tac x rule: Abs_exhausts(3))
apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
done
termination supp_lst
@@ -450,86 +448,88 @@
shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
- apply(case_tac x rule: abs_exhausts(1))
+ apply(case_tac x rule: Abs_exhausts(1))
apply(simp add: supp_eqvt Diff_eqvt)
- apply(case_tac y rule: abs_exhausts(2))
+ apply(case_tac y rule: Abs_exhausts(2))
apply(simp add: supp_eqvt Diff_eqvt)
- apply(case_tac z rule: abs_exhausts(3))
+ apply(case_tac z rule: Abs_exhausts(3))
apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
done
-lemma aux_fresh:
+lemma Abs_fresh_aux:
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
by (rule_tac [!] fresh_fun_eqvt_app)
(simp_all only: eqvts_raw)
-lemma supp_abs_subset1:
+lemma Abs_supp_subset1:
assumes a: "finite (supp x)"
shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
and "(supp x) - as \<subseteq> supp (Abs_res as x)"
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
unfolding supp_conv_fresh
- by (auto dest!: aux_fresh)
+ by (auto dest!: Abs_fresh_aux)
(simp_all add: fresh_def supp_finite_atom_set a)
-lemma supp_abs_subset2:
+lemma Abs_supp_subset2:
assumes a: "finite (supp x)"
shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
and "supp (Abs_res as x) \<subseteq> (supp x) - as"
and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
by (rule_tac [!] supp_is_subset)
- (simp_all add: abs_supports a)
+ (simp_all add: Abs_supports a)
-lemma abs_finite_supp:
+lemma Abs_finite_supp:
assumes a: "finite (supp x)"
shows "supp (Abs_set as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
by (rule_tac [!] subset_antisym)
- (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
+ (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])
-lemma supp_abs:
+lemma supp_Abs:
fixes x::"'a::fs"
shows "supp (Abs_set as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
- by (rule_tac [!] abs_finite_supp)
+ by (rule_tac [!] Abs_finite_supp)
(simp_all add: finite_supp)
instance abs_set :: (fs) fs
apply(default)
- apply(case_tac x rule: abs_exhausts(1))
- apply(simp add: supp_abs finite_supp)
+ apply(case_tac x rule: Abs_exhausts(1))
+ apply(simp add: supp_Abs finite_supp)
done
instance abs_res :: (fs) fs
apply(default)
- apply(case_tac x rule: abs_exhausts(2))
- apply(simp add: supp_abs finite_supp)
+ apply(case_tac x rule: Abs_exhausts(2))
+ apply(simp add: supp_Abs finite_supp)
done
instance abs_lst :: (fs) fs
apply(default)
- apply(case_tac x rule: abs_exhausts(3))
- apply(simp add: supp_abs finite_supp)
+ apply(case_tac x rule: Abs_exhausts(3))
+ apply(simp add: supp_Abs finite_supp)
done
-lemma abs_fresh_iff:
+lemma Abs_fresh_iff:
fixes x::"'a::fs"
shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
unfolding fresh_def
- unfolding supp_abs
+ unfolding supp_Abs
by auto
-lemma Abs_eq_iff:
- shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
- and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
- and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
- by (lifting alphas_abs)
+lemma Abs_fresh_star:
+ fixes x::"'a::fs"
+ shows "as \<sharp>* Abs_set as x"
+ and "as \<sharp>* Abs_res as x"
+ and "set bs \<sharp>* Abs_lst bs x"
+ unfolding fresh_star_def
+ by(simp_all add: Abs_fresh_iff)
section {* Infrastructure for building tuples of relations and functions *}
@@ -570,6 +570,16 @@
unfolding prod_fv.simps
by (perm_simp) (rule refl)
+lemma prod_fv_supp:
+ shows "prod_fv supp supp = supp"
+by (rule ext)
+ (auto simp add: prod_fv.simps supp_Pair)
+
+lemma prod_alpha_eq:
+ shows "prod_alpha (op=) (op=) = (op=)"
+unfolding prod_alpha_def
+by (auto intro!: ext)
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Foo1.thy Tue Sep 28 08:21:47 2010 -0400
@@ -0,0 +1,49 @@
+theory Foo1
+imports "../Nominal2"
+begin
+
+(*
+ Contrived example that has more than one
+ binding function for a datatype
+*)
+
+atom_decl name
+
+nominal_datatype foo: trm =
+ Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm" bind x in t
+| Let1 a::"assg" t::"trm" bind "bn1 a" in t
+| Let2 a::"assg" t::"trm" bind "bn2 a" in t
+| Let3 a::"assg" t::"trm" bind "bn3 a" in t
+and assg =
+ As "name" "name" "trm"
+binder
+ bn1::"assg \<Rightarrow> atom list" and
+ bn2::"assg \<Rightarrow> atom list" and
+ bn3::"assg \<Rightarrow> atom list"
+where
+ "bn1 (As x y t) = [atom x]"
+| "bn2 (As x y t) = [atom y]"
+| "bn3 (As x y t) = [atom x, atom y]"
+
+thm foo.distinct
+thm foo.induct
+thm foo.inducts
+thm foo.exhaust
+thm foo.fv_defs
+thm foo.bn_defs
+thm foo.perm_simps
+thm foo.eq_iff
+thm foo.fv_bn_eqvt
+thm foo.size_eqvt
+thm foo.supports
+thm foo.fsupp
+thm foo.supp
+thm foo.fresh
+
+
+end
+
+
+
--- a/Nominal/Ex/Let.thy Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Ex/Let.thy Tue Sep 28 08:21:47 2010 -0400
@@ -2,41 +2,252 @@
imports "../Nominal2"
begin
-text {* example 3 or example 5 from Terms.thy *}
-
atom_decl name
-declare [[STEPS = 29]]
-
nominal_datatype trm =
Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm" bind x in t
-| Let a::"lts" t::"trm" bind "bn a" in t
-and lts =
- Lnil
-| Lcons "name" "trm" "lts"
+| Let as::"assn" t::"trm" bind "bn as" in t
+and assn =
+ ANil
+| ACons "name" "trm" "assn"
binder
bn
where
- "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
+ "bn ANil = []"
+| "bn (ACons x t as) = (atom x) # (bn as)"
+
+thm at_set_avoiding2
+thm trm_assn.fv_defs
+thm trm_assn.eq_iff
+thm trm_assn.bn_defs
+thm trm_assn.perm_simps
+thm trm_assn.induct
+thm trm_assn.inducts
+thm trm_assn.distinct
+thm trm_assn.supp
+thm trm_assn.fresh
+
+
+lemma fin_bn:
+ shows "finite (set (bn l))"
+ apply(induct l rule: trm_assn.inducts(2))
+ apply(simp_all)
+ done
+
+primrec
+ permute_bn_raw
+where
+ "permute_bn_raw p (ANil_raw) = ANil_raw"
+| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
+
+quotient_definition
+ "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
+is
+ "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
+ apply simp
+ apply clarify
+ apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
+ apply (rule TrueI)+
+ apply simp_all
+ apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
+ apply simp_all
+ done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma uu:
+ shows "alpha_bn (permute_bn p as) as"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+done
+
+lemma tt:
+ shows "(p \<bullet> bn as) = bn (permute_bn p as)"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+thm trm_assn.supp
+
+lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)"
+apply(simp add: fresh_def)
+apply(simp add: fresh_star_def)
+oops
+
+inductive
+ test_trm :: "trm \<Rightarrow> bool"
+and test_assn :: "assn \<Rightarrow> bool"
+where
+ "test_trm (Var x)"
+| "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)"
+| "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)"
+| "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)"
+| "test_assn ANil"
+| "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)"
+
+declare trm_assn.fv_bn_eqvt[eqvt]
+equivariance test_trm
+
+lemma
+ fixes p::"perm"
+ shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)"
+apply(induct t and as arbitrary: p and p rule: trm_assn.inducts)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+apply(assumption)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+apply(simp add: trm_assn.fresh fresh_star_def)
+apply(simp)
+defer
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+apply(assumption)
+apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))")
+apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))")
+apply(drule_tac c="()" in at_set_avoiding2)
+apply(simp add: supp_Unit)
+prefer 2
+apply(assumption)
+apply(simp add: finite_supp)
+apply(erule exE)
+apply(erule conjE)
+apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and
+ s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst)
+apply(rule trm_assn.eq_iff(4)[THEN iffD2])
+apply(simp add: uu)
+apply(drule supp_perm_eq)
+apply(simp add: tt)
+apply(rule test_trm_test_assn.intros(4))
+defer
+apply(subst permute_plus[symmetric])
+apply(blast)
+oops
+
+
+(*
+lemma
+ fixes t::trm
+ and as::assn
+ and c::"'a::fs"
+ assumes a1: "\<And>x c. P1 c (Var x)"
+ and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
+ and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
+ and a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"
+ and a5: "\<And>c. P2 c ANil"
+ and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"
+ shows "P1 c t" and "P2 c as"
+proof -
+ have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)"
+ and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"
+ apply(induct rule: trm_assn.inducts)
+ apply(simp)
+ apply(rule a1)
+ apply(simp)
+ apply(rule a2)
+ apply(assumption)
+ apply(assumption)
+ -- "lam case"
+ apply(simp)
+ apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+ apply(erule exE)
+ apply(erule conjE)
+ apply(drule supp_perm_eq[symmetric])
+ apply(simp)
+ apply(thin_tac "?X = ?Y")
+ apply(rule a3)
+ apply(simp add: atom_eqvt permute_set_eq)
+ apply(simp only: permute_plus[symmetric])
+ apply(rule at_set_avoiding2)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: freshs fresh_star_def)
+ --"let case"
+ apply(simp)
+ thm trm_assn.eq_iff
+ thm eq_iffs
+ apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q")
+ apply(erule exE)
+ apply(erule conjE)
+ prefer 2
+ apply(rule at_set_avoiding2)
+ apply(rule fin_bn)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: abs_fresh)
+ apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+ prefer 2
+ apply(rule a4)
+ prefer 4
+ apply(simp add: eq_iffs)
+ apply(rule conjI)
+ prefer 2
+ apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+ apply(subst permute_plus[symmetric])
+ apply(blast)
+ prefer 2
+ apply(simp add: eq_iffs)
+ thm eq_iffs
+ apply(subst permute_plus[symmetric])
+ apply(blast)
+ apply(simp add: supps)
+ apply(simp add: fresh_star_def freshs)
+ apply(drule supp_perm_eq[symmetric])
+ apply(simp)
+ apply(simp add: eq_iffs)
+ apply(simp)
+ apply(thin_tac "?X = ?Y")
+ apply(rule a4)
+ apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+ apply(subst permute_plus[symmetric])
+ apply(blast)
+ apply(subst permute_plus[symmetric])
+ apply(blast)
+ apply(simp add: supps)
+ thm at_set_avoiding2
+ --"HERE"
+ apply(rule at_set_avoiding2)
+ apply(rule fin_bn)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: fresh_star_def freshs)
+ apply(rule ballI)
+ apply(simp add: eqvts permute_bn)
+ apply(rule a5)
+ apply(simp add: permute_bn)
+ apply(rule a6)
+ apply simp
+ apply simp
+ done
+ then have a: "P1 c (0 \<bullet> t)" by blast
+ have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+ then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+*)
text {* *}
(*
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct[no_vars]
-thm trm_lts.inducts[no_vars]
-thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp(1-2)]
-
-
primrec
permute_bn_raw
where
--- a/Nominal/Ex/SingleLet.thy Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy Tue Sep 28 08:21:47 2010 -0400
@@ -13,7 +13,7 @@
| Let a::"assg" t::"trm" bind "bn a" in t
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2
and assg =
As "name" x::"name" t::"trm" bind x in t
binder
@@ -22,6 +22,7 @@
"bn (As x y t) = [atom x]"
+
thm single_let.distinct
thm single_let.induct
thm single_let.inducts
@@ -35,9 +36,7 @@
thm single_let.supports
thm single_let.fsupp
thm single_let.supp
-thm single_let.size
-
-
+thm single_let.fresh
end
--- a/Nominal/Ex/TypeSchemes.thy Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Ex/TypeSchemes.thy Tue Sep 28 08:21:47 2010 -0400
@@ -24,7 +24,8 @@
thm ty_tys.fv_bn_eqvt
thm ty_tys.size_eqvt
thm ty_tys.supports
-thm ty_tys.fsupp
+thm ty_tys.supp
+thm ty_tys.fresh
(* defined as two separate nominal datatypes *)
@@ -45,8 +46,8 @@
thm tys2.fv_bn_eqvt
thm tys2.size_eqvt
thm tys2.supports
-thm tys2.fsupp
-
+thm tys2.supp
+thm tys2.fresh
text {* *}
--- a/Nominal/Nominal2.thy Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Nominal2.thy Tue Sep 28 08:21:47 2010 -0400
@@ -568,7 +568,27 @@
qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
else []
-
+ (* postprocessing of eq and fv theorems *)
+
+ val qeq_iffs' = qeq_iffs
+ |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+ |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
+
+ val qsupp_constrs = qfv_defs
+ |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
+
+ val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+ val transform_thms =
+ [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp},
+ @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp},
+ @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp},
+ @{thm fresh_def[symmetric]}]
+
+ val qfresh_constrs = qsupp_constrs
+ |> map (fn thm => thm RS transform_thm)
+ |> map (simplify (HOL_basic_ss addsimps transform_thms))
+
+
(* noting the theorems *)
(* generating the prefix for the theorem names *)
@@ -578,7 +598,7 @@
val (_, lthy9') = lthyC
|> Local_Theory.note ((thms_suffix "distinct", []), qdistincts)
- ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
+ ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs)
||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs)
||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)
@@ -590,7 +610,8 @@
||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
- ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms)
+ ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
+ ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
in
(0, lthy9')
end handle TEST ctxt => (0, ctxt)
--- a/Nominal/ROOT.ML Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/ROOT.ML Tue Sep 28 08:21:47 2010 -0400
@@ -18,5 +18,6 @@
"Ex/Modules",
"Ex/SingleLet",
"Ex/TypeSchemes",
- "Ex/TypeVarsTest"
+ "Ex/TypeVarsTest",
+ "Ex/Foo1"
];
--- a/Nominal/nominal_dt_supp.ML Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML Tue Sep 28 08:21:47 2010 -0400
@@ -20,8 +20,6 @@
structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
struct
-fun lookup xs x = the (AList.lookup (op=) xs x)
-
(* supports lemmas for constructors *)
fun mk_supports_goal ctxt qtrm =
@@ -122,13 +120,13 @@
fun symmetric thms =
map (fn thm => thm RS @{thm sym}) thms
-val supp_abs_set = @{thms supp_abs(1)[symmetric]}
-val supp_abs_res = @{thms supp_abs(2)[symmetric]}
-val supp_abs_lst = @{thms supp_abs(3)[symmetric]}
+val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
+val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
+val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
-fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set
- | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res
- | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst
+fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set
+ | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
+ | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
fun mk_supp_abs_tac ctxt [] = []
| mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
@@ -139,8 +137,8 @@
|> fastype_of
|> body_type
|> (fn ty => case ty of
- @{typ "atom set"} => simp_tac (add_ss supp_abs_set)
- | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst)
+ @{typ "atom set"} => simp_tac (add_ss supp_Abs_set)
+ | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
| _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
@@ -186,6 +184,8 @@
end)
in
induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
+ |> map atomize
+ |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
end