1 theory Let |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 |
|
6 atom_decl name |
|
7 |
|
8 nominal_datatype trm = |
|
9 Var "name" |
|
10 | App "trm" "trm" |
|
11 | Lam x::"name" t::"trm" binds x in t |
|
12 | Let as::"assn" t::"trm" binds "bn as" in t |
|
13 and assn = |
|
14 ANil |
|
15 | ACons "name" "trm" "assn" |
|
16 binder |
|
17 bn |
|
18 where |
|
19 "bn ANil = []" |
|
20 | "bn (ACons x t as) = (atom x) # (bn as)" |
|
21 |
|
22 lemma alpha_bn_inducts_raw: |
|
23 "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw; |
|
24 \<And>trm_raw trm_rawa assn_raw assn_rawa name namea. |
|
25 \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa; |
|
26 P3 assn_raw assn_rawa\<rbrakk> |
|
27 \<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw) |
|
28 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
|
29 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
|
30 |
|
31 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
|
32 |
|
33 lemma alpha_bn_refl: "alpha_bn x x" |
|
34 by (induct x rule: trm_assn.inducts(2)) |
|
35 (rule TrueI, auto simp add: trm_assn.eq_iff) |
|
36 |
|
37 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
|
38 by (simp add: permute_pure) |
|
39 |
|
40 lemma what_we_would_like: |
|
41 assumes a: "alpha_bn as asa" |
|
42 shows "\<forall>p. set (bn as) \<sharp>* fv_bn as \<and> set (bn asa) \<sharp>* fv_bn asa \<and> |
|
43 p \<bullet> bn as = bn asa \<and> supp p \<subseteq> set (bn as) \<union> set (bn asa) \<longrightarrow> p \<bullet> as = asa" |
|
44 apply (rule alpha_bn_inducts[OF a]) |
|
45 apply |
|
46 (simp_all add: trm_assn.bn_defs trm_assn.perm_bn_simps trm_assn.supp) |
|
47 apply clarify |
|
48 apply simp |
|
49 apply (simp add: atom_eqvt) |
|
50 apply (case_tac "name = namea") |
|
51 sorry |
|
52 |
|
53 lemma Abs_lst_fcb2: |
|
54 fixes as bs :: "'a :: fs" |
|
55 and x y :: "'b :: fs" |
|
56 and c::"'c::fs" |
|
57 assumes eq: "[ba as]lst. x = [ba bs]lst. y" |
|
58 and fcb1: "set (ba as) \<sharp>* f as x c" |
|
59 and fresh1: "set (ba as) \<sharp>* c" |
|
60 and fresh2: "set (ba bs) \<sharp>* c" |
|
61 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
62 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
63 and ba_inj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs" |
|
64 shows "f as x c = f bs y c" |
|
65 sorry |
|
66 |
|
67 nominal_primrec |
|
68 height_trm :: "trm \<Rightarrow> nat" |
|
69 and height_assn :: "assn \<Rightarrow> nat" |
|
70 where |
|
71 "height_trm (Var x) = 1" |
|
72 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
|
73 | "height_trm (Lam v b) = 1 + (height_trm b)" |
|
74 | "set (bn as) \<sharp>* fv_bn as \<Longrightarrow> height_trm (Let as b) = max (height_assn as) (height_trm b)" |
|
75 | "height_assn ANil = 0" |
|
76 | "height_assn (ACons v t as) = max (height_trm t) (height_assn as)" |
|
77 apply (simp only: eqvt_def height_trm_height_assn_graph_def) |
|
78 apply (rule, perm_simp, rule, rule TrueI) |
|
79 apply (case_tac x) |
|
80 apply (rule_tac y="a" in trm_assn.strong_exhaust(1)) |
|
81 apply (auto)[4] |
|
82 apply (drule_tac x="assn" in meta_spec) |
|
83 apply (drule_tac x="trm" in meta_spec) |
|
84 apply (simp add: alpha_bn_refl) |
|
85 --"HERE" |
|
86 defer |
|
87 apply (case_tac b rule: trm_assn.exhaust(2)) |
|
88 apply (auto)[2] |
|
89 apply(simp_all) |
|
90 apply (erule_tac c="()" in Abs_lst_fcb2) |
|
91 apply (simp_all add: pure_fresh fresh_star_def)[3] |
|
92 apply (simp add: eqvt_at_def) |
|
93 apply (simp add: eqvt_at_def) |
|
94 apply assumption |
|
95 apply(erule conjE) |
|
96 apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff]) |
|
97 apply (simp add: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff]) |
|
98 apply (subgoal_tac "eqvt_at height_assn as") |
|
99 apply (subgoal_tac "eqvt_at height_assn asa") |
|
100 apply (subgoal_tac "eqvt_at height_trm b") |
|
101 apply (subgoal_tac "eqvt_at height_trm ba") |
|
102 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr as)") |
|
103 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr asa)") |
|
104 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl b)") |
|
105 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl ba)") |
|
106 defer |
|
107 apply (simp add: eqvt_at_def height_trm_def) |
|
108 apply (simp add: eqvt_at_def height_trm_def) |
|
109 apply (simp add: eqvt_at_def height_assn_def) |
|
110 apply (simp add: eqvt_at_def height_assn_def) |
|
111 defer |
|
112 apply (subgoal_tac "height_assn as = height_assn asa") |
|
113 apply (subgoal_tac "height_trm b = height_trm ba") |
|
114 apply simp |
|
115 apply (erule_tac c="()" in Abs_lst_fcb2) |
|
116 apply (simp_all add: pure_fresh fresh_star_def)[3] |
|
117 apply (simp_all add: eqvt_at_def)[2] |
|
118 apply assumption |
|
119 apply (erule_tac Abs_lst_fcb) |
|
120 apply (simp_all add: pure_fresh fresh_star_def)[2] |
|
121 apply (drule what_we_would_like) |
|
122 apply (drule_tac x="p" in spec) |
|
123 apply simp |
|
124 apply (simp add: eqvt_at_def) |
|
125 oops |
|
126 |
|
127 end |
|
128 |
|
129 |
|
130 |
|