Move manual examples to a subdirectory.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term1.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,261 @@
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term2.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,81 @@
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term3.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,55 @@
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term4.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,121 @@
+theory Term4
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List"
+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)"
+print_theorems
+
+thm rtrm4.recs
+
+(* there cannot be a clause for lists, as *)
+(* permutations are already defined in Nominal (also functions, options, and so on) *)
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
+
+(* "repairing" of the permute function *)
+lemma repaired:
+ fixes ts::"rtrm4 list"
+ shows "permute_rtrm4_list p ts = p \<bullet> ts"
+ apply(induct ts)
+ apply(simp_all)
+ done
+
+thm permute_rtrm4_permute_rtrm4_list.simps
+thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
+ [[[], [], [(NONE, 0,1)]], [[], []] ] *}
+print_theorems
+
+lemma fix2: "alpha_rtrm4_list = list_rel 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
+
+(* We need sth like:
+lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
+
+notation
+ alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
+ alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
+thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
+thm alpha4_inj
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_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)) *}
+thm alpha4_inj_no
+
+local_setup {*
+snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
+*}
+print_theorems
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
+ build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+*}
+lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
+ (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
+lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
+
+(*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*)
+
+
+quotient_type
+ trm4 = rtrm4 / alpha_rtrm4
+(*and
+ trm4list = "rtrm4 list" / alpha_rtrm4_list*)
+ 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 ("Ap4", @{term rAp4}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4})))
+*}
+print_theorems
+
+local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}]
+ (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 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} @{thms alpha4_equivp} 1) *}
+lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
+apply simp
+apply clarify
+apply (simp add: alpha4_inj)
+
+
+local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}]
+ (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
+local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp}
+ [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}]
+ (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
+
+thm rtrm4.induct
+lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term5.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,344 @@
+theory Term5
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+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, 2]])] *}
+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_alpha_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 (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
+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]
+
+(* why is this not in Isabelle? *)
+lemma set_sub: "{a, b} - {b} = {a} - {b}"
+by auto
+
+lemma lets_bla:
+ "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
+apply (simp only: alpha5_INJ bv5)
+apply simp
+apply (rule allI)
+apply (simp_all add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
+apply (rule impI)
+apply (rule impI)
+apply (rule impI)
+apply (simp add: set_sub)
+done
+
+lemma lets_ok:
+ "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+thm alpha5_INJ
+apply (simp only: alpha5_INJ)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp_all add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
+apply (simp add: eqvts)
+done
+
+lemma lets_ok3:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
+done
+
+
+lemma lets_not_ok1:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp add: alpha5_INJ alpha_gen)
+apply (simp add: permute_trm5_lts eqvts)
+apply (simp add: alpha5_INJ)
+done
+
+lemma lets_nok:
+ "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
+apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term5n.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,228 @@
+theory Term5
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+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, 2]])] *}
+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_alpha_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)"
+sorry
+
+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))"
+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 ("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]
+
+lemma lets_bla:
+ "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
+apply (simp only: alpha5_INJ)
+apply (simp only: bv5)
+apply simp
+done
+
+lemma lets_ok:
+ "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+apply (simp add: alpha5_INJ)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp_all add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def eqvts)
+done
+
+lemma lets_ok3:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
+done
+
+
+lemma lets_not_ok1:
+ "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+ (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp add: alpha5_INJ alpha_gen)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
+apply blast
+done
+
+lemma distinct_helper:
+ shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
+ apply auto
+ apply (erule alpha_rtrm5.cases)
+ apply (simp_all only: rtrm5.distinct)
+ done
+
+lemma distinct_helper2:
+ shows "(Vr5 x) \<noteq> (Ap5 y z)"
+ by (lifting distinct_helper)
+
+lemma lets_nok:
+ "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
+apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term8.thy Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,61 @@
+theory Term8
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../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
+
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [
+ [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+notation
+ alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
+ alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
+thm alpha_rfoo8_alpha_rbar8.intros
+
+
+inductive
+ alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
+and
+ alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+where
+ a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
+| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
+| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
+| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
+
+lemma "(alpha8b ===> op =) rbv8 rbv8"
+ apply simp apply clarify
+ apply (erule alpha8f_alpha8b.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.inducts(2))
+ apply (simp_all add: alpha_gen)
+done
+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.inducts(1))
+ apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
+done
+
+end
--- a/Nominal/Term1.thy Tue Mar 23 08:16:39 2010 +0100
+++ /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/Term2.thy Tue Mar 23 08:16:39 2010 +0100
+++ /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/Term3.thy Tue Mar 23 08:16:39 2010 +0100
+++ /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/Term4.thy Tue Mar 23 08:16:39 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-theory Term4
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List"
-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)"
-print_theorems
-
-thm rtrm4.recs
-
-(* there cannot be a clause for lists, as *)
-(* permutations are already defined in Nominal (also functions, options, and so on) *)
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
-
-(* "repairing" of the permute function *)
-lemma repaired:
- fixes ts::"rtrm4 list"
- shows "permute_rtrm4_list p ts = p \<bullet> ts"
- apply(induct ts)
- apply(simp_all)
- done
-
-thm permute_rtrm4_permute_rtrm4_list.simps
-thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
- [[[], [], [(NONE, 0,1)]], [[], []] ] *}
-print_theorems
-
-lemma fix2: "alpha_rtrm4_list = list_rel 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
-
-(* We need sth like:
-lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
-
-notation
- alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
- alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
-thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
-thm alpha4_inj
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_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)) *}
-thm alpha4_inj_no
-
-local_setup {*
-snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
-*}
-print_theorems
-
-local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
- build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
-*}
-lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
- (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
-lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
-
-(*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*)
-
-
-quotient_type
- trm4 = rtrm4 / alpha_rtrm4
-(*and
- trm4list = "rtrm4 list" / alpha_rtrm4_list*)
- 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 ("Ap4", @{term rAp4}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4})))
-*}
-print_theorems
-
-local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}]
- (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 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} @{thms alpha4_equivp} 1) *}
-lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
-apply simp
-apply clarify
-apply (simp add: alpha4_inj)
-
-
-local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}]
- (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp}
- [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}]
- (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
-
-thm rtrm4.induct
-lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]
-
-end
--- a/Nominal/Term5.thy Tue Mar 23 08:16:39 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,344 +0,0 @@
-theory Term5
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-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, 2]])] *}
-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_alpha_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 (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
-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]
-
-(* why is this not in Isabelle? *)
-lemma set_sub: "{a, b} - {b} = {a} - {b}"
-by auto
-
-lemma lets_bla:
- "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
-apply (simp only: alpha5_INJ bv5)
-apply simp
-apply (rule allI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
-apply (rule impI)
-apply (rule impI)
-apply (rule impI)
-apply (simp add: set_sub)
-done
-
-lemma lets_ok:
- "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-thm alpha5_INJ
-apply (simp only: alpha5_INJ)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (simp add: eqvts)
-done
-
-lemma lets_ok3:
- "x \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
-done
-
-
-lemma lets_not_ok1:
- "x \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: alpha5_INJ alpha_gen)
-apply (simp add: permute_trm5_lts eqvts)
-apply (simp add: alpha5_INJ)
-done
-
-lemma lets_nok:
- "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
-done
-
-end
--- a/Nominal/Term5n.thy Tue Mar 23 08:16:39 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,228 +0,0 @@
-theory Term5
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-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, 2]])] *}
-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_alpha_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)"
-sorry
-
-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))"
-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 ("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]
-
-lemma lets_bla:
- "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
-apply (simp only: alpha5_INJ)
-apply (simp only: bv5)
-apply simp
-done
-
-lemma lets_ok:
- "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (simp add: alpha5_INJ)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def eqvts)
-done
-
-lemma lets_ok3:
- "x \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
-done
-
-
-lemma lets_not_ok1:
- "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
- (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: alpha5_INJ alpha_gen)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
-apply blast
-done
-
-lemma distinct_helper:
- shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
- apply auto
- apply (erule alpha_rtrm5.cases)
- apply (simp_all only: rtrm5.distinct)
- done
-
-lemma distinct_helper2:
- shows "(Vr5 x) \<noteq> (Ap5 y z)"
- by (lifting distinct_helper)
-
-lemma lets_nok:
- "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
-done
-
-end
--- a/Nominal/Term8.thy Tue Mar 23 08:16:39 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-theory Term8
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../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
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [
- [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
-notation
- alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
- alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
-thm alpha_rfoo8_alpha_rbar8.intros
-
-
-inductive
- alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
-and
- alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
-| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
-| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
-| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
-
-lemma "(alpha8b ===> op =) rbv8 rbv8"
- apply simp apply clarify
- apply (erule alpha8f_alpha8b.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.inducts(2))
- apply (simp_all add: alpha_gen)
-done
-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.inducts(1))
- apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
-done
-
-end