101 | "\<exists>pi. (bi bp, lam) \<approx>gen Alpha_lam fv_lam_raw pi (bi bp', lam') \<and> Compat_bp bp pi bp' |
101 | "\<exists>pi. (bi bp, lam) \<approx>gen Alpha_lam fv_lam_raw pi (bi bp', lam') \<and> Compat_bp bp pi bp' |
102 \<and> (pi \<bullet> (bi bp)) = bi bp' |
102 \<and> (pi \<bullet> (bi bp)) = bi bp' |
103 \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')" |
103 \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')" |
104 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')" |
104 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')" |
105 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')" |
105 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')" |
106 |
106 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding Alpha_inj}, []), (build_alpha_inj @{thms Alpha_lam_Alpha_bp_Compat_bp.intros} @{thms lam_raw.distinct lam_raw.inject bp_raw.distinct bp_raw.inject} @{thms Alpha_lam.cases Alpha_bp.cases Compat_bp.cases} ctxt)) ctxt)) *} |
107 |
107 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_inj}, []), (build_alpha_inj @{thms alpha_lam_raw_alpha_bp_raw.intros} @{thms lam_raw.distinct lam_raw.inject bp_raw.distinct bp_raw.inject} @{thms alpha_lam_raw.cases alpha_bp_raw.cases} ctxt)) ctxt)) *} |
|
108 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel ctxt @{thms alpha_lam_raw.cases}) ([(@{thms lam_raw.distinct},@{term alpha_lam_raw})])))) ctxt)) *} |
|
109 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding Alpha_dis}, []), (flat (map (distinct_rel ctxt @{thms Alpha_lam.cases}) ([(@{thms lam_raw.distinct},@{term Alpha_lam})])))) ctxt)) *} |
|
110 lemma "Alpha_lam x y = alpha_lam_raw x y" |
|
111 apply rule |
|
112 apply(induct x y rule: Alpha_lam_Alpha_bp_Compat_bp.inducts(1)) |
|
113 apply(simp_all only: alpha_lam_raw_alpha_bp_raw.intros) |
|
114 apply(simp_all add: alpha_inj) |
|
115 apply(erule exE) apply(rule_tac x="pi" in exI) |
|
116 apply(simp add: alpha_gen) |
|
117 apply clarify |
|
118 apply simp |
|
119 defer |
|
120 apply(induct x y rule: alpha_lam_raw_alpha_bp_raw.inducts(1)) |
|
121 apply(simp_all only: Alpha_lam_Alpha_bp_Compat_bp.intros) |
|
122 apply(simp_all add: Alpha_inj) |
|
123 apply(erule exE) apply(rule_tac x="pi" in exI) |
|
124 apply(simp add: alpha_gen) |
|
125 apply clarify |
|
126 apply simp |
|
127 oops |
108 |
128 |
109 lemma Test1: |
129 lemma Test1: |
110 assumes "distinct [x, y]" |
130 assumes "distinct [x, y]" |
111 shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
131 shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
112 (LET (BP y (VAR y)) (VAR y))" |
132 (LET (BP y (VAR y)) (VAR y))" |