--- a/Nominal/Terms.thy Thu Feb 25 12:32:15 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1006 +0,0 @@
-theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-begin
-
-atom_decl name
-
-text {* primrec seems to be genarally faster than fun *}
-
-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 ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
-thm permute_rtrm1_permute_bp.simps
-
-local_setup {*
- snd o define_fv_alpha "Terms.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
- [[], [[]], [[], []]]] *}
-
-notation
- alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
- alpha_bp ("_ \<approx>1b _" [100, 100] 100)
-thm alpha_rtrm1_alpha_bp.intros
-thm fv_rtrm1_fv_bp.simps
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
-thm alpha1_inj
-
-local_setup {*
-snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})
-*}
-
-local_setup {*
-snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}
-*}
-
-
-local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
- build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt))
-*}
-print_theorems
-
-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
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
- (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.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
-
-thm alpha_rtrm1_alpha_bp.induct
-local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
- (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *}
-local_setup {* 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 {* 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 {* 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 {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
- (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* 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 ["Terms.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(1)[quot_lifted]
-and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, 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(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
-apply(rule_tac [!] allI)+
-apply(rule_tac [!] impI)
-apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
-apply(simp_all add: fresh_atom)
-done
-
-lemma rtrm1_bp_fs:
- "finite (supp (x :: trm1))"
- "finite (supp (b :: bp))"
- apply (induct x and b rule: trm1_bp_inducts)
- apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
- apply(simp_all add: supp_atom)
- done
-
-instance trm1 :: fs
-apply default
-apply (rule rtrm1_bp_fs(1))
-done
-
-lemma fv_eq_bv: "fv_bp bp = bv1 bp"
-apply(induct bp rule: trm1_bp_inducts(2))
-apply(simp_all)
-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.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 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)
-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(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
-apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
-apply(simp (no_asm) add: supp_def permute_trm1)
-apply(simp add: alpha1_INJ alpha_bp_eq)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
-apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
-apply(simp (no_asm) add: supp_def eqvts)
-apply(fold supp_def)
-apply(simp add: supp_at_base)
-apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
-apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
-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
-
-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 ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
-
-local_setup {* snd o define_fv_alpha "Terms.rtrm2"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
- [[[], []]]] *}
-
-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 {* 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 {* 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 {* 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 {* 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 {* 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 {* 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 {* 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) *}
-
-
-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 ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *}
-
-local_setup {* snd o define_fv_alpha "Terms.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))
-
-
-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 ["rtrm4"] ["Terms.rtrm4"] *}
-
-(* "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 "Terms.rtrm4" [
- [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
-print_theorems
-
-notation
- alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
- alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
-thm alpha_rtrm4_alpha_rtrm4_list.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (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
-thm alpha_rtrm4_alpha_rtrm4_list.induct
-
-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}, []),
- 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} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
-*}
-print_theorems
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
- (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} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
-thm alpha4_equivp
-
-quotient_type
- qrtrm4 = rtrm4 / alpha_rtrm4 and
- qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
- by (simp_all add: alpha4_equivp)
-
-
-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 ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
- [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *}
-print_theorems
-
-(* Alternate version with additional binding of name in rlts in rLcons *)
-(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
- [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *}
-print_theorems*)
-
-notation
- alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
- alpha_rlts ("_ \<approx>l _" [100, 100] 100)
-thm alpha_rtrm5_alpha_rlts.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.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> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
- "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
- apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
- apply (simp_all add: alpha5_inj)
- apply (tactic {*
- ALLGOALS (
- TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
- (etac @{thm alpha_gen_compose_eqvt})
- ) *})
- apply (simp_all only: eqvts atom_eqvt)
- done
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
- (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}
-thm alpha5_equivp
-
-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})))
-*}
-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)"
- apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
- apply(simp_all 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.inducts(2))
- apply(simp_all)
- done
-
-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"
- apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
- apply (clarify) apply (rule conjI)
- apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
- 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]
-and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-and bv5[simp] = rbv5.simps[quot_lifted]
-and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
-
-lemma lets_ok:
- "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-done
-
-lemma lets_ok2:
- "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
- (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-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(3) alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))
-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)
-done
-
-
-(* example with a bn function defined over the type itself *)
-datatype rtrm6 =
- rVr6 "name"
-| rLm6 "name" "rtrm6" --"bind name in rtrm6"
-| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
-
-primrec
- rbv6
-where
- "rbv6 (rVr6 n) = {}"
-| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
-| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
-
-setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha "Terms.rtrm6" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
-notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
-(* HERE THE RULES DIFFER *)
-thm alpha_rtrm6.intros
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *}
-thm alpha6_inj
-
-local_setup {*
-snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct})
-*}
-
-local_setup {*
-snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}
-*}
-
-local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []),
- build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt))
-*}
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
- (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *}
-thm alpha6_equivp
-
-quotient_type
- trm6 = rtrm6 / alpha_rtrm6
- by (auto intro: alpha6_equivp)
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))
-*}
-print_theorems
-
-lemma [quot_respect]:
- "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"
-by (auto simp add: alpha6_eqvt)
-
-(* Definitely not true , see lemma below *)
-lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"
-apply simp apply clarify
-apply (erule alpha_rtrm6.induct)
-oops
-
-lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha_rtrm6 ===> op =) rbv6 rbv6"
-apply simp
-apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI)
-apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI)
-apply simp
-apply (simp add: alpha6_inj)
-apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
-apply (simp add: alpha_gen fresh_star_def)
-apply (simp add: alpha6_inj)
-done
-
-lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y"
-apply (induct_tac x y rule: alpha_rtrm6.induct)
-apply simp_all
-apply (erule exE)
-apply (simp_all add: alpha_gen)
-done
-
-lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6"
-by (simp add: fv6_rsp)
-
-lemma [quot_respect]:
- "(op = ===> alpha_rtrm6) rVr6 rVr6"
- "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6"
-apply auto
-apply (simp_all add: alpha6_inj)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm)
-done
-
-lemma [quot_respect]:
- "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"
-apply auto
-apply (simp_all add: alpha6_inj)
-apply (rule_tac [!] x="0::perm" in exI)
-apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm)
-(* needs rbv6_rsp *)
-oops
-
-instantiation trm6 :: pt begin
-
-quotient_definition
- "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
-
-instance
-apply default
-sorry
-end
-
-lemma lifted_induct:
-"\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea);
- \<And>name rtrm6 namea rtrm6a.
- \<lbrakk>True;
- \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and>
- (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>
- \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);
- \<And>rtrm61 rtrm61a rtrm62 rtrm62a.
- \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a;
- \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
- (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>
- \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk>
-\<Longrightarrow> P x1 x2"
-apply (lifting alpha_rtrm6.induct[unfolded alpha_gen])
-apply injection
-(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
-oops
-
-lemma lifted_inject_a3:
-"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) =
-(rtrm61 = rtrm61a \<and>
- (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
- (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))"
-apply(lifting alpha6_inj(3)[unfolded alpha_gen])
-apply injection
-(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
-oops
-
-
-
-
-(* example with a respectful bn function defined over the type itself *)
-
-datatype rtrm7 =
- rVr7 "name"
-| rLm7 "name" "rtrm7" --"bind left in right"
-| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
-
-primrec
- rbv7
-where
- "rbv7 (rVr7 n) = {atom n}"
-| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
-| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
-
-setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
-thm permute_rtrm7.simps
-
-local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
-print_theorems
-notation
- alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
-(* HERE THE RULES DIFFER *)
-thm alpha_rtrm7.intros
-thm fv_rtrm7.simps
-inductive
- alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
-| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
-| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
-
-lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
- apply simp
- apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
- apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
- apply simp
- apply (rule a3)
- apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp_all add: alpha_gen fresh_star_def)
- apply (rule a1)
- apply (rule refl)
-done
-
-
-
-
-
-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 ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha "Terms.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)
-(* HERE THE RULE DIFFERS *)
-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
-
-
-
-
-
-
-datatype rlam9 =
- Var9 "name"
-| Lam9 "name" "rlam9" --"bind name in rlam"
-and rbla9 =
- Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
-
-primrec
- rbv9
-where
- "rbv9 (Var9 x) = {}"
-| "rbv9 (Lam9 x b) = {atom x}"
-
-setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha "Terms.rlam9" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
-notation
- alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
- alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
-(* HERE THE RULES DIFFER *)
-thm alpha_rlam9_alpha_rbla9.intros
-
-
-inductive
- alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
-and
- alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
-| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
-| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
-
-quotient_type
- lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
-sorry
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))
- |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))
- |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))
-*}
-print_theorems
-
-instantiation lam9 and bla9 :: pt
-begin
-
-quotient_definition
- "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
-is
- "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
-
-quotient_definition
- "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
-is
- "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
-
-instance
-sorry
-
-end
-
-lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
- \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
-apply (lifting a3[unfolded alpha_gen])
-apply injection
-sorry
-
-
-
-
-
-
-
-
-text {* type schemes *}
-datatype ty =
- Var "name"
-| Fun "ty" "ty"
-
-setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
-print_theorems
-
-datatype tyS =
- All "name set" "ty"
-
-setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *}
-print_theorems
-
-(*
-Doesnot work yet since we do not refer to fv_ty
-local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
-print_theorems
-*)
-
-primrec
- fv_tyS
-where
- "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
-
-inductive
- alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
-where
- a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2))
- \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
-
-lemma
- shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
- apply(rule a1)
- apply(simp add: alpha_gen)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: fresh_star_def)
- done
-
-lemma
- shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
- apply(rule a1)
- apply(simp add: alpha_gen)
- apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: fresh_star_def)
- done
-
-lemma
- shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
- apply(rule a1)
- apply(simp add: alpha_gen)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: fresh_star_def)
- done
-
-lemma
- assumes a: "a \<noteq> b"
- shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
- using a
- apply(clarify)
- apply(erule alpha_tyS.cases)
- apply(simp add: alpha_gen)
- apply(erule conjE)+
- apply(erule exE)
- apply(erule conjE)+
- apply(clarify)
- apply(simp)
- apply(simp add: fresh_star_def)
- apply(auto)
- done
-
-
-end