19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 |
24 (* can lift *) |
25 |
|
26 thm alpha_sym_thms |
|
27 thm alpha_trans_thms |
|
28 thm size_eqvt |
|
29 thm size_simps |
|
30 thm size_rsp |
|
31 thm alpha_bn_imps |
|
32 thm distinct |
25 thm distinct |
|
26 thm trm_raw_assg_raw.inducts |
|
27 thm fv_defs |
|
28 |
|
29 |
|
30 (* cannot lift yet *) |
33 thm eq_iff |
31 thm eq_iff |
34 thm eq_iff_simps |
32 thm eq_iff_simps |
35 thm fv_defs |
|
36 thm perm_simps |
33 thm perm_simps |
37 thm perm_laws |
34 thm perm_laws |
|
35 thm trm_raw_assg_raw.size(9 - 16) |
|
36 |
|
37 (* rsp lemmas *) |
|
38 thm size_rsp |
38 thm funs_rsp |
39 thm funs_rsp |
39 thm constrs_rsp |
40 thm constrs_rsp |
|
41 thm permute_rsp |
40 |
42 |
41 declare constrs_rsp[quot_respect] |
43 declare constrs_rsp[quot_respect] |
42 (* declare funs_rsp[quot_respect] *) |
44 declare funs_rsp[quot_respect] |
43 |
45 declare size_rsp[quot_respect] |
44 typ trm |
46 declare permute_rsp[quot_respect] |
45 typ assg |
|
46 term Var |
|
47 term App |
|
48 term Baz |
|
49 term bn |
|
50 term fv_trm |
|
51 term alpha_bn |
|
52 |
|
53 lemma [quot_respect]: |
|
54 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
|
55 apply(simp) |
|
56 sorry |
|
57 |
47 |
58 ML {* |
48 ML {* |
59 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
49 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
60 *} |
50 *} |
61 |
51 |
65 |
55 |
66 ML {* |
56 ML {* |
67 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
57 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
68 *} |
58 *} |
69 |
59 |
70 thm perm_defs[no_vars] |
60 instantiation trm and assg :: size |
|
61 begin |
|
62 |
|
63 quotient_definition |
|
64 "size_trm :: trm \<Rightarrow> nat" |
|
65 is "size :: trm_raw \<Rightarrow> nat" |
|
66 |
|
67 quotient_definition |
|
68 "size_assg :: assg \<Rightarrow> nat" |
|
69 is "size :: assg_raw \<Rightarrow> nat" |
|
70 |
|
71 instance .. |
|
72 |
|
73 end |
|
74 |
|
75 ML {* |
|
76 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} |
|
77 *} |
|
78 |
|
79 |
|
80 |
|
81 instantiation trm and assg :: pt |
|
82 begin |
|
83 |
|
84 quotient_definition |
|
85 "permute_trm :: perm => trm => trm" |
|
86 is "permute :: perm \<Rightarrow> trm_raw \<Rightarrow> trm_raw" |
|
87 |
|
88 quotient_definition |
|
89 "permute_assg :: perm => assg => assg" |
|
90 is "permute :: perm \<Rightarrow> assg_raw \<Rightarrow> assg_raw" |
|
91 |
|
92 lemma qperm_laws: |
|
93 fixes t::trm and a::assg |
|
94 shows "permute 0 t = t" |
|
95 and "permute 0 a = a" |
|
96 sorry |
|
97 |
|
98 instance |
|
99 apply(default) |
|
100 sorry |
|
101 |
|
102 end |
|
103 |
|
104 |
|
105 (* |
|
106 lemma [quot_respect]: |
|
107 "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" |
|
108 apply(simp) |
|
109 sorry |
|
110 *) |
|
111 |
|
112 ML {* |
|
113 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]} |
|
114 *} |
|
115 |
|
116 ML {* |
|
117 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
|
118 *} |
|
119 |
|
120 |
|
121 (* |
|
122 instance trm :: size .. |
|
123 instance assg :: size .. |
|
124 |
|
125 lemma "(size (Var x)) = 0" |
|
126 apply(descending) |
|
127 apply(rule trm_raw_assg_raw.size(9 - 16)) |
|
128 apply(simp) |
|
129 *) |
|
130 |
|
131 ML {* |
|
132 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
|
133 *} |
|
134 |
|
135 section {* NOT *} |
|
136 |
|
137 |
|
138 ML {* |
|
139 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} |
|
140 *} |
|
141 |
|
142 |
|
143 ML {* |
|
144 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} |
|
145 *} |
|
146 |
|
147 ML {* |
|
148 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
|
149 *} |
|
150 |
|
151 |
|
152 ML {* |
|
153 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} |
|
154 *} |
71 |
155 |
72 instance trm :: pt sorry |
156 instance trm :: pt sorry |
73 instance assg :: pt sorry |
157 instance assg :: pt sorry |
74 |
158 |
75 lemma b1: |
159 |
76 "p \<bullet> Var name = Var (p \<bullet> name)" |
160 |
77 "p \<bullet> App trm1 trm2 = App (p \<bullet> trm1) (p \<bullet> trm2)" |
161 |
78 "p \<bullet> Lam name trm = Lam (p \<bullet> name) (p \<bullet> trm)" |
162 |
79 "p \<bullet> Let assg trm = Let (p \<bullet> assg) (p \<bullet> trm)" |
163 |
80 "p \<bullet> Foo name1 name2 trm1 trm2 trm3 = |
164 |
81 Foo (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm1) (p \<bullet> trm2) (p \<bullet> trm3)" |
165 |
82 "p \<bullet> Bar name1 name2 trm = Bar (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm)" |
166 |
83 "p \<bullet> Baz name trm1 trm2 = Baz (p \<bullet> name) (p \<bullet> trm1) (p \<bullet> trm2)" |
|
84 "p \<bullet> As name1 name2 trm = As (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm)" |
|
85 sorry |
|
86 |
|
87 |
|
88 (* |
|
89 ML {* |
|
90 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_defs} |
|
91 *} |
|
92 *) |
|
93 |
167 |
94 thm eq_iff[no_vars] |
168 thm eq_iff[no_vars] |
95 |
169 |
96 ML {* |
170 ML {* |
97 val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)} |
171 val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)} |