equal
deleted
inserted
replaced
1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal/Nominal2" |
2 imports "../Nominal/Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 section {* Definitions for Lambda Terms *} |
5 section {* Definitions for Lambda Terms *} |
|
6 |
6 |
7 |
7 text {* type of variables *} |
8 text {* type of variables *} |
8 |
9 |
9 atom_decl name |
10 atom_decl name |
10 |
11 |
48 |
49 |
49 termination |
50 termination |
50 by (relation "measure size") (simp_all add: lam.size) |
51 by (relation "measure size") (simp_all add: lam.size) |
51 |
52 |
52 |
53 |
53 subsection {* Capture-avoiding Substitution *} |
54 subsection {* Capture-Avoiding Substitution *} |
54 |
55 |
55 nominal_primrec |
56 nominal_primrec |
56 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
57 where |
58 where |
58 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
95 apply(drule sym) |
96 apply(drule sym) |
96 apply(simp add: Abs_fresh_iff) |
97 apply(simp add: Abs_fresh_iff) |
97 done |
98 done |
98 |
99 |
99 termination |
100 termination |
100 by (relation "measure (\<lambda>(t,_,_). size t)") |
101 by (relation "measure (\<lambda>(t, _, _). size t)") |
101 (simp_all add: lam.size) |
102 (simp_all add: lam.size) |
102 |
103 |
103 lemma subst_eqvt[eqvt]: |
104 lemma subst_eqvt[eqvt]: |
104 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)]" |
105 by (induct t x s rule: subst.induct) (simp_all) |
106 by (induct t x s rule: subst.induct) (simp_all) |