equal
deleted
inserted
replaced
6 |
6 |
7 nominal_datatype lam = |
7 nominal_datatype lam = |
8 Var "name" |
8 Var "name" |
9 | App "lam" "lam" |
9 | App "lam" "lam" |
10 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
10 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 |
|
12 lemma Abs1_eq_fdest: |
|
13 fixes x y :: "'a :: at_base" |
|
14 and S T :: "'b :: fs" |
|
15 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
|
16 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T" |
|
17 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T" |
|
18 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S" |
|
19 and "sort_of (atom x) = sort_of (atom y)" |
|
20 shows "f x T = f y S" |
|
21 using assms apply - |
|
22 apply (subst (asm) Abs1_eq_iff') |
|
23 apply simp_all |
|
24 apply (elim conjE disjE) |
|
25 apply simp |
|
26 apply(rule trans) |
|
27 apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
|
28 apply(rule fresh_star_supp_conv) |
|
29 apply(simp add: supp_swap fresh_star_def) |
|
30 apply(simp add: swap_commute) |
|
31 done |
|
32 |
11 |
33 lemma fresh_fun_eqvt_app3: |
12 lemma fresh_fun_eqvt_app3: |
34 assumes a: "eqvt f" |
13 assumes a: "eqvt f" |
35 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
14 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
36 shows "a \<sharp> f x y z" |
15 shows "a \<sharp> f x y z" |
87 apply (simp add: fresh_star_def fresh_def) |
66 apply (simp add: fresh_star_def fresh_def) |
88 apply simp_all |
67 apply simp_all |
89 apply(case_tac x) |
68 apply(case_tac x) |
90 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
69 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
91 apply(auto simp add: fresh_star_def) |
70 apply(auto simp add: fresh_star_def) |
92 apply(erule Abs1_eq_fdest) |
71 apply(erule Abs_lst1_fcb) |
93 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
72 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
94 apply (simp add: fresh_star_def) |
73 apply (simp add: fresh_star_def) |
95 apply (rule fcb3) |
74 apply (rule fcb3) |
96 apply (simp add: fresh_star_def) |
75 apply (simp add: fresh_star_def) |
97 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
76 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |