23 |
23 |
24 thm trm_lts.fv |
24 thm trm_lts.fv |
25 thm trm_lts.eq_iff |
25 thm trm_lts.eq_iff |
26 thm trm_lts.bn |
26 thm trm_lts.bn |
27 thm trm_lts.perm |
27 thm trm_lts.perm |
28 thm trm_lts.induct |
28 thm trm_lts.induct[no_vars] |
|
29 thm trm_lts.inducts[no_vars] |
29 thm trm_lts.distinct |
30 thm trm_lts.distinct |
30 thm trm_lts.fv[simplified trm_lts.supp] |
31 thm trm_lts.fv[simplified trm_lts.supp] |
|
32 |
|
33 lemma |
|
34 fixes t::trm |
|
35 and l::lts |
|
36 and c::"'a::fs" |
|
37 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)" |
|
39 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)" |
|
41 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)" |
|
43 shows "P1 c t" and "P2 c l" |
|
44 proof - |
|
45 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
|
46 "(\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> l))" |
|
47 apply(induct rule: trm_lts.inducts) |
|
48 apply(simp) |
|
49 apply(rule a1) |
|
50 apply(simp) |
|
51 apply(rule a2) |
|
52 apply(simp) |
|
53 apply(simp) |
|
54 apply(simp) |
|
55 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
56 apply(erule exE) |
|
57 apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" |
|
58 and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst) |
|
59 apply(rule supp_perm_eq) |
|
60 apply(simp) |
|
61 apply(simp) |
|
62 apply(rule a3) |
|
63 apply(simp add: atom_eqvt) |
|
64 apply(subst permute_plus[symmetric]) |
|
65 apply(blast) |
|
66 apply(rule at_set_avoiding2_atom) |
|
67 apply(simp add: finite_supp) |
|
68 apply(simp add: finite_supp) |
|
69 apply(simp add: fresh_def) |
|
70 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
71 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") |
|
73 apply(erule exE) |
|
74 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) |
|
76 apply(rule supp_perm_eq) |
|
77 apply(simp) |
|
78 apply(simp) |
|
79 apply(rule a4) |
|
80 apply(simp add: eqvts) |
|
81 apply(subst permute_plus[symmetric]) |
|
82 apply(blast) |
|
83 apply(subst permute_plus[symmetric]) |
|
84 apply(blast) |
|
85 apply(rule at_set_avoiding2) |
|
86 apply(simp add: finite_supp) |
|
87 defer |
|
88 apply(simp add: finite_supp) |
|
89 apply(simp add: finite_supp) |
|
90 apply(simp add: fresh_star_def) |
|
91 apply(simp add: fresh_def) |
|
92 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
93 defer |
|
94 apply(simp) |
|
95 apply(rule a5) |
|
96 apply(simp) |
|
97 apply(rule a6) |
|
98 apply(simp) |
|
99 apply(simp) |
|
100 oops |
|
101 |
|
102 |
31 |
103 |
32 lemma lets_bla: |
104 lemma lets_bla: |
33 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
105 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
34 by (simp add: trm_lts.eq_iff) |
106 by (simp add: trm_lts.eq_iff) |
35 |
107 |