3 theory LambdaTerms imports "../../Nominal2" begin |
3 theory LambdaTerms imports "../../Nominal2" begin |
4 |
4 |
5 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x" |
5 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x" |
6 unfolding fresh_def by blast |
6 unfolding fresh_def by blast |
7 |
7 |
8 atom_decl var |
8 atom_decl name |
9 |
9 |
10 nominal_datatype lam = |
10 nominal_datatype lam = |
11 Var "var" |
11 Var "name" |
12 | App "lam" "lam" |
12 | App "lam" "lam" |
13 | Lam x::"var" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
13 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
14 |
14 |
15 notation |
15 notation |
16 App (infixl "\<cdot>" 98) and |
16 App (infixl "\<cdot>" 98) and |
17 Lam ("\<integral> _. _" [97, 97] 99) |
17 Lam ("\<integral> _. _" [97, 97] 99) |
18 |
18 |
19 nominal_primrec |
19 nominal_primrec |
20 subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
20 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
21 where |
21 where |
22 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
22 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
23 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])" |
23 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])" |
24 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])" |
24 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])" |
25 proof auto |
25 proof auto |
26 fix a b :: lam and aa :: var and P |
26 fix a b :: lam and aa :: name and P |
27 assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P" |
27 assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P" |
28 "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P" |
28 "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P" |
29 "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P" |
29 "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P" |
30 then show "P" |
30 then show "P" |
31 by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
31 by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
32 (blast, blast, simp add: fresh_star_def) |
32 (blast, blast, simp add: fresh_star_def) |
33 next |
33 next |
34 fix x :: var and t and xa :: var and ya sa ta |
34 fix x :: name and t and xa :: name and ya sa ta |
35 assume *: "eqvt_at subst_sumC (t, ya, sa)" |
35 assume *: "eqvt_at subst_sumC (t, ya, sa)" |
36 "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)" |
36 "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)" |
37 "[[atom x]]lst. t = [[atom xa]]lst. ta" |
37 "[[atom x]]lst. t = [[atom xa]]lst. ta" |
38 then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)" |
38 then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)" |
39 apply - |
39 apply - |