equal
deleted
inserted
replaced
8 atom_decl var |
8 atom_decl var |
9 |
9 |
10 nominal_datatype lam = |
10 nominal_datatype lam = |
11 V "var" |
11 V "var" |
12 | Ap "lam" "lam" (infixl "\<cdot>" 98) |
12 | Ap "lam" "lam" (infixl "\<cdot>" 98) |
13 | Lm x::"var" l::"lam" bind x in l ("\<integral> _. _" [97, 97] 99) |
13 | Lm x::"var" l::"lam" binds x in l ("\<integral> _. _" [97, 97] 99) |
14 |
14 |
15 nominal_primrec |
15 nominal_primrec |
16 subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
16 subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
17 where |
17 where |
18 "(V x)[y ::= s] = (if x = y then s else (V x))" |
18 "(V x)[y ::= s] = (if x = y then s else (V x))" |
46 next |
46 next |
47 show "eqvt subst_graph" unfolding eqvt_def subst_graph_def |
47 show "eqvt subst_graph" unfolding eqvt_def subst_graph_def |
48 by (rule, perm_simp, rule) |
48 by (rule, perm_simp, rule) |
49 qed |
49 qed |
50 |
50 |
51 termination |
51 termination (eqvt) by lexicographic_order |
52 by (relation "measure (\<lambda>(t,_,_). size t)") |
|
53 (simp_all add: lam.size) |
|
54 |
|
55 lemma subst_eqvt[eqvt]: |
|
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) |
|
58 |
52 |
59 lemma forget[simp]: |
53 lemma forget[simp]: |
60 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
54 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
61 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
55 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
62 (auto simp add: lam.fresh fresh_at_base) |
56 (auto simp add: lam.fresh fresh_at_base) |