equal
deleted
inserted
replaced
103 |
103 |
104 lemma subst_eqvt[eqvt]: |
104 lemma subst_eqvt[eqvt]: |
105 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
105 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
106 by (induct t x s rule: subst.induct) (simp_all) |
106 by (induct t x s rule: subst.induct) (simp_all) |
107 |
107 |
108 |
108 lemma fresh_fact: |
109 subsection {* Single-Step Beta-Reduction *} |
109 assumes a: "atom z \<sharp> s" |
110 |
110 and b: "z = y \<or> atom z \<sharp> t" |
111 inductive |
111 shows "atom z \<sharp> t[y ::= s]" |
112 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
112 using a b |
113 where |
113 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
114 b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s" |
114 (auto simp add: lam.fresh fresh_at_base) |
115 | b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2" |
|
116 | b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2" |
|
117 | b4[intro]: "App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]" |
|
118 |
|
119 |
|
120 |
115 |
121 |
116 |
122 end |
117 end |
123 |
118 |
124 |
119 |