69 equivariance Beta |
69 equivariance Beta |
70 |
70 |
71 nominal_inductive Beta |
71 nominal_inductive Beta |
72 by (simp_all add: abs_fresh fresh_fact') |
72 by (simp_all add: abs_fresh fresh_fact') |
73 |
73 |
74 lemma supp_beta: |
74 lemma beta_preserves_fresh: |
|
75 fixes a::"name" |
75 assumes a: "t\<longrightarrow>\<^isub>\<beta> s" |
76 assumes a: "t\<longrightarrow>\<^isub>\<beta> s" |
76 shows "(supp s)\<subseteq>((supp t)::name set)" |
77 shows "a\<sharp>t \<Longrightarrow> a\<sharp>s" |
77 using a |
78 using a |
78 by (induct) |
79 apply(nominal_induct t s avoiding: a rule: Beta.strong_induct) |
79 (auto intro!: simp add: abs_supp lam.supp subst_supp) |
80 apply(auto simp add: abs_fresh fresh_fact fresh_atm) |
|
81 done |
80 |
82 |
81 lemma beta_abs: |
83 lemma beta_abs: |
82 assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'" |
84 assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'" |
83 shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''" |
85 shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''" |
84 using a |
86 proof - |
85 apply - |
87 have "a\<sharp>Lam [a].t" by (simp add: abs_fresh) |
86 apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'") |
88 with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh) |
87 apply(auto simp add: lam.distinct lam.inject) |
89 with a show ?thesis |
88 apply(auto simp add: alpha) |
90 by (cases rule: Beta.strong_cases[where a="a" and aa="a"]) |
89 apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI) |
91 (auto simp add: lam.inject abs_fresh alpha) |
90 apply(rule conjI) |
92 qed |
91 apply(rule sym) |
|
92 apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst]) |
|
93 apply(simp) |
|
94 apply(rule pt_name3) |
|
95 apply(simp add: at_ds5[OF at_name_inst]) |
|
96 apply(rule conjI) |
|
97 apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm) |
|
98 apply(force dest!: supp_beta simp add: fresh_def) |
|
99 apply(force intro!: eqvts) |
|
100 done |
|
101 |
93 |
102 lemma beta_subst: |
94 lemma beta_subst: |
103 assumes a: "M \<longrightarrow>\<^isub>\<beta> M'" |
95 assumes a: "M \<longrightarrow>\<^isub>\<beta> M'" |
104 shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" |
96 shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" |
105 using a |
97 using a |