4 |
4 |
5 text {* example 1, equivalent to example 2 from Terms *} |
5 text {* example 1, equivalent to example 2 from Terms *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
|
9 (* maybe should be added to Infinite.thy *) |
|
10 lemma infinite_Un: |
|
11 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
12 by simp |
|
13 |
9 ML {* val _ = cheat_alpha_eqvt := false *} |
14 ML {* val _ = cheat_alpha_eqvt := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
15 ML {* val _ = cheat_fv_eqvt := false *} |
11 ML {* val _ = recursive := false *} |
16 ML {* val _ = recursive := false *} |
|
17 |
|
18 nominal_datatype lm = |
|
19 Vr "name" |
|
20 | Ap "lm" "lm" |
|
21 | Lm x::"name" l::"lm" bind x in l |
|
22 |
|
23 lemma finite_fv: |
|
24 shows "finite (fv_lm t)" |
|
25 apply(induct t rule: lm_induct) |
|
26 apply(simp_all add: lm_fv) |
|
27 done |
|
28 |
|
29 lemma supp_fn: |
|
30 shows "supp t = fv_lm t" |
|
31 apply(induct t rule: lm_induct) |
|
32 apply(simp_all add: lm_fv) |
|
33 apply(simp only: supp_def) |
|
34 apply(simp only: lm_perm) |
|
35 apply(simp only: lm_inject) |
|
36 apply(simp only: supp_def[symmetric]) |
|
37 apply(simp only: supp_at_base) |
|
38 apply(simp (no_asm) only: supp_def) |
|
39 apply(simp only: lm_perm) |
|
40 apply(simp only: lm_inject) |
|
41 apply(simp only: de_Morgan_conj) |
|
42 apply(simp only: Collect_disj_eq) |
|
43 apply(simp only: infinite_Un) |
|
44 apply(simp only: Collect_disj_eq) |
|
45 apply(simp only: supp_def[symmetric]) |
|
46 apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst) |
|
47 apply(simp (no_asm) only: supp_def) |
|
48 apply(simp only: lm_perm) |
|
49 apply(simp only: permute_ABS) |
|
50 apply(simp only: lm_inject) |
|
51 apply(simp only: Abs_eq_iff) |
|
52 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
53 apply(simp only: alpha_gen) |
|
54 apply(simp only: supp_eqvt[symmetric]) |
|
55 apply(simp only: eqvts) |
|
56 apply(simp only: supp_Abs) |
|
57 done |
|
58 |
|
59 lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]] |
|
60 |
|
61 lemma obtain_atom_ex: |
|
62 assumes fin: "finite (supp x)" |
|
63 shows "\<exists>a. a \<sharp> x \<and> sort_of a = s" |
|
64 using obtain_atom[OF fin] |
|
65 unfolding fresh_def |
|
66 by blast |
|
67 |
|
68 lemma |
|
69 assumes a0: "finite (supp c)" |
|
70 and a1: "\<And>name c. P c (Vr name)" |
|
71 and a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)" |
|
72 and a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)" |
|
73 shows "P c lm" |
|
74 proof - |
|
75 have "\<And>p c. P c (p \<bullet> lm)" |
|
76 apply(induct lm rule: lm_induct) |
|
77 apply(simp only: lm_perm) |
|
78 apply(rule a1) |
|
79 apply(simp only: lm_perm) |
|
80 apply(rule a2) |
|
81 apply(assumption) |
|
82 apply(assumption) |
|
83 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw)) |
|
84 \<and> sort_of (atom new) = sort_of (atom name)") |
|
85 apply(erule exE) |
|
86 apply(rule_tac t="(p \<bullet> Lm name lm_raw)" and |
|
87 s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm_raw)" in subst) |
|
88 apply(simp) |
|
89 apply(subst lm_perm) |
|
90 apply(subst (2) lm_perm) |
|
91 apply(rule swap_fresh_fresh) |
|
92 apply(simp add: fresh_def) |
|
93 apply(simp only: supp_fn') |
|
94 apply(simp) |
|
95 apply(simp add: fresh_Pair) |
|
96 apply(simp add: lm_perm) |
|
97 apply(rule a3) |
|
98 apply(drule_tac x="(atom (p \<bullet> name) \<rightleftharpoons> atom new) + p" in meta_spec) |
|
99 apply(simp) |
|
100 sorry (* use at_set_avoiding *) |
|
101 then have "P c (0 \<bullet> lm)" by blast |
|
102 then show "P c lm" by simp |
|
103 qed |
|
104 |
12 |
105 |
13 nominal_datatype lam = |
106 nominal_datatype lam = |
14 VAR "name" |
107 VAR "name" |
15 | APP "lam" "lam" |
108 | APP "lam" "lam" |
16 | LAM x::"name" t::"lam" bind x in t |
109 | LAM x::"name" t::"lam" bind x in t |
104 apply(simp only: supp_at_base) |
192 apply(simp only: supp_at_base) |
105 apply(simp) |
193 apply(simp) |
106 done |
194 done |
107 |
195 |
108 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
196 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
109 |
|
110 lemma supports_lam_bp: |
|
111 "(supp (atom a)) supports (VAR a)" |
|
112 "(supp t \<union> supp s) supports (APP t s)" |
|
113 "(supp (atom a) \<union> supp t) supports (LAM a t)" |
|
114 "(supp b \<union> supp t) supports (LET b t)" |
|
115 "(supp (atom a) \<union> supp t) supports (BP a t)" |
|
116 apply - |
|
117 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
118 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
119 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
120 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
121 apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *}) |
|
122 done |
|
123 |
|
124 lemma finite_supp_lam_bp: |
|
125 fixes lam::"lam" |
|
126 and bp::"bp" |
|
127 shows "finite (supp lam)" |
|
128 and "finite (supp bp)" |
|
129 apply(induct lam and bp rule: lam_bp_inducts) |
|
130 apply(rule supports_finite) |
|
131 apply(rule supports_lam_bp) |
|
132 apply(simp add: supp_atom) |
|
133 apply(rule supports_finite) |
|
134 apply(rule supports_lam_bp) |
|
135 apply(simp) |
|
136 apply(rule supports_finite) |
|
137 apply(rule supports_lam_bp) |
|
138 apply(simp add: supp_atom) |
|
139 apply(rule supports_finite) |
|
140 apply(rule supports_lam_bp) |
|
141 apply(simp) |
|
142 apply(rule supports_finite) |
|
143 apply(rule supports_lam_bp) |
|
144 apply(simp add: supp_atom) |
|
145 done |
|
146 |
|
147 |
197 |
148 ML {* val _ = cheat_alpha_eqvt := true *} |
198 ML {* val _ = cheat_alpha_eqvt := true *} |
149 ML {* val _ = recursive := true *} |
199 ML {* val _ = recursive := true *} |
150 |
200 |
151 nominal_datatype lam' = |
201 nominal_datatype lam' = |