# HG changeset patch # User Christian Urban # Date 1324141811 0 # Node ID 7eb352826b429e1856627fe2a711694333d72b3f # Parent 11f6a561eb4b6be07f3e70e0cf8f2534ba580971 deleted Manual directory in stable branch diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/LamEx.thy --- 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 \ atom set" -where - rfv_var: "rfv (rVar a) = {atom a}" -| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \ (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 \ a)" -| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)" -| "permute_rlam pi (rLam a t) = rLam (pi \ a) (permute_rlam pi t)" - -instance -apply default -apply(induct_tac [!] x) -apply(simp_all) -done - -end - -instantiation rlam :: fs -begin - -lemma neg_conj: - "\(P \ Q) \ (\P) \ (\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\rfv t) = rfv (pi\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 \ rlam \ bool" ("_ \a _" [100, 100] 100) -where - a1: "a = b \ (rVar a) \a (rVar b)" -| a2: "\t1 \a t2; s1 \a s2\ \ rApp t1 s1 \a rApp t2 s2" -| a3: "\pi. (rfv t - {atom a} = rfv s - {atom b} \ (rfv t - {atom a})\* pi \ (pi \ t) \a s) - \ rLam a t \a rLam b s" - -lemma a3_inverse: - assumes "rLam a t \a rLam b s" - shows "\pi. (rfv t - {atom a} = rfv s - {atom b} \ (rfv t - {atom a})\* pi \ (pi \ t) \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 \a s \ (pi \ t) \a (pi \ 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 \ 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 \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 \a s \ s \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 \a t2 \ t2 \a t3 \ t1 \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 \ 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 \a s \ rfv t = rfv s" - apply(induct rule: alpha.induct) - apply(simp_all) - done - -inductive - alpha2 :: "rlam \ rlam \ bool" ("_ \a2 _" [100, 100] 100) -where - a21: "a = b \ (rVar a) \a2 (rVar b)" -| a22: "\t1 \a2 t2; s1 \a2 s2\ \ rApp t1 s1 \a2 rApp t2 s2" -| a23: "(a = b \ t \a2 s) \ (a \ b \ ((a \ b) \ t) \a2 s \ atom b \ rfv t)\ rLam a t \a2 rLam b s" - -lemma fv_vars: - fixes a::name - assumes a1: "\x \ rfv t - {atom a}. pi \ x = x" - shows "(pi \ t) \a2 ((a \ (pi \ a)) \ 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 \a2 s" - shows "t \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 \ 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 \ (rfv t - {atom a})") -apply(subgoal_tac "atom b \ (rfv t - {atom a})") - -defer -sorry - -lemma - assumes a1: "t \a s" - shows "t \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 \ lam" -is - "rVar" - -quotient_definition - "App :: lam \ lam \ lam" -is - "rApp" - -quotient_definition - "Lam :: name \ lam \ lam" -is - "rLam" - -quotient_definition - "fv :: lam \ 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: - "\\name. P (Var name); - \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); - \name lam. P lam \ P (Lam name lam)\ - \ P lam" - apply (lifting rlam.induct) - done - -instantiation lam :: pt -begin - -quotient_definition - "permute_lam :: perm \ lam \ lam" -is - "permute :: perm \ rlam \ rlam" - -lemma permute_lam [simp]: - shows "pi \ Var a = Var (pi \ a)" - and "pi \ App t1 t2 = App (pi \ t1) (pi \ t2)" - and "pi \ Lam a t = Lam (pi \ a) (pi \ 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 \ 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 \ fv t) = fv (p \ t)" -apply(lifting rfv_eqvt) -done - -lemma a1: - "a = b \ Var a = Var b" - by (lifting a1) - -lemma a2: - "\x = xa; xb = xc\ \ App x xb = App xa xc" - by (lifting a2) - -lemma a3: - "\\pi. (fv t - {atom a} = fv s - {atom b} \ (fv t - {atom a})\* pi \ (pi \ t) = s)\ - \ Lam a t = Lam b s" - apply (lifting a3) - done - -lemma a3_inv: - assumes "Lam a t = Lam b s" - shows "\pi. (fv t - {atom a} = fv s - {atom b} \ (fv t - {atom a})\* pi \ (pi \ t) = s)" -using assms -apply(lifting a3_inverse) -done - -lemma alpha_cases: - "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; - \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; - \t a s b. \a1 = Lam a t; a2 = Lam b s; - \pi. fv t - {atom a} = fv s - {atom b} \ (fv t - {atom a}) \* pi \ (pi \ t) = s\ - \ P\ - \ P" - by (lifting alpha.cases) - -(* not sure whether needed *) -lemma alpha_induct: - "\qx = qxa; \a b. a = b \ qxb (Var a) (Var b); - \x xa xb xc. \x = xa; qxb x xa; xb = xc; qxb xb xc\ \ qxb (App x xb) (App xa xc); - \t a s b. - \\pi. fv t - {atom a} = fv s - {atom b} \ - (fv t - {atom a}) \* pi \ ((pi \ t) = s \ qxb (pi \ t) s)\ - \ qxb (Lam a t) (Lam b s)\ - \ 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 \ 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) = - (\pi. (fv t - {atom a} = fv s - {atom b} \ (fv t - {atom a})\* pi \ (pi \ t) = s))" -apply(rule iffI) -apply(rule a3_inv) -apply(assumption) -apply(rule a3) -apply(assumption) -done - -lemma rlam_distinct: - shows "\(rVar nam \a rApp rlam1' rlam2')" - and "\(rApp rlam1' rlam2' \a rVar nam)" - and "\(rVar nam \a rLam nam' rlam')" - and "\(rLam nam' rlam' \a rVar nam)" - and "\(rApp rlam1 rlam2 \a rLam nam' rlam')" - and "\(rLam nam' rlam' \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 \ App lam1' lam2'" - and "App lam1' lam2' \ Var nam" - and "Var nam \ Lam nam' lam'" - and "Lam nam' lam' \ Var nam" - and "App lam1 lam2 \ Lam nam' lam'" - and "Lam nam' lam' \ 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) \ (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 \ Lam b t) \ (a = b) \ (a \ b \ atom a \ t)" -apply(simp add: fresh_def) -apply(simp add: lam_supp) -apply(auto) -done - -lemma lam_induct_strong: - fixes a::"'a::fs" - assumes a1: "\name b. P b (Var name)" - and a2: "\lam1 lam2 b. \\c. P c lam1; \c. P c lam2\ \ P b (App lam1 lam2)" - and a3: "\name lam b. \\c. P c lam; (atom name) \ b\ \ P b (Lam name lam)" - shows "P a lam" -proof - - have "\pi a. P a (pi \ lam)" - proof (induct lam rule: lam_induct) - case (1 name pi) - show "P a (pi \ Var name)" - apply (simp) - apply (rule a1) - done - next - case (2 lam1 lam2 pi) - have b1: "\pi a. P a (pi \ lam1)" by fact - have b2: "\pi a. P a (pi \ lam2)" by fact - show "P a (pi \ App lam1 lam2)" - apply (simp) - apply (rule a2) - apply (rule b1) - apply (rule b2) - done - next - case (3 name lam pi a) - have b: "\pi a. P a (pi \ lam)" by fact - obtain c::name where fr: "atom c\(a, pi\name, pi\lam)" - apply(rule obtain_atom) - apply(auto) - sorry - from b fr have p: "P a (Lam c (((c \ (pi \ name)) + pi)\lam))" - apply - - apply(rule a3) - apply(blast) - apply(simp add: fresh_Pair) - done - have eq: "(atom c \ atom (pi\name)) \ Lam (pi \ name) (pi \ lam) = Lam (pi \ name) (pi \ 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 \ 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 \ lam)" by blast - then show "P a lam" by simp -qed - - -lemma var_fresh: - fixes a::"name" - shows "(atom a \ (Var b)) = (atom a \ b)" - apply(simp add: fresh_def) - apply(simp add: var_supp1) - done - - - -end - diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/LamEx2.thy --- 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 \ atom set" -where - rfv_var: "rfv (rVar a) = {atom a}" -| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \ (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 \ a)" -| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)" -| "permute_rlam pi (rLam a t) = rLam (pi \ a) (permute_rlam pi t)" - -instance -apply default -apply(induct_tac [!] x) -apply(simp_all) -done - -end - -instantiation rlam :: fs -begin - -lemma neg_conj: - "\(P \ Q) \ (\P) \ (\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\rfv t) = rfv (pi\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 \ rlam \ bool" ("_ \ _" [100, 100] 100) -where - a1: "a = b \ (rVar a) \ (rVar b)" -| a2: "\t1 \ t2; s1 \ s2\ \ rApp t1 s1 \ rApp t2 s2" -| a3: "\pi. (({atom a}, t) \gen alpha rfv pi ({atom b}, s)) \ rLam a t \ rLam b s" -print_theorems -thm alpha.induct - -lemma a3_inverse: - assumes "rLam a t \ rLam b s" - shows "\pi. (({atom a}, t) \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 \ s \ (pi \ t) \ (pi \ 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 \ 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 \ s \ s \ 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 \ t2 \ t2 \ t3 \ t1 \ 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 \ s \ 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 \ lam" -is - "rVar" - -quotient_definition - "App :: lam \ lam \ lam" -is - "rApp" - -quotient_definition - "Lam :: name \ lam \ lam" -is - "rLam" - -quotient_definition - "fv :: lam \ 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: - "\\name. P (Var name); - \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); - \name lam. P lam \ P (Lam name lam)\ - \ P lam" - apply (lifting rlam.induct) - done - -instantiation lam :: pt -begin - -quotient_definition - "permute_lam :: perm \ lam \ lam" -is - "permute :: perm \ rlam \ rlam" - -lemma permute_lam [simp]: - shows "pi \ Var a = Var (pi \ a)" - and "pi \ App t1 t2 = App (pi \ t1) (pi \ t2)" - and "pi \ Lam a t = Lam (pi \ a) (pi \ 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 \ 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 \ fv t) = fv (p \ t)" -apply(lifting rfv_eqvt) -done - -lemma a1: - "a = b \ Var a = Var b" - by (lifting a1) - -lemma a2: - "\x = xa; xb = xc\ \ App x xb = App xa xc" - by (lifting a2) - -lemma alpha_gen_rsp_pre: - assumes a5: "\t s. R t s \ R (pi \ t) (pi \ s)" - and a1: "R s1 t1" - and a2: "R s2 t2" - and a3: "\a b c d. R a b \ R c d \ R1 a c = R2 b d" - and a4: "\x y. R x y \ fv1 x = fv2 y" - shows "(a, s1) \gen R1 fv1 pi (b, s2) = (a, t1) \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 \ (rep_lam x) = rep_lam (pi \ 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: - "\pi. ({atom a}, t) \gen (op =) fv pi ({atom b}, s) \ 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 \ \pi. ({atom a}, t) \gen (op =) fv pi ({atom b}, s)" - apply (unfold alpha_gen) - apply (lifting a3_inverse[unfolded alpha_gen]) - done - -lemma alpha_cases: - "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; - \t1 t2 s1 s2. \a1 = App t1 s1; a2 = App t2 s2; t1 = t2; s1 = s2\ \ P; - \a t b s. \a1 = Lam a t; a2 = Lam b s; \pi. ({atom a}, t) \gen (op =) fv pi ({atom b}, s)\ - \ P\ - \ P" -unfolding alpha_gen -apply (lifting alpha.cases[unfolded alpha_gen]) -done - -(* not sure whether needed *) -lemma alpha_induct: - "\qx = qxa; \a b. a = b \ qxb (Var a) (Var b); - \x xa xb xc. \x = xa; qxb x xa; xb = xc; qxb xb xc\ \ qxb (App x xb) (App xa xc); - \a t b s. \pi. ({atom a}, t) \gen (\x1 x2. x1 = x2 \ qxb x1 x2) fv pi ({atom b}, s) \ qxb (Lam a t) (Lam b s)\ - \ 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 \ 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) = (\pi. ({atom a}, t) \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 "\(rVar nam \ rApp rlam1' rlam2')" - and "\(rApp rlam1' rlam2' \ rVar nam)" - and "\(rVar nam \ rLam nam' rlam')" - and "\(rLam nam' rlam' \ rVar nam)" - and "\(rApp rlam1 rlam2 \ rLam nam' rlam')" - and "\(rLam nam' rlam' \ 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 \ App lam1' lam2'" - and "App lam1' lam2' \ Var nam" - and "Var nam \ Lam nam' lam'" - and "Lam nam' lam' \ Var nam" - and "App lam1 lam2 \ Lam nam' lam'" - and "Lam nam' lam' \ 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) \ (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 \ Lam b t) \ (a = b) \ (a \ b \ atom a \ t)" -apply(simp add: fresh_def) -apply(simp add: lam_supp) -apply(auto) -done - -lemma lam_induct_strong: - fixes a::"'a::fs" - assumes a1: "\name b. P b (Var name)" - and a2: "\lam1 lam2 b. \\c. P c lam1; \c. P c lam2\ \ P b (App lam1 lam2)" - and a3: "\name lam b. \\c. P c lam; (atom name) \ b\ \ P b (Lam name lam)" - shows "P a lam" -proof - - have "\pi a. P a (pi \ lam)" - proof (induct lam rule: lam_induct) - case (1 name pi) - show "P a (pi \ Var name)" - apply (simp) - apply (rule a1) - done - next - case (2 lam1 lam2 pi) - have b1: "\pi a. P a (pi \ lam1)" by fact - have b2: "\pi a. P a (pi \ lam2)" by fact - show "P a (pi \ App lam1 lam2)" - apply (simp) - apply (rule a2) - apply (rule b1) - apply (rule b2) - done - next - case (3 name lam pi a) - have b: "\pi a. P a (pi \ lam)" by fact - obtain c::name where fr: "atom c\(a, pi\name, pi\lam)" - apply(rule obtain_atom) - apply(auto) - sorry - from b fr have p: "P a (Lam c (((c \ (pi \ name)) + pi)\lam))" - apply - - apply(rule a3) - apply(blast) - apply(simp add: fresh_Pair) - done - have eq: "(atom c \ atom (pi\name)) \ Lam (pi \ name) (pi \ lam) = Lam (pi \ name) (pi \ 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 \ 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 \ lam)" by blast - then show "P a lam" by simp -qed - - -lemma var_fresh: - fixes a::"name" - shows "(atom a \ (Var b)) = (atom a \ b)" - apply(simp add: fresh_def) - apply(simp add: var_supp1) - done - - - -end - diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term1.thy --- 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) \ (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 ("_ \1 _" [100, 100] 100) and - alpha_bp ("_ \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 \ (t \1 s) = ((pi \ t) \1 (pi \ s))" - "pi \ (alpha_bp a b) = (alpha_bp (pi \ a) (pi \ 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 \1 a \ a \1 b) \ (x \1b y \ y \1b x) \ (alpha_bv1 x y \ 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 \ rtrm1 \ 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 \ rtrm1 \ 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 \ supp s) supports (Ap1 t s)" - "(supp (atom x) \ supp t) supports (Lm1 x t)" - "(supp b \ supp t \ supp s) supports (Lt1 b t s)" - "{} supports BUnit" - "(supp (atom x)) supports (BVr x)" - "(supp a \ 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. \pi. pi \ (a \ b) \ bp \ bp} = {}" -apply auto -apply (rule_tac x="(x \ 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: - "(\x. Z x \ Q) = (Q \ (\x. Z x))" - "(\x. Q \ Z x) = (Q \ (\x. Z x))" - "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" - "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" - "(\x. Q \ P x \ Z x \ W x) = (Q \ (\x. P x \ Z x \ W x))" -apply (blast)+ -done - -lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" -by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) - -lemma supp_fv_let: - assumes sa : "fv_bp bp = supp bp" - shows "\fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\ - \ supp (Lt1 bp ta tb) = supp ta \ (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 \ supp t2" - "supp (Lm1 x t) = (supp t) - {atom x}" - "supp (Lt1 b t s) = supp t \ (supp s - bv1 b)" -by (simp_all add: supp_fv fv_trm1 fv_eq_bv) - -lemma trm1_induct_strong: - assumes "\name b. P b (Vr1 name)" - and "\rtrm11 rtrm12 b. \\c. P c rtrm11; \c. P c rtrm12\ \ P b (Ap1 rtrm11 rtrm12)" - and "\name rtrm1 b. \\c. P c rtrm1; (atom name) \ b\ \ P b (Lm1 name rtrm1)" - and "\bp rtrm11 rtrm12 b. \\c. P c rtrm11; \c. P c rtrm12; bv1 bp \* b\ \ P b (Lt1 bp rtrm11 rtrm12)" - shows "P a rtrma" -sorry - -end diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term2.thy --- 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 ("_ \2 _" [100, 100] 100) and - alpha_rassign ("_ \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 \2 s \ (pi \ t) \2 (pi \ s)" - "a \2b b \ (pi \ a) \2b (pi \ 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 \ rtrm2 \ rtrm2"}] - (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} - -end diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term3.thy --- 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} \ (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 ("_ \3 _" [100, 100] 100) and - alpha_rassigns ("_ \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 \3 s \ (pi \ t) \3 (pi \ s)" - "a \3a b \ (pi \ a) \3a (pi \ 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 diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term4.thy --- 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 \ 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 ("_ \4 _" [100, 100] 100) -and alpha_rtrm4_list ("_ \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 \4 ya \ fv_rtrm4 xa = fv_rtrm4 ya" - "x \4l y \ 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 \ rtrm4 \ 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 \ rtrm4 \ 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 diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term5.thy --- 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} \ (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 ("_ \5 _" [100, 100] 100) and - alpha_rlts ("_ \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 \ (rbv5 x) = rbv5 (pi \ x)" - apply (induct x) - apply (simp_all add: eqvts atom_eqvt) - done - -lemma fv_rtrm5_rlts_eqvt[eqvt]: - "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" - "pi \ (fv_rlts l) = fv_rlts (pi \ l)" - apply (induct x and l) - apply (simp_all add: eqvts atom_eqvt) - done - -(*lemma alpha5_eqvt: - "(xa \5 y \ (p \ xa) \5 (p \ y)) \ - (xb \l ya \ (p \ xb) \l (p \ ya)) \ - (alpha_rbv5 b c \ alpha_rbv5 (p \ b) (p \ 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 \5 y \ (x \l x \ 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 \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ 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 \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ 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: - "\R (- p \ x) y \ R (p \ y) x; (bs, x) \gen R f (- p) (cs, y)\ \ (cs, y) \gen R f p (bs, x)" - unfolding alphas - unfolding fresh_star_def - by (auto simp add: fresh_minus_perm) - -lemma alpha5_symp2: - shows "a \5 b \ b \5 a" - and "x \l y \ y \l x" - and "alpha_rbv5 x y \ 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 \5 b \ (\c. b \5 c \ a \5 c)) \ -(x \l y \ (\z. y \l z \ x \l z)) \ -(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ 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 \ 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 \ 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 \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ fv_rlts l = fv_rlts m)" - "(alpha_rbv5 b c \ 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 \l y \ 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 \ trm5 \ trm5" -is - "permute :: perm \ rtrm5 \ rtrm5" - -quotient_definition - "permute_lts :: perm \ lts \ lts" -is - "permute :: perm \ rlts \ 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 diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term5n.thy --- 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} \ (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 ("_ \5 _" [100, 100] 100) and - alpha_rlts ("_ \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 \ (rbv5 x) = rbv5 (pi \ x)" - apply (induct x) - apply (simp_all add: eqvts atom_eqvt) - done - -lemma fv_rtrm5_rlts_eqvt[eqvt]: - "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" - "pi \ (fv_rlts l) = fv_rlts (pi \ l)" - "pi \ (fv_rbv5 l) = fv_rbv5 (pi \ 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 \5 y \ (x \l x \ 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 \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ 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 \5 b \ (\c. b \5 c \ a \5 c)) \ -(x \l y \ (\z. y \l z \ x \l z)) \ -(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ 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 \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ (fv_rlts l = fv_rlts m \ fv_rbv5 l = fv_rbv5 m))" - "(alpha_rbv5 b c \ 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 \l y \ 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 \ trm5 \ trm5" -is - "permute :: perm \ rtrm5 \ rtrm5" - -quotient_definition - "permute_lts :: perm \ lts \ lts" -is - "permute :: perm \ rlts \ 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 diff -r 11f6a561eb4b -r 7eb352826b42 Nominal/Manual/Term8.thy --- 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 ("_ \f' _" [100, 100] 100) and - alpha_rbar8 ("_ \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 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) -and - alpha8b :: "rbar8 \ rbar8 \ bool" ("_ \b _" [100, 100] 100) -and - alpha8bv:: "rbar8 \ rbar8 \ bool" ("_ \bv _" [100, 100] 100) -where - "name = namea \ Foo0 name \f Foo0 namea" -| "\pi. rbar8 \bv rbar8a \ - (rbv8 rbar8, rfoo8) \gen alpha8f fv_rfoo8 pi (rbv8 rbar8a, rfoo8a) \ - Foo1 rbar8 rfoo8 \f Foo1 rbar8a rfoo8a" -| "name = namea \ Bar0 name \b Bar0 namea" -| "\pi. name1 = name1a \ ({atom name2}, rbar8) \gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \ - Bar1 name1 name2 rbar8 \b Bar1 name1a name2a rbar8a" -| "name = namea \ alpha8bv (Bar0 name) (Bar0 namea)" -| "({atom name2}, rbar8) \gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \ - 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 \b y \ 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