--- a/Nominal/Manual/LamEx.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,620 +0,0 @@
-theory LamEx
-imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs"
-begin
-
-atom_decl name
-
-datatype rlam =
- rVar "name"
-| rApp "rlam" "rlam"
-| rLam "name" "rlam"
-
-fun
- rfv :: "rlam \<Rightarrow> atom set"
-where
- rfv_var: "rfv (rVar a) = {atom a}"
-| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
-| rfv_lam: "rfv (rLam a t) = (rfv t) - {atom a}"
-
-instantiation rlam :: pt
-begin
-
-primrec
- permute_rlam
-where
- "permute_rlam pi (rVar a) = rVar (pi \<bullet> a)"
-| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)"
-| "permute_rlam pi (rLam a t) = rLam (pi \<bullet> a) (permute_rlam pi t)"
-
-instance
-apply default
-apply(induct_tac [!] x)
-apply(simp_all)
-done
-
-end
-
-instantiation rlam :: fs
-begin
-
-lemma neg_conj:
- "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
- by simp
-
-instance
-apply default
-apply(induct_tac x)
-(* var case *)
-apply(simp add: supp_def)
-apply(fold supp_def)[1]
-apply(simp add: supp_at_base)
-(* app case *)
-apply(simp only: supp_def)
-apply(simp only: permute_rlam.simps)
-apply(simp only: rlam.inject)
-apply(simp only: neg_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp)
-(* lam case *)
-apply(simp only: supp_def)
-apply(simp only: permute_rlam.simps)
-apply(simp only: rlam.inject)
-apply(simp only: neg_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp)
-apply(fold supp_def)[1]
-apply(simp add: supp_at_base)
-done
-
-end
-
-
-(* for the eqvt proof of the alpha-equivalence *)
-declare permute_rlam.simps[eqvt]
-
-lemma rfv_eqvt[eqvt]:
- shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)"
-apply(induct t)
-apply(simp_all)
-apply(simp add: permute_set_eq atom_eqvt)
-apply(simp add: union_eqvt)
-apply(simp add: Diff_eqvt)
-apply(simp add: permute_set_eq atom_eqvt)
-done
-
-inductive
- alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVar a) \<approx>a (rVar b)"
-| a2: "\<lbrakk>t1 \<approx>a t2; s1 \<approx>a s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a rApp t2 s2"
-| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s)
- \<Longrightarrow> rLam a t \<approx>a rLam b s"
-
-lemma a3_inverse:
- assumes "rLam a t \<approx>a rLam b s"
- shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s)"
-using assms
-apply(erule_tac alpha.cases)
-apply(auto)
-done
-
-text {* should be automatic with new version of eqvt-machinery *}
-lemma alpha_eqvt:
- shows "t \<approx>a s \<Longrightarrow> (pi \<bullet> t) \<approx>a (pi \<bullet> s)"
-apply(induct rule: alpha.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(simp)
-apply(rule a3)
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp only: Diff_eqvt rfv_eqvt insert_eqvt atom_eqvt empty_eqvt)
-apply(simp)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: Diff_eqvt rfv_eqvt atom_eqvt insert_eqvt empty_eqvt)
-apply(subst permute_eqvt[symmetric])
-apply(simp)
-done
-
-lemma alpha_refl:
- shows "t \<approx>a t"
-apply(induct t rule: rlam.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(rule a3)
-apply(rule_tac x="0" in exI)
-apply(simp_all add: fresh_star_def fresh_zero_perm)
-done
-
-lemma alpha_sym:
- shows "t \<approx>a s \<Longrightarrow> s \<approx>a t"
-apply(induct rule: alpha.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(rule a3)
-apply(erule exE)
-apply(rule_tac x="- pi" in exI)
-apply(simp)
-apply(simp add: fresh_star_def fresh_minus_perm)
-apply(erule conjE)+
-apply(rotate_tac 3)
-apply(drule_tac pi="- pi" in alpha_eqvt)
-apply(simp)
-done
-
-lemma alpha_trans:
- shows "t1 \<approx>a t2 \<Longrightarrow> t2 \<approx>a t3 \<Longrightarrow> t1 \<approx>a t3"
-apply(induct arbitrary: t3 rule: alpha.induct)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(simp add: a1)
-apply(rotate_tac 4)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(simp add: a2)
-apply(rotate_tac 1)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(erule conjE)+
-apply(erule exE)+
-apply(erule conjE)+
-apply(rule a3)
-apply(rule_tac x="pia + pi" in exI)
-apply(simp add: fresh_star_plus)
-apply(drule_tac x="- pia \<bullet> sa" in spec)
-apply(drule mp)
-apply(rotate_tac 7)
-apply(drule_tac pi="- pia" in alpha_eqvt)
-apply(simp)
-apply(rotate_tac 9)
-apply(drule_tac pi="pia" in alpha_eqvt)
-apply(simp)
-done
-
-lemma alpha_equivp:
- shows "equivp alpha"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(auto intro: alpha_refl alpha_sym alpha_trans)
- done
-
-lemma alpha_rfv:
- shows "t \<approx>a s \<Longrightarrow> rfv t = rfv s"
- apply(induct rule: alpha.induct)
- apply(simp_all)
- done
-
-inductive
- alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a2 _" [100, 100] 100)
-where
- a21: "a = b \<Longrightarrow> (rVar a) \<approx>a2 (rVar b)"
-| a22: "\<lbrakk>t1 \<approx>a2 t2; s1 \<approx>a2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a2 rApp t2 s2"
-| a23: "(a = b \<and> t \<approx>a2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>a2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>a2 rLam b s"
-
-lemma fv_vars:
- fixes a::name
- assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x"
- shows "(pi \<bullet> t) \<approx>a2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
-using a1
-apply(induct t)
-apply(auto)
-apply(rule a21)
-apply(case_tac "name = a")
-apply(simp)
-apply(simp)
-defer
-apply(rule a22)
-apply(simp)
-apply(simp)
-apply(rule a23)
-apply(case_tac "a = name")
-apply(simp)
-oops
-
-
-lemma
- assumes a1: "t \<approx>a2 s"
- shows "t \<approx>a s"
-using a1
-apply(induct)
-apply(rule alpha.intros)
-apply(simp)
-apply(rule alpha.intros)
-apply(simp)
-apply(simp)
-apply(rule alpha.intros)
-apply(erule disjE)
-apply(rule_tac x="0" in exI)
-apply(simp add: fresh_star_def fresh_zero_perm)
-apply(erule conjE)+
-apply(drule alpha_rfv)
-apply(simp)
-apply(rule_tac x="(a \<leftrightarrow> b)" in exI)
-apply(simp)
-apply(erule conjE)+
-apply(rule conjI)
-apply(drule alpha_rfv)
-apply(drule sym)
-apply(simp)
-apply(simp add: rfv_eqvt[symmetric])
-defer
-apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")
-apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")
-
-defer
-sorry
-
-lemma
- assumes a1: "t \<approx>a s"
- shows "t \<approx>a2 s"
-using a1
-apply(induct)
-apply(rule alpha2.intros)
-apply(simp)
-apply(rule alpha2.intros)
-apply(simp)
-apply(simp)
-apply(clarify)
-apply(rule alpha2.intros)
-apply(frule alpha_rfv)
-apply(rotate_tac 4)
-apply(drule sym)
-apply(simp)
-apply(drule sym)
-apply(simp)
-oops
-
-quotient_type lam = rlam / alpha
- by (rule alpha_equivp)
-
-quotient_definition
- "Var :: name \<Rightarrow> lam"
-is
- "rVar"
-
-quotient_definition
- "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-is
- "rApp"
-
-quotient_definition
- "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-is
- "rLam"
-
-quotient_definition
- "fv :: lam \<Rightarrow> atom set"
-is
- "rfv"
-
-lemma perm_rsp[quot_respect]:
- "(op = ===> alpha ===> alpha) permute permute"
- apply(auto)
- apply(rule alpha_eqvt)
- apply(simp)
- done
-
-lemma rVar_rsp[quot_respect]:
- "(op = ===> alpha) rVar rVar"
- by (auto intro: a1)
-
-lemma rApp_rsp[quot_respect]:
- "(alpha ===> alpha ===> alpha) rApp rApp"
- by (auto intro: a2)
-
-lemma rLam_rsp[quot_respect]:
- "(op = ===> alpha ===> alpha) rLam rLam"
- apply(auto)
- apply(rule a3)
- apply(rule_tac x="0" in exI)
- unfolding fresh_star_def
- apply(simp add: fresh_star_def fresh_zero_perm)
- apply(simp add: alpha_rfv)
- done
-
-lemma rfv_rsp[quot_respect]:
- "(alpha ===> op =) rfv rfv"
-apply(simp add: alpha_rfv)
-done
-
-
-section {* lifted theorems *}
-
-lemma lam_induct:
- "\<lbrakk>\<And>name. P (Var name);
- \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
- \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk>
- \<Longrightarrow> P lam"
- apply (lifting rlam.induct)
- done
-
-instantiation lam :: pt
-begin
-
-quotient_definition
- "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
-is
- "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
-
-lemma permute_lam [simp]:
- shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
- and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
- and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
-apply(lifting permute_rlam.simps)
-done
-
-instance
-apply default
-apply(induct_tac [!] x rule: lam_induct)
-apply(simp_all)
-done
-
-end
-
-lemma fv_lam [simp]:
- shows "fv (Var a) = {atom a}"
- and "fv (App t1 t2) = fv t1 \<union> fv t2"
- and "fv (Lam a t) = fv t - {atom a}"
-apply(lifting rfv_var rfv_app rfv_lam)
-done
-
-lemma fv_eqvt:
- shows "(p \<bullet> fv t) = fv (p \<bullet> t)"
-apply(lifting rfv_eqvt)
-done
-
-lemma a1:
- "a = b \<Longrightarrow> Var a = Var b"
- by (lifting a1)
-
-lemma a2:
- "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
- by (lifting a2)
-
-lemma a3:
- "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)\<rbrakk>
- \<Longrightarrow> Lam a t = Lam b s"
- apply (lifting a3)
- done
-
-lemma a3_inv:
- assumes "Lam a t = Lam b s"
- shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)"
-using assms
-apply(lifting a3_inverse)
-done
-
-lemma alpha_cases:
- "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
- \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
- \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s;
- \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s\<rbrakk>
- \<Longrightarrow> P\<rbrakk>
- \<Longrightarrow> P"
- by (lifting alpha.cases)
-
-(* not sure whether needed *)
-lemma alpha_induct:
- "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
- \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
- \<And>t a s b.
- \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and>
- (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s)\<rbrakk>
- \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
- \<Longrightarrow> qxb qx qxa"
- by (lifting alpha.induct)
-
-(* should they lift automatically *)
-lemma lam_inject [simp]:
- shows "(Var a = Var b) = (a = b)"
- and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
-apply(lifting rlam.inject(1) rlam.inject(2))
-apply(regularize)
-prefer 2
-apply(regularize)
-prefer 2
-apply(auto)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(simp add: alpha.a1)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(rule alpha.a2)
-apply(simp_all)
-done
-
-lemma Lam_pseudo_inject:
- shows "(Lam a t = Lam b s) =
- (\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s))"
-apply(rule iffI)
-apply(rule a3_inv)
-apply(assumption)
-apply(rule a3)
-apply(assumption)
-done
-
-lemma rlam_distinct:
- shows "\<not>(rVar nam \<approx>a rApp rlam1' rlam2')"
- and "\<not>(rApp rlam1' rlam2' \<approx>a rVar nam)"
- and "\<not>(rVar nam \<approx>a rLam nam' rlam')"
- and "\<not>(rLam nam' rlam' \<approx>a rVar nam)"
- and "\<not>(rApp rlam1 rlam2 \<approx>a rLam nam' rlam')"
- and "\<not>(rLam nam' rlam' \<approx>a rApp rlam1 rlam2)"
-apply auto
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-done
-
-lemma lam_distinct[simp]:
- shows "Var nam \<noteq> App lam1' lam2'"
- and "App lam1' lam2' \<noteq> Var nam"
- and "Var nam \<noteq> Lam nam' lam'"
- and "Lam nam' lam' \<noteq> Var nam"
- and "App lam1 lam2 \<noteq> Lam nam' lam'"
- and "Lam nam' lam' \<noteq> App lam1 lam2"
-apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
-done
-
-lemma var_supp1:
- shows "(supp (Var a)) = (supp a)"
- apply (simp add: supp_def)
- done
-
-lemma var_supp:
- shows "(supp (Var a)) = {a:::name}"
- using var_supp1 by (simp add: supp_at_base)
-
-lemma app_supp:
- shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
-apply(simp only: supp_def lam_inject)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-done
-
-(* supp for lam *)
-lemma lam_supp1:
- shows "(supp (atom x, t)) supports (Lam x t) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
-apply(simp_all add: fresh_atom)
-done
-
-lemma lam_fsupp1:
- assumes a: "finite (supp t)"
- shows "finite (supp (Lam x t))"
-apply(rule supports_finite)
-apply(rule lam_supp1)
-apply(simp add: a supp_Pair supp_atom)
-done
-
-instance lam :: fs
-apply(default)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: var_supp)
-apply(simp add: app_supp)
-apply(simp add: lam_fsupp1)
-done
-
-lemma supp_fv:
- shows "supp t = fv t"
-apply(induct t rule: lam_induct)
-apply(simp add: var_supp)
-apply(simp add: app_supp)
-apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)")
-apply(simp add: supp_Abs)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
-apply(simp add: Lam_pseudo_inject)
-apply(simp add: Abs_eq_iff alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
-done
-
-lemma lam_supp2:
- shows "supp (Lam x t) = supp (Abs {atom x} t)"
-apply(simp add: supp_def permute_set_eq atom_eqvt)
-apply(simp add: Lam_pseudo_inject)
-apply(simp add: Abs_eq_iff supp_fv alpha_gen)
-done
-
-lemma lam_supp:
- shows "supp (Lam x t) = ((supp t) - {atom x})"
-apply(simp add: lam_supp2)
-apply(simp add: supp_Abs)
-done
-
-lemma fresh_lam:
- "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"
-apply(simp add: fresh_def)
-apply(simp add: lam_supp)
-apply(auto)
-done
-
-lemma lam_induct_strong:
- fixes a::"'a::fs"
- assumes a1: "\<And>name b. P b (Var name)"
- and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
- and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
- shows "P a lam"
-proof -
- have "\<And>pi a. P a (pi \<bullet> lam)"
- proof (induct lam rule: lam_induct)
- case (1 name pi)
- show "P a (pi \<bullet> Var name)"
- apply (simp)
- apply (rule a1)
- done
- next
- case (2 lam1 lam2 pi)
- have b1: "\<And>pi a. P a (pi \<bullet> lam1)" by fact
- have b2: "\<And>pi a. P a (pi \<bullet> lam2)" by fact
- show "P a (pi \<bullet> App lam1 lam2)"
- apply (simp)
- apply (rule a2)
- apply (rule b1)
- apply (rule b2)
- done
- next
- case (3 name lam pi a)
- have b: "\<And>pi a. P a (pi \<bullet> lam)" by fact
- obtain c::name where fr: "atom c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)"
- apply(rule obtain_atom)
- apply(auto)
- sorry
- from b fr have p: "P a (Lam c (((c \<leftrightarrow> (pi \<bullet> name)) + pi)\<bullet>lam))"
- apply -
- apply(rule a3)
- apply(blast)
- apply(simp add: fresh_Pair)
- done
- have eq: "(atom c \<rightleftharpoons> atom (pi\<bullet>name)) \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)"
- apply(rule swap_fresh_fresh)
- using fr
- apply(simp add: fresh_lam fresh_Pair)
- apply(simp add: fresh_lam fresh_Pair)
- done
- show "P a (pi \<bullet> Lam name lam)"
- apply (simp)
- apply(subst eq[symmetric])
- using p
- apply(simp only: permute_lam)
- apply(simp add: flip_def)
- done
- qed
- then have "P a (0 \<bullet> lam)" by blast
- then show "P a lam" by simp
-qed
-
-
-lemma var_fresh:
- fixes a::"name"
- shows "(atom a \<sharp> (Var b)) = (atom a \<sharp> b)"
- apply(simp add: fresh_def)
- apply(simp add: var_supp1)
- done
-
-
-
-end
-
--- a/Nominal/Manual/LamEx2.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,563 +0,0 @@
-theory LamEx
-imports "../Nominal/Nominal2" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
-begin
-
-atom_decl name
-
-datatype rlam =
- rVar "name"
-| rApp "rlam" "rlam"
-| rLam "name" "rlam"
-
-fun
- rfv :: "rlam \<Rightarrow> atom set"
-where
- rfv_var: "rfv (rVar a) = {atom a}"
-| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
-| rfv_lam: "rfv (rLam a t) = (rfv t) - {atom a}"
-
-instantiation rlam :: pt
-begin
-
-primrec
- permute_rlam
-where
- "permute_rlam pi (rVar a) = rVar (pi \<bullet> a)"
-| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)"
-| "permute_rlam pi (rLam a t) = rLam (pi \<bullet> a) (permute_rlam pi t)"
-
-instance
-apply default
-apply(induct_tac [!] x)
-apply(simp_all)
-done
-
-end
-
-instantiation rlam :: fs
-begin
-
-lemma neg_conj:
- "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
- by simp
-
-instance
-apply default
-apply(induct_tac x)
-(* var case *)
-apply(simp add: supp_def)
-apply(fold supp_def)[1]
-apply(simp add: supp_at_base)
-(* app case *)
-apply(simp only: supp_def)
-apply(simp only: permute_rlam.simps)
-apply(simp only: rlam.inject)
-apply(simp only: neg_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp)
-(* lam case *)
-apply(simp only: supp_def)
-apply(simp only: permute_rlam.simps)
-apply(simp only: rlam.inject)
-apply(simp only: neg_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp)
-apply(fold supp_def)[1]
-apply(simp add: supp_at_base)
-done
-
-end
-
-
-(* for the eqvt proof of the alpha-equivalence *)
-declare permute_rlam.simps[eqvt]
-
-lemma rfv_eqvt[eqvt]:
- shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)"
-apply(induct t)
-apply(simp_all)
-apply(simp add: permute_set_eq atom_eqvt)
-apply(simp add: union_eqvt)
-apply(simp add: Diff_eqvt)
-apply(simp add: permute_set_eq atom_eqvt)
-done
-
-inductive
- alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
-| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s)) \<Longrightarrow> rLam a t \<approx> rLam b s"
-print_theorems
-thm alpha.induct
-
-lemma a3_inverse:
- assumes "rLam a t \<approx> rLam b s"
- shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))"
-using assms
-apply(erule_tac alpha.cases)
-apply(auto)
-done
-
-text {* should be automatic with new version of eqvt-machinery *}
-lemma alpha_eqvt:
- shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
-apply(induct rule: alpha.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(simp)
-apply(rule a3)
-apply(rule alpha_gen_atom_eqvt)
-apply(rule rfv_eqvt)
-apply assumption
-done
-
-lemma alpha_refl:
- shows "t \<approx> t"
-apply(induct t rule: rlam.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(rule a3)
-apply(rule_tac x="0" in exI)
-apply(rule alpha_gen_refl)
-apply(assumption)
-done
-
-lemma alpha_sym:
- shows "t \<approx> s \<Longrightarrow> s \<approx> t"
- apply(induct rule: alpha.induct)
- apply(simp add: a1)
- apply(simp add: a2)
- apply(rule a3)
- apply(erule alpha_gen_compose_sym)
- apply(erule alpha_eqvt)
- done
-
-lemma alpha_trans:
- shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
-apply(induct arbitrary: t3 rule: alpha.induct)
-apply(simp add: a1)
-apply(rotate_tac 4)
-apply(erule alpha.cases)
-apply(simp_all add: a2)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(rule a3)
-apply(erule alpha_gen_compose_trans)
-apply(assumption)
-apply(erule alpha_eqvt)
-done
-
-lemma alpha_equivp:
- shows "equivp alpha"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(auto intro: alpha_refl alpha_sym alpha_trans)
- done
-
-lemma alpha_rfv:
- shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
- apply(induct rule: alpha.induct)
- apply(simp_all add: alpha_gen.simps)
- done
-
-quotient_type lam = rlam / alpha
- by (rule alpha_equivp)
-
-quotient_definition
- "Var :: name \<Rightarrow> lam"
-is
- "rVar"
-
-quotient_definition
- "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-is
- "rApp"
-
-quotient_definition
- "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-is
- "rLam"
-
-quotient_definition
- "fv :: lam \<Rightarrow> atom set"
-is
- "rfv"
-
-lemma perm_rsp[quot_respect]:
- "(op = ===> alpha ===> alpha) permute permute"
- apply(auto)
- apply(rule alpha_eqvt)
- apply(simp)
- done
-
-lemma rVar_rsp[quot_respect]:
- "(op = ===> alpha) rVar rVar"
- by (auto intro: a1)
-
-lemma rApp_rsp[quot_respect]:
- "(alpha ===> alpha ===> alpha) rApp rApp"
- by (auto intro: a2)
-
-lemma rLam_rsp[quot_respect]:
- "(op = ===> alpha ===> alpha) rLam rLam"
- apply(auto)
- apply(rule a3)
- apply(rule_tac x="0" in exI)
- unfolding fresh_star_def
- apply(simp add: fresh_star_def fresh_zero_perm alpha_gen.simps)
- apply(simp add: alpha_rfv)
- done
-
-lemma rfv_rsp[quot_respect]:
- "(alpha ===> op =) rfv rfv"
-apply(simp add: alpha_rfv)
-done
-
-
-section {* lifted theorems *}
-
-lemma lam_induct:
- "\<lbrakk>\<And>name. P (Var name);
- \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
- \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk>
- \<Longrightarrow> P lam"
- apply (lifting rlam.induct)
- done
-
-instantiation lam :: pt
-begin
-
-quotient_definition
- "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
-is
- "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
-
-lemma permute_lam [simp]:
- shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
- and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
- and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
-apply(lifting permute_rlam.simps)
-done
-
-instance
-apply default
-apply(induct_tac [!] x rule: lam_induct)
-apply(simp_all)
-done
-
-end
-
-lemma fv_lam [simp]:
- shows "fv (Var a) = {atom a}"
- and "fv (App t1 t2) = fv t1 \<union> fv t2"
- and "fv (Lam a t) = fv t - {atom a}"
-apply(lifting rfv_var rfv_app rfv_lam)
-done
-
-lemma fv_eqvt:
- shows "(p \<bullet> fv t) = fv (p \<bullet> t)"
-apply(lifting rfv_eqvt)
-done
-
-lemma a1:
- "a = b \<Longrightarrow> Var a = Var b"
- by (lifting a1)
-
-lemma a2:
- "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
- by (lifting a2)
-
-lemma alpha_gen_rsp_pre:
- assumes a5: "\<And>t s. R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s)"
- and a1: "R s1 t1"
- and a2: "R s2 t2"
- and a3: "\<And>a b c d. R a b \<Longrightarrow> R c d \<Longrightarrow> R1 a c = R2 b d"
- and a4: "\<And>x y. R x y \<Longrightarrow> fv1 x = fv2 y"
- shows "(a, s1) \<approx>gen R1 fv1 pi (b, s2) = (a, t1) \<approx>gen R2 fv2 pi (b, t2)"
-apply (simp add: alpha_gen.simps)
-apply (simp only: a4[symmetric, OF a1] a4[symmetric, OF a2])
-apply auto
-apply (subst a3[symmetric])
-apply (rule a5)
-apply (rule a1)
-apply (rule a2)
-apply (assumption)
-apply (subst a3)
-apply (rule a5)
-apply (rule a1)
-apply (rule a2)
-apply (assumption)
-done
-
-lemma [quot_respect]: "(prod_rel op = alpha ===>
- (alpha ===> alpha ===> op =) ===> (alpha ===> op =) ===> op = ===> prod_rel op = alpha ===> op =)
- alpha_gen alpha_gen"
-apply simp
-apply clarify
-apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt])
-apply auto
-done
-
-(* pi_abs would be also sufficient to prove the next lemma *)
-lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
-apply (unfold rep_lam_def)
-sorry
-
-lemma [quot_preserve]: "(prod_fun id rep_lam --->
- (abs_lam ---> abs_lam ---> id) ---> (abs_lam ---> id) ---> id ---> (prod_fun id rep_lam) ---> id)
- alpha_gen = alpha_gen"
-apply (simp add: expand_fun_eq alpha_gen.simps Quotient_abs_rep[OF Quotient_lam])
-apply (simp add: replam_eqvt)
-apply (simp only: Quotient_abs_rep[OF Quotient_lam])
-apply auto
-done
-
-
-lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
-apply (simp add: expand_fun_eq)
-apply (simp add: Quotient_rel_rep[OF Quotient_lam])
-done
-
-lemma a3:
- "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s"
- apply (unfold alpha_gen)
- apply (lifting a3[unfolded alpha_gen])
- done
-
-
-lemma a3_inv:
- "Lam a t = Lam b s \<Longrightarrow> \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)"
- apply (unfold alpha_gen)
- apply (lifting a3_inverse[unfolded alpha_gen])
- done
-
-lemma alpha_cases:
- "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
- \<And>t1 t2 s1 s2. \<lbrakk>a1 = App t1 s1; a2 = App t2 s2; t1 = t2; s1 = s2\<rbrakk> \<Longrightarrow> P;
- \<And>a t b s. \<lbrakk>a1 = Lam a t; a2 = Lam b s; \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)\<rbrakk>
- \<Longrightarrow> P\<rbrakk>
- \<Longrightarrow> P"
-unfolding alpha_gen
-apply (lifting alpha.cases[unfolded alpha_gen])
-done
-
-(* not sure whether needed *)
-lemma alpha_induct:
- "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
- \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
- \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2) fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
- \<Longrightarrow> qxb qx qxa"
-unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen])
-
-(* should they lift automatically *)
-lemma lam_inject [simp]:
- shows "(Var a = Var b) = (a = b)"
- and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
-apply(lifting rlam.inject(1) rlam.inject(2))
-apply(regularize)
-prefer 2
-apply(regularize)
-prefer 2
-apply(auto)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(simp add: alpha.a1)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(rule alpha.a2)
-apply(simp_all)
-done
-
-thm a3_inv
-lemma Lam_pseudo_inject:
- shows "(Lam a t = Lam b s) = (\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s))"
-apply(rule iffI)
-apply(rule a3_inv)
-apply(assumption)
-apply(rule a3)
-apply(assumption)
-done
-
-lemma rlam_distinct:
- shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
- and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
- and "\<not>(rVar nam \<approx> rLam nam' rlam')"
- and "\<not>(rLam nam' rlam' \<approx> rVar nam)"
- and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
- and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
-apply auto
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-apply (erule alpha.cases)
-apply (simp_all only: rlam.distinct)
-done
-
-lemma lam_distinct[simp]:
- shows "Var nam \<noteq> App lam1' lam2'"
- and "App lam1' lam2' \<noteq> Var nam"
- and "Var nam \<noteq> Lam nam' lam'"
- and "Lam nam' lam' \<noteq> Var nam"
- and "App lam1 lam2 \<noteq> Lam nam' lam'"
- and "Lam nam' lam' \<noteq> App lam1 lam2"
-apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
-done
-
-lemma var_supp1:
- shows "(supp (Var a)) = (supp a)"
- apply (simp add: supp_def)
- done
-
-lemma var_supp:
- shows "(supp (Var a)) = {a:::name}"
- using var_supp1 by (simp add: supp_at_base)
-
-lemma app_supp:
- shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
-apply(simp only: supp_def lam_inject)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-done
-
-(* supp for lam *)
-lemma lam_supp1:
- shows "(supp (atom x, t)) supports (Lam x t) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
-apply(simp_all add: fresh_atom)
-done
-
-lemma lam_fsupp1:
- assumes a: "finite (supp t)"
- shows "finite (supp (Lam x t))"
-apply(rule supports_finite)
-apply(rule lam_supp1)
-apply(simp add: a supp_Pair supp_atom)
-done
-
-instance lam :: fs
-apply(default)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: var_supp)
-apply(simp add: app_supp)
-apply(simp add: lam_fsupp1)
-done
-
-lemma supp_fv:
- shows "supp t = fv t"
-apply(induct t rule: lam_induct)
-apply(simp add: var_supp)
-apply(simp add: app_supp)
-apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)")
-apply(simp add: supp_Abs)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
-apply(simp add: Lam_pseudo_inject)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen.simps)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
-done
-
-lemma lam_supp2:
- shows "supp (Lam x t) = supp (Abs {atom x} t)"
-apply(simp add: supp_def permute_set_eq atom_eqvt)
-apply(simp add: Lam_pseudo_inject)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen supp_fv)
-done
-
-lemma lam_supp:
- shows "supp (Lam x t) = ((supp t) - {atom x})"
-apply(simp add: lam_supp2)
-apply(simp add: supp_Abs)
-done
-
-lemma fresh_lam:
- "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"
-apply(simp add: fresh_def)
-apply(simp add: lam_supp)
-apply(auto)
-done
-
-lemma lam_induct_strong:
- fixes a::"'a::fs"
- assumes a1: "\<And>name b. P b (Var name)"
- and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
- and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
- shows "P a lam"
-proof -
- have "\<And>pi a. P a (pi \<bullet> lam)"
- proof (induct lam rule: lam_induct)
- case (1 name pi)
- show "P a (pi \<bullet> Var name)"
- apply (simp)
- apply (rule a1)
- done
- next
- case (2 lam1 lam2 pi)
- have b1: "\<And>pi a. P a (pi \<bullet> lam1)" by fact
- have b2: "\<And>pi a. P a (pi \<bullet> lam2)" by fact
- show "P a (pi \<bullet> App lam1 lam2)"
- apply (simp)
- apply (rule a2)
- apply (rule b1)
- apply (rule b2)
- done
- next
- case (3 name lam pi a)
- have b: "\<And>pi a. P a (pi \<bullet> lam)" by fact
- obtain c::name where fr: "atom c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)"
- apply(rule obtain_atom)
- apply(auto)
- sorry
- from b fr have p: "P a (Lam c (((c \<leftrightarrow> (pi \<bullet> name)) + pi)\<bullet>lam))"
- apply -
- apply(rule a3)
- apply(blast)
- apply(simp add: fresh_Pair)
- done
- have eq: "(atom c \<rightleftharpoons> atom (pi\<bullet>name)) \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)"
- apply(rule swap_fresh_fresh)
- using fr
- apply(simp add: fresh_lam fresh_Pair)
- apply(simp add: fresh_lam fresh_Pair)
- done
- show "P a (pi \<bullet> Lam name lam)"
- apply (simp)
- apply(subst eq[symmetric])
- using p
- apply(simp only: permute_lam)
- apply(simp add: flip_def)
- done
- qed
- then have "P a (0 \<bullet> lam)" by blast
- then show "P a lam" by simp
-qed
-
-
-lemma var_fresh:
- fixes a::"name"
- shows "(atom a \<sharp> (Var b)) = (atom a \<sharp> b)"
- apply(simp add: fresh_def)
- apply(simp add: var_supp1)
- done
-
-
-
-end
-
--- a/Nominal/Manual/Term1.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,261 +0,0 @@
-theory Term1
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-begin
-
-atom_decl name
-
-section {*** lets with binding patterns ***}
-
-datatype rtrm1 =
- rVr1 "name"
-| rAp1 "rtrm1" "rtrm1"
-| rLm1 "name" "rtrm1" --"name is bound in trm1"
-| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
-and bp =
- BUnit
-| BVr "name"
-| BPr "bp" "bp"
-
-print_theorems
-
-(* to be given by the user *)
-
-primrec
- bv1
-where
- "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *}
-thm permute_rtrm1_permute_bp.simps
-
-local_setup {*
- snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
- [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]],
- [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
-
-notation
- alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
- alpha_bp ("_ \<approx>1b _" [100, 100] 100)
-thm alpha_rtrm1_alpha_bp_alpha_bv1.intros
-(*thm fv_rtrm1_fv_bp.simps[no_vars]*)
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *}
-thm alpha1_inj
-
-local_setup {*
-snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms bv1.simps permute_rtrm1_permute_bp.simps} @{context}))
-*}
-
-local_setup {*
-snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
-*}
-
-(*local_setup {*
-snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context})
-*}
-print_theorems
-
-local_setup {*
-snd o build_eqvts @{binding fv_bp_eqvt} [@{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms fv_rtrm1_fv_bv1.simps fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
-*}
-print_theorems
-*)
-
-local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
-build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms permute_rtrm1_permute_bp.simps alpha1_inj} ctxt 1) ctxt) ctxt)) *}
-
-lemma alpha1_eqvt_proper[eqvt]:
- "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
- "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"
- apply (simp_all only: eqvts)
- apply rule
- apply (simp_all add: alpha1_eqvt)
- apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"])
- apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"])
- apply (simp_all only: alpha1_eqvt)
- apply rule
- apply (simp_all add: alpha1_eqvt)
- apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])
- apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])
- apply (simp_all only: alpha1_eqvt)
-done
-thm eqvts_raw(1)
-
-lemma "(b \<approx>1 a \<longrightarrow> a \<approx>1 b) \<and> (x \<approx>1b y \<longrightarrow> y \<approx>1b x) \<and> (alpha_bv1 x y \<longrightarrow> alpha_bv1 y x)"
-apply (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} @{context} 1 *})
-done
-
-lemma alpha1_equivp:
- "equivp alpha_rtrm1"
- "equivp alpha_bp"
-sorry
-
-(*
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
- (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
-thm alpha1_equivp*)
-
-local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
- (rtac @{thm alpha1_equivp(1)} 1) *}
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))
-*}
-print_theorems
-
-local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
- (fn _ => Skip_Proof.cheat_tac @{theory}) *}
-local_setup {* snd o prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
- (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
- (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
- (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
- (fn _ => Skip_Proof.cheat_tac @{theory}) *}
-local_setup {* snd o prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
- (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}
-
-lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
-lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
-
-setup {* define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
- @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
-
-lemmas
- permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
-and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
-and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt[quot_lifted]
-and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
-
-lemma supports:
- "(supp (atom x)) supports (Vr1 x)"
- "(supp t \<union> supp s) supports (Ap1 t s)"
- "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
- "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
- "{} supports BUnit"
- "(supp (atom x)) supports (BVr x)"
- "(supp a \<union> supp b) supports (BPr a b)"
-apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
-done
-
-prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *}
-apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *})
-done
-
-instance trm1 and bp :: fs
-apply default
-apply (simp_all add: rtrm1_bp_fs)
-done
-
-lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp"
-apply(induct bp rule: trm1_bp_inducts(2))
-apply(simp_all)
-done
-
-lemma fv_eq_bv: "fv_bp = bv1"
-apply(rule ext)
-apply(rule fv_eq_bv_pre)
-done
-
-lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
-apply auto
-apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
-apply auto
-done
-
-lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
-apply rule
-apply (induct a b rule: alpha_rtrm1_alpha_bp_alpha_bv1.inducts(2))
-apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)])
-done
-
-lemma alpha_bp_eq: "alpha_bp = (op =)"
-apply (rule ext)+
-apply (rule alpha_bp_eq_eq)
-done
-
-lemma ex_out:
- "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
- "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
- "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
- "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
- "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))"
-apply (blast)+
-done
-
-lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
-by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-
-lemma supp_fv_let:
- assumes sa : "fv_bp bp = supp bp"
- shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk>
- \<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)"
-apply(fold supp_Abs)
-apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
-apply(simp (no_asm) only: supp_def)
-apply(simp only: permute_set_eq permute_trm1)
-apply(simp only: alpha1_INJ alpha_bp_eq)
-apply(simp only: ex_out)
-apply(simp only: Collect_neg_conj)
-apply(simp only: permute_ABS)
-apply(simp only: Abs_eq_iff)
-apply(simp only: alpha_gen supp_Pair split_conv eqvts)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
-apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric])
-apply (simp only: eqvts Pair_eq)
-done
-
-lemma supp_fv:
- "supp t = fv_trm1 t"
- "supp b = fv_bp b"
-apply(induct t and b rule: trm1_bp_inducts)
-apply(simp_all)
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp only: supp_at_base[simplified supp_def])
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute)
-apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
-apply(simp add: supp_Abs fv_trm1)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
-apply(simp add: alpha1_INJ)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen.simps)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
-apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair)
-apply blast
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp only: supp_at_base[simplified supp_def])
-apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq])
-apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-apply(fold supp_def)
-apply simp
-done
-
-lemma trm1_supp:
- "supp (Vr1 x) = {atom x}"
- "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
- "supp (Lm1 x t) = (supp t) - {atom x}"
- "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
-by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
-
-lemma trm1_induct_strong:
- assumes "\<And>name b. P b (Vr1 name)"
- and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
- and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
- and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
- shows "P a rtrma"
-sorry
-
-end
--- a/Nominal/Manual/Term2.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-theory Term2
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-begin
-
-atom_decl name
-
-section {*** lets with single assignments ***}
-
-datatype rtrm2 =
- rVr2 "name"
-| rAp2 "rtrm2" "rtrm2"
-| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
-| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
-and rassign =
- rAs "name" "rtrm2"
-
-(* to be given by the user *)
-primrec
- rbv2
-where
- "rbv2 (rAs x t) = {atom x}"
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *}
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2")
- [[[],
- [],
- [(NONE, 0, 1)],
- [(SOME @{term rbv2}, 0, 1)]],
- [[]]] *}
-
-notation
- alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
- alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
-thm alpha_rtrm2_alpha_rassign.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}
-thm alpha2_inj
-
-lemma alpha2_eqvt:
- "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)"
- "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)"
-sorry
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []),
- (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}
-thm alpha2_equivp
-
-local_setup {* define_quotient_type
- [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),
- (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]
- ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))
- |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))
-*}
-print_theorems
-
-local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
- (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]
- (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]
- (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]
- (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]
- (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]
- (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]
- (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}
-
-end
--- a/Nominal/Manual/Term3.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-theory Term3
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-begin
-
-atom_decl name
-
-section {*** lets with many assignments ***}
-
-datatype rtrm3 =
- rVr3 "name"
-| rAp3 "rtrm3" "rtrm3"
-| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"
-| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"
-and rassigns =
- rANil
-| rACons "name" "rtrm3" "rassigns"
-
-(* to be given by the user *)
-primrec
- bv3
-where
- "bv3 rANil = {}"
-| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *}
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3")
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
- [[], [[], [], []]]] *}
-print_theorems
-
-notation
- alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and
- alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
-thm alpha_rtrm3_alpha_rassigns.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}
-thm alpha3_inj
-
-lemma alpha3_eqvt:
- "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"
- "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"
-sorry
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),
- (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}
-thm alpha3_equivp
-
-quotient_type
- trm3 = rtrm3 / alpha_rtrm3
-and
- assigns = rassigns / alpha_rassigns
- by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
-
-end
--- a/Nominal/Manual/Term4.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,167 +0,0 @@
-theory Term4
-imports "../NewAlpha" "../Abs" "../Perm" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
-begin
-
-atom_decl name
-
-section {*** lam with indirect list recursion ***}
-
-datatype rtrm4 =
- rVr4 "name"
-| rAp4 "rtrm4" "rtrm4 list"
-| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
-
-(* there cannot be a clause for lists, as *)
-(* permutations are already defined in Nominal (also functions, options, and so on) *)
-ML {*
- val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4";
- val {descr, sorts, ...} = dtinfo;
-*}
-setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *}
-lemmas perm = permute_rtrm4_permute_rtrm4_list.simps(1-3)
-lemma perm_fix:
- fixes ts::"rtrm4 list"
- shows "permute_rtrm4_list p ts = p \<bullet> ts"
- by (induct ts) simp_all
-lemmas perm_fixed = perm[simplified perm_fix]
-
-ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
-
-local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *}
-lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*)
-
-lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
- by (rule ext) (induct_tac x, simp_all)
-lemmas fv_fixed = fv[simplified fv_fix]
-
-(* TODO: check remove 2 *)
-local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms perm_fixed fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
-thm eqvts(1-2)
-
-local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *}
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
-lemmas alpha_inj = alpha4_inj(1-3)
-
-lemma alpha_fix: "alpha_rtrm4_list = list_all2 alpha_rtrm4"
- apply (rule ext)+
- apply (induct_tac x xa rule: list_induct2')
- apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
- apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
- apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
- apply rule
- apply (erule alpha_rtrm4_list.cases)
- apply simp_all
- apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
- apply simp_all
- done
-
-lemmas alpha_inj_fixed = alpha_inj[simplified alpha_fix (*fv_fix*)]
-
-notation
- alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
-and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
-
-declare perm_fixed[eqvt]
-equivariance alpha_rtrm4
-lemmas alpha4_eqvt = eqvts(1-2)
-lemmas alpha4_eqvt_fixed = alpha4_eqvt(2)[simplified alpha_fix (*fv_fix*)]
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
- build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
-thm alpha4_reflp
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
- (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
-lemmas alpha4_equivp_fixed = alpha4_equivp[simplified alpha_fix fv_fix]
-
-quotient_type
- trm4 = rtrm4 / alpha_rtrm4
- by (simp_all add: alpha4_equivp)
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))
- |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4}))
- |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4}))
- |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4})))
-*}
-print_theorems
-
-
-lemma fv_rtrm4_rsp:
- "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
- "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
- apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)
- apply (simp_all add: alpha_gen)
-done
-
-local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}]
- (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *}
-print_theorems
-
-local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}]
- (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
-local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
- (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
-
-lemma [quot_respect]:
- "(alpha_rtrm4 ===> list_all2 alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
- by (simp add: alpha_inj_fixed)
-
-local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
- [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
- (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
-
-setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *}
-print_theorems
-
-(* Instead of permute for trm4_list we may need the following 2 lemmas: *)
-lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute"
- apply (simp add: expand_fun_eq)
- apply clarify
- apply (rename_tac "pi" x)
- apply (induct_tac x)
- apply simp
- apply simp
- apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified])
- done
-
-lemma [quot_respect]: "(op = ===> list_all2 alpha_rtrm4 ===> list_all2 alpha_rtrm4) permute permute"
- apply simp
- apply (rule allI)+
- apply (induct_tac xa y rule: list_induct2')
- apply simp_all
- apply clarify
- apply (erule alpha4_eqvt)
- done
-
-ML {*
- map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed}
-*}
-
-ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
-
-ML {*
- map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fv_fix] fv_rtrm4_list.simps[simplified fv_fix]}
-*}
-
-ML {*
-val liftd =
- map (Local_Defs.unfold @{context} @{thms id_simps}) (
- map (Local_Defs.fold @{context} @{thms alphas}) (
- map (lift_thm [@{typ trm4}] @{context}) @{thms alpha_inj_fixed[unfolded alphas]}
- )
- )
-*}
-
-ML {*
- map (lift_thm [@{typ trm4}] @{context})
- (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
-*}
-
-thm eqvts(6-7)
-ML {*
- map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(6-7)[simplified fv_fix]}
-*}
-
-end
--- a/Nominal/Manual/Term5.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,302 +0,0 @@
-theory Term5
-imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp"
-begin
-
-atom_decl name
-
-datatype rtrm5 =
- rVr5 "name"
-| rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
- rLnil
-| rLcons "name" "rtrm5" "rlts"
-
-primrec
- rbv5
-where
- "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
- [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *}
-print_theorems
-
-notation
- alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
- alpha_rlts ("_ \<approx>l _" [100, 100] 100)
-thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
-thm alpha5_inj
-
-lemma rbv5_eqvt[eqvt]:
- "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
- apply (induct x)
- apply (simp_all add: eqvts atom_eqvt)
- done
-
-lemma fv_rtrm5_rlts_eqvt[eqvt]:
- "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
- "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
- apply (induct x and l)
- apply (simp_all add: eqvts atom_eqvt)
- done
-
-(*lemma alpha5_eqvt:
- "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
- (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
- (alpha_rbv5 b c \<longrightarrow> alpha_rbv5 (p \<bullet> b) (p \<bullet> c))"
-apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
-done*)
-
-local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []),
-build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *}
-print_theorems
-
-lemma alpha5_reflp:
-"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)"
-apply (rule rtrm5_rlts.induct)
-apply (simp_all add: alpha5_inj)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
-done
-
-lemma alpha5_symp:
-"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
-(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
-(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (simp_all add: alpha5_inj)
-apply (erule exE)
-apply (rule_tac x="-pi" in exI)
-apply (rule alpha_gen_sym)
-apply (simp_all add: alphas)
-apply (case_tac x)
-apply (case_tac y)
-apply (simp add: alpha5_eqvt)
-apply clarify
-apply simp
-done
-
-lemma alpha5_symp1:
-"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
-(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
-(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (simp_all add: alpha5_inj)
-apply (erule exE)
-apply (rule_tac x="- pi" in exI)
-apply (simp add: alpha_gen)
- apply(simp add: fresh_star_def fresh_minus_perm)
-apply clarify
-apply (rule conjI)
-apply (rotate_tac 3)
-apply (frule_tac p="- pi" in alpha5_eqvt(2))
-apply simp
-apply (rule conjI)
-apply (rotate_tac 5)
-apply (frule_tac p="- pi" in alpha5_eqvt(1))
-apply simp
-apply (rotate_tac 6)
-apply simp
-apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
-apply (simp)
-done
-
-thm alpha_gen_sym[no_vars]
-thm alpha_gen_compose_sym[no_vars]
-
-lemma tt:
- "\<lbrakk>R (- p \<bullet> x) y \<Longrightarrow> R (p \<bullet> y) x; (bs, x) \<approx>gen R f (- p) (cs, y)\<rbrakk> \<Longrightarrow> (cs, y) \<approx>gen R f p (bs, x)"
- unfolding alphas
- unfolding fresh_star_def
- by (auto simp add: fresh_minus_perm)
-
-lemma alpha5_symp2:
- shows "a \<approx>5 b \<Longrightarrow> b \<approx>5 a"
- and "x \<approx>l y \<Longrightarrow> y \<approx>l x"
- and "alpha_rbv5 x y \<Longrightarrow> alpha_rbv5 y x"
-apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
-(* non-binding case *)
-apply(simp add: alpha5_inj)
-(* non-binding case *)
-apply(simp add: alpha5_inj)
-(* binding case *)
-apply(simp add: alpha5_inj)
-apply(erule exE)
-apply(rule_tac x="- pi" in exI)
-apply(rule tt)
-apply(simp add: alphas)
-apply(erule conjE)+
-apply(drule_tac p="- pi" in alpha5_eqvt(2))
-apply(drule_tac p="- pi" in alpha5_eqvt(2))
-apply(drule_tac p="- pi" in alpha5_eqvt(1))
-apply(drule_tac p="- pi" in alpha5_eqvt(1))
-apply(simp)
-apply(simp add: alphas)
-apply(erule conjE)+
-apply metis
-(* non-binding case *)
-apply(simp add: alpha5_inj)
-(* non-binding case *)
-apply(simp add: alpha5_inj)
-(* non-binding case *)
-apply(simp add: alpha5_inj)
-(* non-binding case *)
-apply(simp add: alpha5_inj)
-done
-
-lemma alpha5_transp:
-"(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
-(x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
-(alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
-(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*)
-apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (rule_tac [!] allI)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-defer
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
-(* HERE *)
-(*
-apply(rule alpha_gen_trans)
-thm alpha_gen_trans
-defer
-apply (simp add: alpha_gen)
-apply clarify
-apply(simp add: fresh_star_plus)
-apply (rule conjI)
-apply (erule_tac x="- pi \<bullet> rltsaa" in allE)
-apply (rotate_tac 5)
-apply (drule_tac p="- pi" in alpha5_eqvt(2))
-apply simp
-apply (drule_tac p="pi" in alpha5_eqvt(2))
-apply simp
-apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE)
-apply (rotate_tac 7)
-apply (drule_tac p="- pi" in alpha5_eqvt(1))
-apply simp
-apply (rotate_tac 3)
-apply (drule_tac p="pi" in alpha5_eqvt(1))
-apply simp
-done
-*)
-sorry
-
-lemma alpha5_equivp:
- "equivp alpha_rtrm5"
- "equivp alpha_rlts"
- unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
- apply (simp_all only: alpha5_reflp)
- apply (meson alpha5_symp alpha5_transp)
- apply (meson alpha5_symp alpha5_transp)
- done
-
-quotient_type
- trm5 = rtrm5 / alpha_rtrm5
-and
- lts = rlts / alpha_rlts
- by (auto intro: alpha5_equivp)
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
- |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
-*}
-print_theorems
-
-lemma alpha5_rfv:
- "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
- "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
- "(alpha_rbv5 b c \<Longrightarrow> True)"
- apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
- apply(simp_all add: eqvts)
- apply(simp add: alpha_gen)
- apply(clarify)
- apply blast
-done
-
-lemma bv_list_rsp:
- shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
- apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
- apply(simp_all)
- apply(clarify)
- apply simp
- done
-
-local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
-print_theorems
-
-local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
-thm alpha_bn_rsp
-
-lemma [quot_respect]:
- "(alpha_rlts ===> op =) fv_rlts fv_rlts"
- "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
- "(alpha_rlts ===> op =) rbv5 rbv5"
- "(op = ===> alpha_rtrm5) rVr5 rVr5"
- "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
- "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
- "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
- "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
- "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
- "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
- apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp)
- apply (clarify)
- apply (rule_tac x="0" in exI)
- apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-done
-
-
-lemma
- shows "(alpha_rlts ===> op =) rbv5 rbv5"
- by (simp add: bv_list_rsp)
-
-lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
-
-instantiation trm5 and lts :: pt
-begin
-
-quotient_definition
- "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
-
-quotient_definition
- "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
-is
- "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
-
-instance by default
- (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
-
-end
-
-lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-lemmas bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
-lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
-lemmas alpha5_DIS = alpha_dis[quot_lifted]
-
-end
--- a/Nominal/Manual/Term5n.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,209 +0,0 @@
-theory Term5
-imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp"
-begin
-
-atom_decl name
-
-datatype rtrm5 =
- rVr5 "name"
-| rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
- rLnil
-| rLcons "name" "rtrm5" "rlts"
-
-primrec
- rbv5
-where
- "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
- [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *}
-print_theorems
-
-notation
- alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
- alpha_rlts ("_ \<approx>l _" [100, 100] 100)
-thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
-thm alpha5_inj
-
-lemma rbv5_eqvt[eqvt]:
- "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
- apply (induct x)
- apply (simp_all add: eqvts atom_eqvt)
- done
-
-lemma fv_rtrm5_rlts_eqvt[eqvt]:
- "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
- "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
- "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)"
- apply (induct x and l)
- apply (simp_all add: eqvts atom_eqvt)
- done
-
-local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []),
-build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *}
-print_theorems
-
-lemma alpha5_reflp:
-"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)"
-apply (rule rtrm5_rlts.induct)
-apply (simp_all add: alpha5_inj)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
-done
-
-lemma alpha5_symp:
-"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
-(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
-(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (simp_all add: alpha5_inj)
-apply (erule conjE)+
-apply (erule exE)
-apply (rule_tac x="-pi" in exI)
-apply (rule alpha_gen_sym)
-apply (simp add: alphas)
-apply (simp add: alpha5_eqvt)
-apply (simp add: alphas)
-apply clarify
-apply simp
-done
-
-lemma alpha5_transp:
-"(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
-(x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
-(alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
-apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (rule_tac [!] allI)
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-defer
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (erule conjE)+
-apply (erule exE)+
-apply (rule_tac x="pi + pia" in exI)
-apply (rule alpha_gen_trans)
-prefer 6
-apply assumption
-apply (simp_all add: alphas alpha5_eqvt)
-apply (clarify)
-apply simp
-done
-
-lemma alpha5_equivp:
- "equivp alpha_rtrm5"
- "equivp alpha_rlts"
- unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
- apply (simp_all only: alpha5_reflp)
- apply (meson alpha5_symp alpha5_transp)
- apply (meson alpha5_symp alpha5_transp)
- done
-
-quotient_type
- trm5 = rtrm5 / alpha_rtrm5
-and
- lts = rlts / alpha_rlts
- by (auto intro: alpha5_equivp)
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
- |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
-*}
-print_theorems
-
-lemma alpha5_rfv:
- "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
- "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"
- "(alpha_rbv5 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
- apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
- apply(simp_all)
- apply(simp add: alpha_gen)
- done
-
-lemma bv_list_rsp:
- shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
- apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
- apply(simp_all)
- apply(clarify)
- apply simp
- done
-
-local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
-print_theorems
-
-local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
-thm alpha_bn_rsp
-
-
-lemma [quot_respect]:
- "(alpha_rlts ===> op =) fv_rlts fv_rlts"
- "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5"
- "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
- "(alpha_rlts ===> op =) rbv5 rbv5"
- "(op = ===> alpha_rtrm5) rVr5 rVr5"
- "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
- "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
- "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
- "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
- "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
- "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
- apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp)
- apply (clarify)
- apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-done
-
-lemma
- shows "(alpha_rlts ===> op =) rbv5 rbv5"
- by (simp add: bv_list_rsp)
-
-lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
-
-instantiation trm5 and lts :: pt
-begin
-
-quotient_definition
- "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
-
-quotient_definition
- "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
-is
- "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
-
-instance by default
- (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
-
-end
-
-lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-lemmas bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted]
-lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]
-lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-
-end
--- a/Nominal/Manual/Term8.thy Sat Dec 17 17:08:47 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-theory Term8
-imports "../../Nominal-General/Nominal2_Atoms" "../../Nominal-General/Nominal2_Eqvt" "../../Nominal-General/Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "../../Attic/Prove"
-begin
-
-atom_decl name
-
-datatype rfoo8 =
- Foo0 "name"
-| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
-and rbar8 =
- Bar0 "name"
-| Bar1 "name" "name" "rbar8" --"bind second name in b"
-
-primrec
- rbv8
-where
- "rbv8 (Bar0 x) = {}"
-| "rbv8 (Bar1 v x b) = {atom v}"
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *}
-print_theorems
-
-ML define_fv_alpha_export
-local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term8.rfoo8") [
- [[], [(SOME (@{term rbv8}, false), 0, 1, AlphaGen)]], [[], [(NONE, 1, 2, AlphaGen)]]]
- [(@{term "rbv8"}, 1, [[], [(0, NONE), (2, SOME @{term rbv8})]])] *}
-notation
- alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
- alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
-thm alpha_rfoo8_alpha_rbar8_alpha_rbv8.intros[no_vars]
-thm fv_rbar8.simps fv_rfoo8_fv_rbv8.simps
-
-inductive
- alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
-and
- alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
-and
- alpha8bv:: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>bv _" [100, 100] 100)
-where
- "name = namea \<Longrightarrow> Foo0 name \<approx>f Foo0 namea"
-| "\<exists>pi. rbar8 \<approx>bv rbar8a \<and>
- (rbv8 rbar8, rfoo8) \<approx>gen alpha8f fv_rfoo8 pi (rbv8 rbar8a, rfoo8a) \<Longrightarrow>
- Foo1 rbar8 rfoo8 \<approx>f Foo1 rbar8a rfoo8a"
-| "name = namea \<Longrightarrow> Bar0 name \<approx>b Bar0 namea"
-| "\<exists>pi. name1 = name1a \<and> ({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow>
- Bar1 name1 name2 rbar8 \<approx>b Bar1 name1a name2a rbar8a"
-| "name = namea \<Longrightarrow> alpha8bv (Bar0 name) (Bar0 namea)"
-| "({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow>
- alpha8bv (Bar1 name1 name2 rbar8) (Bar1 name1a name2a rbar8a)"
-
-lemma "(alpha8b ===> op =) rbv8 rbv8"
- apply rule
- apply (induct_tac a b rule: alpha8f_alpha8b_alpha8bv.inducts(2))
- apply (simp_all)
- done
-
-lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
- apply (erule alpha8f_alpha8b_alpha8bv.inducts(2))
- apply (simp_all add: alpha_gen)
- apply clarify
- sorry
-
-lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
- apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
- done
-
-lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
- apply simp apply clarify
- apply (erule alpha8f_alpha8b_alpha8bv.inducts(1))
- apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
-
-done
-
-end