50 |
50 |
51 termination |
51 termination |
52 by (relation "measure (\<lambda>(t,_,_). size t)") |
52 by (relation "measure (\<lambda>(t,_,_). size t)") |
53 (simp_all add: lam.size) |
53 (simp_all add: lam.size) |
54 |
54 |
55 lemma subst4[eqvt]: |
55 lemma subst_eqvt[eqvt]: |
56 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
56 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
57 by (induct t x s rule: subst.induct) (simp_all) |
57 by (induct t x s rule: subst.induct) (simp_all) |
58 |
58 |
59 lemma subst1[simp]: |
59 lemma forget[simp]: |
60 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
60 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
61 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
61 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
62 (auto simp add: lam.fresh fresh_at_base) |
62 (auto simp add: lam.fresh fresh_at_base) |
63 |
63 |
64 lemma subst2[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t" |
64 lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t" |
65 by (simp add: fresh_def) |
65 by (simp add: fresh_def) |
66 |
66 |
67 lemma subst3[simp]: "M [x ::= V x] = M" |
67 lemma subst_id[simp]: "M [x ::= V x] = M" |
68 by (rule_tac lam="M" and c="x" in lam.strong_induct) |
68 by (rule_tac lam="M" and c="x" in lam.strong_induct) |
69 (simp_all add: fresh_star_def lam.fresh fresh_Pair) |
69 (simp_all add: fresh_star_def lam.fresh fresh_Pair) |
70 |
70 |
71 inductive |
71 inductive |
72 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80) |
72 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80) |