28 thm trm_lts.induct[no_vars] |
28 thm trm_lts.induct[no_vars] |
29 thm trm_lts.inducts[no_vars] |
29 thm trm_lts.inducts[no_vars] |
30 thm trm_lts.distinct |
30 thm trm_lts.distinct |
31 thm trm_lts.fv[simplified trm_lts.supp] |
31 thm trm_lts.fv[simplified trm_lts.supp] |
32 |
32 |
|
33 consts |
|
34 permute_bn :: "perm \<Rightarrow> lts \<Rightarrow> lts" |
|
35 |
|
36 lemma test: |
|
37 "permute_bn pi (Lnil) = Lnil" |
|
38 "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)" |
|
39 sorry |
|
40 |
33 lemma |
41 lemma |
34 fixes t::trm |
42 fixes t::trm |
35 and l::lts |
43 and l::lts |
36 and c::"'a::fs" |
44 and c::"'a::fs" |
37 assumes a1: "\<And>name c. P1 c (Vr name)" |
45 assumes a1: "\<And>name c. P1 c (Vr name)" |
38 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
46 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
39 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
47 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
40 and a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
48 and a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* (c, Lt lts trm); \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
41 and a5: "\<And>c. P2 c Lnil" |
49 and a5: "\<And>c. P2 c Lnil" |
42 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
50 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
43 shows "P1 c t" and "P2 c l" |
51 shows "P1 c t" and "P2 c l" |
44 proof - |
52 proof - |
45 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
53 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
67 apply(simp add: finite_supp) |
75 apply(simp add: finite_supp) |
68 apply(simp add: finite_supp) |
76 apply(simp add: finite_supp) |
69 apply(simp add: fresh_def) |
77 apply(simp add: fresh_def) |
70 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
78 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
71 apply(simp) |
79 apply(simp) |
72 apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Lt (p \<bullet> lts) (p \<bullet> trm)) \<sharp>* q") |
80 apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
73 apply(erule exE) |
81 apply(erule exE) |
|
82 (* HERE *) |
74 apply(rule_tac t="Lt (p \<bullet> lts) (p \<bullet> trm)" |
83 apply(rule_tac t="Lt (p \<bullet> lts) (p \<bullet> trm)" |
75 and s="q \<bullet> Lt (p \<bullet> lts) (p \<bullet> trm)" in subst) |
84 and s="Lt (permute_bn q (p \<bullet> lts)) (q \<bullet> p \<bullet> trm)" in subst) |
76 apply(rule supp_perm_eq) |
85 defer |
77 apply(simp) |
|
78 apply(simp) |
|
79 apply(rule a4) |
86 apply(rule a4) |
|
87 defer |
80 apply(simp add: eqvts) |
88 apply(simp add: eqvts) |
|
89 apply(simp add: fresh_star_prod) |
|
90 apply(simp add: fresh_star_def) |
|
91 apply(simp add: fresh_def) |
|
92 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
81 apply(subst permute_plus[symmetric]) |
93 apply(subst permute_plus[symmetric]) |
82 apply(blast) |
94 apply(blast) |
83 apply(subst permute_plus[symmetric]) |
95 apply(subst permute_plus[symmetric]) |
84 apply(blast) |
96 apply(blast) |
85 apply(rule at_set_avoiding2) |
97 apply(rule at_set_avoiding2) |
87 defer |
99 defer |
88 apply(simp add: finite_supp) |
100 apply(simp add: finite_supp) |
89 apply(simp add: finite_supp) |
101 apply(simp add: finite_supp) |
90 apply(simp add: fresh_star_def) |
102 apply(simp add: fresh_star_def) |
91 apply(simp add: fresh_def) |
103 apply(simp add: fresh_def) |
|
104 thm trm_lts.fv[simplified trm_lts.supp] |
92 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
105 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
106 apply(simp add: alpha_bn_eq_iff) |
93 defer |
107 defer |
94 apply(simp) |
108 apply(simp) |
95 apply(rule a5) |
109 apply(rule a5) |
96 apply(simp) |
110 apply(simp) |
97 apply(rule a6) |
111 apply(rule a6) |