equal
deleted
inserted
replaced
8 |
8 |
9 nominal_datatype trm = |
9 nominal_datatype trm = |
10 Var "name" |
10 Var "name" |
11 | App "trm" "trm" |
11 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |
13 | Let p::"pat" "trm" t::"trm" bind_set "f p" in t |
13 | Let p::"pat" "trm" t::"trm" bind "f p" in t |
14 and pat = |
14 and pat = |
15 PN |
15 PN |
16 | PS "name" |
16 | PS "name" |
17 | PD "name" "name" |
17 | PD "name" "name" |
18 binder |
18 binder |
19 f::"pat \<Rightarrow> atom set" |
19 f::"pat \<Rightarrow> atom list" |
20 where |
20 where |
21 "f PN = {}" |
21 "f PN = []" |
22 | "f (PD x y) = {atom x, atom y}" |
22 | "f (PS x) = [atom x]" |
23 | "f (PS x) = {atom x}" |
23 | "f (PD x y) = [atom x, atom y]" |
|
24 |
24 thm trm_pat.bn |
25 thm trm_pat.bn |
25 thm trm_pat.perm |
26 thm trm_pat.perm |
26 thm trm_pat.induct |
27 thm trm_pat.induct |
27 thm trm_pat.distinct |
28 thm trm_pat.distinct |
28 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
29 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
29 |
30 |
|
31 lemma lets_overlap1: |
|
32 "atom a \<noteq> atom b \<Longrightarrow> Let (PD a a) x y \<noteq> Let (PD a b) x y" |
|
33 by (simp add: trm_pat.eq_iff alphas) |
|
34 |
|
35 lemma lets_overlap2: |
|
36 "atom a \<notin> supp y \<Longrightarrow> atom b \<notin> supp y \<Longrightarrow> Let (PD a a) x y = Let (PD b b) x y" |
|
37 apply (simp add: trm_pat.eq_iff alphas trm_pat.supp) |
|
38 apply (rule_tac x="(a\<leftrightarrow>b)" in exI) |
|
39 apply (simp add: eqvts) |
|
40 apply (rule conjI) |
|
41 prefer 2 |
|
42 apply (rule Nominal2_Supp.supp_perm_eq) |
|
43 apply (unfold fresh_star_def) |
|
44 apply (unfold fresh_def) |
|
45 apply (unfold flip_def) |
|
46 apply (simp_all add: supp_swap) |
|
47 apply auto |
|
48 done |
30 |
49 |
31 end |
50 end |
32 |
51 |
33 |
52 |
34 |
53 |