# HG changeset patch # User Christian Urban # Date 1322301232 0 # Node ID da0fccee125c1a132597ee802c044f3ce1ce57d2 # Parent 324b148fc6b5985313fea67e632ca28015f28c23 a few more experiments with alpha-beta diff -r 324b148fc6b5 -r da0fccee125c Nominal/Ex/Beta.thy --- a/Nominal/Ex/Beta.thy Sat Nov 26 09:48:14 2011 +0000 +++ b/Nominal/Ex/Beta.thy Sat Nov 26 09:53:52 2011 +0000 @@ -161,6 +161,32 @@ end +quotient_definition subst_qlam ("_[_ ::q= _]") + where "subst_qlam::qlam \ name \ qlam \ qlam" is subst + +lemma + "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))" +apply(descending) +apply(simp) +apply(auto intro: equ_refl) +done + +lemma + "(QApp t1 t2)[y ::q= s] = QApp (t1[y ::q= s]) (t2[y ::q= s])" +apply(descending) +apply(simp) +apply(rule equ_refl) +done + +lemma + "(QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])" +apply(descending) +apply(subst subst.simps) +prefer 3 +apply(rule equ_refl) +oops + + lemma [eqvt]: "(p \ abs_qlam t) = abs_qlam (p \ t)" apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified]) @@ -194,22 +220,6 @@ apply(simp add: QVar_def) done - lemma supports_qapp: - "supp (t, s) supports (QApp t s)" -apply(subgoal_tac "supp (t, s) supports (abs_qlam (App (rep_qlam t) (rep_qlam s)))") -apply(simp add: QApp_def) -apply(subgoal_tac "supp (App (rep_qlam t) (rep_qlam s)) supports (abs_qlam (App (rep_qlam t) (rep_qlam s)))") -prefer 2 -apply(rule supports_abs_qlam) -apply(simp add: lam.supp) -oops - -lemma "(p \ rep_qlam t) \ rep_qlam (p \ t)" - apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) - apply (rule rep_abs_rsp[OF Quotient_qlam]) - apply (rule equ_refl) - done - section {* Supp *} definition @@ -229,6 +239,37 @@ quotient_definition "supp_qlam::qlam \ atom set" is "Supp::lam \ atom set" +lemma s: + assumes "s \ t" + shows "a \ (abs_qlam s) \ a \ (abs_qlam t)" +using assms +by (metis Quotient_qlam Quotient_rel_abs) + +lemma ss: + "Supp t supports (abs_qlam t)" +apply(simp only: supports_def) +apply(rule allI)+ +apply(rule impI) +apply(rule swap_fresh_fresh) +apply(drule conjunct1) +apply(auto)[1] +apply(simp add: Supp_def) +apply(auto)[1] +apply(simp add: s[symmetric]) +apply(rule supports_fresh) +apply(rule supports_abs_qlam) +apply(simp add: finite_supp) +apply(simp) +apply(drule conjunct2) +apply(auto)[1] +apply(simp add: Supp_def) +apply(auto)[1] +apply(simp add: s[symmetric]) +apply(rule supports_fresh) +apply(rule supports_abs_qlam) +apply(simp add: finite_supp) +apply(simp) +done lemma fixes t::"qlam" diff -r 324b148fc6b5 -r da0fccee125c Nominal/Ex/QuotientSet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/QuotientSet.thy Sat Nov 26 09:53:52 2011 +0000 @@ -0,0 +1,91 @@ +theory QuotientSet +imports + "../Nominal2" +begin + +lemma supp_quot: + "(supp (R, x)) supports (R `` {x})" +unfolding supports_def +unfolding fresh_def[symmetric] +apply(perm_simp) +apply(simp add: swap_fresh_fresh) +done + +lemma + assumes "equiv UNIV R" + and "(x, y) \ R" + shows "R `` {x} = R `` {y}" +using assms +by (rule equiv_class_eq) + +lemma s1: + assumes "equiv UNIV R" + and "(x, y) \ R" + shows "a \ (R `` {x}) \ a \ (R `` {y})" +using assms +apply(subst equiv_class_eq) +apply(auto) +done + +lemma s2: + fixes x::"'a::fs" + assumes "equiv UNIV R" + and "supp R = {}" + shows "\{supp y | y. (x, y) \ R} supports (R `` {x})" +unfolding supports_def +apply(rule allI)+ +apply(rule impI) +apply(rule swap_fresh_fresh) +apply(drule conjunct1) +apply(auto)[1] +apply(subst s1) +apply(rule assms) +apply(assumption) +apply(rule supports_fresh) +apply(rule supp_quot) +apply(simp add: supp_Pair finite_supp assms) +apply(simp add: supp_Pair assms) +apply(drule conjunct2) +apply(auto)[1] +apply(subst s1) +apply(rule assms) +apply(assumption) +apply(rule supports_fresh) +apply(rule supp_quot) +apply(simp add: supp_Pair finite_supp assms) +apply(simp add: supp_Pair assms) +done + +lemma s3: + fixes S::"'a::fs set" + assumes "finite S" + and "S \ {}" + and "a \ S" + shows "\x \ S. a \ x" +using assms +apply(auto simp add: fresh_def) +apply(subst (asm) supp_of_finite_sets) +apply(auto) +done + +(* +lemma supp_inter: + fixes x::"'a::fs" + assumes "equiv UNIV R" + and "supp R = {}" + shows "supp (R `` {x}) = \{supp y | y. (x, y) \ R}" +apply(rule finite_supp_unique) +apply(rule s2) +apply(rule assms) +apply(rule assms) +apply(metis (lam_lifting, no_types) at_base_infinite finite_UNIV) +*) + + + + + +end + + +