1992
|
1 |
theory NewAlpha
|
2296
|
2 |
imports "Abs" "Perm"
|
1992
|
3 |
begin
|
|
4 |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
ML {*
|
2296
|
6 |
fun mk_prod_fv (t1, t2) =
|
|
7 |
let
|
|
8 |
val ty1 = fastype_of t1
|
|
9 |
val ty2 = fastype_of t2
|
|
10 |
val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
|
|
11 |
in
|
|
12 |
Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
|
|
13 |
end
|
2073
2bfd5be8578a
compound versions with prod_rel and prod_fun, not made default yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
14 |
*}
|
2bfd5be8578a
compound versions with prod_rel and prod_fun, not made default yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
15 |
|
2bfd5be8578a
compound versions with prod_rel and prod_fun, not made default yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
16 |
ML {*
|
2296
|
17 |
fun mk_prod_alpha (t1, t2) =
|
|
18 |
let
|
|
19 |
val ty1 = fastype_of t1
|
|
20 |
val ty2 = fastype_of t2
|
|
21 |
val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
|
|
22 |
val resT = [prodT, prodT] ---> @{typ "bool"}
|
|
23 |
in
|
|
24 |
Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
|
|
25 |
end
|
2073
2bfd5be8578a
compound versions with prod_rel and prod_fun, not made default yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
26 |
*}
|
1992
|
27 |
|
|
28 |
ML {*
|
2296
|
29 |
fun mk_binders lthy bmode args bodies =
|
|
30 |
let
|
|
31 |
fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
|
|
32 |
| bind_set _ args (SOME bn, i) = bn $ (nth args i)
|
|
33 |
fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
|
|
34 |
| bind_lst _ args (SOME bn, i) = bn $ (nth args i)
|
|
35 |
|
|
36 |
val (connect_fn, bind_fn) =
|
|
37 |
case bmode of
|
|
38 |
Lst => (mk_append, bind_lst)
|
|
39 |
| Set => (mk_union, bind_set)
|
|
40 |
| Res => (mk_union, bind_set)
|
|
41 |
in
|
|
42 |
foldl1 connect_fn (map (bind_fn lthy args) bodies)
|
|
43 |
end
|
|
44 |
*}
|
|
45 |
|
|
46 |
ML {*
|
|
47 |
fun mk_alpha_prem bmode fv alpha args args' binders binders' =
|
1992
|
48 |
let
|
2296
|
49 |
val (alpha_name, binder_ty) =
|
|
50 |
case bmode of
|
|
51 |
Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
|
|
52 |
| Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
|
|
53 |
| Res => (@{const_name "alpha_res"}, @{typ "atom set"})
|
|
54 |
val ty = fastype_of args
|
|
55 |
val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
|
|
56 |
val alpha_ty = [ty, ty] ---> @{typ "bool"}
|
|
57 |
val fv_ty = ty --> @{typ "atom set"}
|
1992
|
58 |
in
|
2296
|
59 |
HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
|
|
60 |
Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
|
|
61 |
$ HOLogic.mk_prod (binders, args) $ alpha $ fv $ (Bound 0) $ HOLogic.mk_prod (binders', args'))
|
1992
|
62 |
end
|
|
63 |
*}
|
|
64 |
|
|
65 |
ML {*
|
2296
|
66 |
fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
|
|
67 |
case binder of
|
|
68 |
(NONE, i) => []
|
|
69 |
| (SOME bn, i) =>
|
|
70 |
if member (op=) bodies i
|
|
71 |
then []
|
|
72 |
else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
|
1992
|
73 |
*}
|
|
74 |
|
|
75 |
ML {*
|
2296
|
76 |
fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
|
1992
|
77 |
let
|
2296
|
78 |
fun mk_frees i =
|
|
79 |
let
|
|
80 |
val arg = nth args i
|
|
81 |
val arg' = nth args' i
|
|
82 |
val ty = fastype_of arg
|
|
83 |
in
|
|
84 |
if nth is_rec i
|
|
85 |
then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
|
|
86 |
else HOLogic.mk_eq (arg, arg')
|
|
87 |
end
|
|
88 |
fun mk_alpha_fv i =
|
|
89 |
let
|
|
90 |
val ty = fastype_of (nth args i)
|
|
91 |
in
|
|
92 |
case AList.lookup (op=) alpha_map ty of
|
|
93 |
NONE => (HOLogic.eq_const ty, supp_const ty)
|
|
94 |
| SOME (alpha, fv) => (alpha, fv)
|
|
95 |
end
|
|
96 |
|
1992
|
97 |
in
|
2296
|
98 |
case bclause of
|
|
99 |
BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
|
|
100 |
| BC (bmode, binders, bodies) =>
|
|
101 |
let
|
|
102 |
val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
|
|
103 |
val comp_fv = foldl1 mk_prod_fv fvs
|
|
104 |
val comp_alpha = foldl1 mk_prod_alpha alphas
|
|
105 |
val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
|
|
106 |
val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
|
|
107 |
val comp_binders = mk_binders lthy bmode args binders
|
|
108 |
val comp_binders' = mk_binders lthy bmode args' binders
|
|
109 |
val alpha_prem =
|
|
110 |
mk_alpha_prem bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
|
|
111 |
val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
|
|
112 |
in
|
|
113 |
map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
|
|
114 |
end
|
1992
|
115 |
end
|
|
116 |
*}
|
|
117 |
|
|
118 |
ML {*
|
2296
|
119 |
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
|
1992
|
120 |
let
|
2296
|
121 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
122 |
val arg_names' = Name.variant_list arg_names arg_names
|
|
123 |
val args = map Free (arg_names ~~ arg_tys)
|
|
124 |
val args' = map Free (arg_names' ~~ arg_tys)
|
|
125 |
val alpha = fst (the (AList.lookup (op=) alpha_map ty))
|
|
126 |
val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
|
|
127 |
val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
|
1992
|
128 |
in
|
2296
|
129 |
Library.foldr Logic.mk_implies (flat prems, concl)
|
1992
|
130 |
end
|
|
131 |
*}
|
|
132 |
|
|
133 |
ML {*
|
2296
|
134 |
fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
|
|
135 |
let
|
|
136 |
fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i =
|
|
137 |
let
|
|
138 |
val arg = nth args i
|
|
139 |
val arg' = nth args' i
|
|
140 |
val ty = fastype_of arg
|
|
141 |
in
|
|
142 |
case AList.lookup (op=) bn_args i of
|
|
143 |
NONE => (case (AList.lookup (op=) alpha_map ty) of
|
|
144 |
NONE => [HOLogic.mk_eq (arg, arg')]
|
|
145 |
| SOME (alpha, _) => [alpha $ arg $ arg'])
|
|
146 |
| SOME (NONE) => []
|
|
147 |
| SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']
|
|
148 |
end
|
|
149 |
in
|
|
150 |
case bclause of
|
|
151 |
BC (_, [], bodies) =>
|
|
152 |
map HOLogic.mk_Trueprop
|
|
153 |
(flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
|
|
154 |
| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
|
|
155 |
end
|
1992
|
156 |
*}
|
|
157 |
|
|
158 |
ML {*
|
2296
|
159 |
fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
|
1992
|
160 |
let
|
2296
|
161 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
162 |
val arg_names' = Name.variant_list arg_names arg_names
|
|
163 |
val args = map Free (arg_names ~~ arg_tys)
|
|
164 |
val args' = map Free (arg_names' ~~ arg_tys)
|
|
165 |
val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
|
|
166 |
val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
|
|
167 |
val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
|
1992
|
168 |
in
|
2296
|
169 |
Library.foldr Logic.mk_implies (flat prems, concl)
|
1992
|
170 |
end
|
|
171 |
*}
|
|
172 |
|
|
173 |
ML {*
|
2296
|
174 |
fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
|
1992
|
175 |
let
|
2296
|
176 |
val nth_constrs_info = nth constrs_info bn_n
|
|
177 |
val nth_bclausess = nth bclausesss bn_n
|
|
178 |
in
|
|
179 |
map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
|
|
180 |
end
|
|
181 |
*}
|
1992
|
182 |
|
2296
|
183 |
ML {*
|
|
184 |
fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy =
|
|
185 |
let
|
|
186 |
val alpha_names = prefix_dt_names descr sorts "alpha_"
|
|
187 |
val alpha_arg_tys = all_dtyps descr sorts
|
|
188 |
val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
|
|
189 |
val alpha_frees = map Free (alpha_names ~~ alpha_tys)
|
|
190 |
val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
|
1992
|
191 |
|
2296
|
192 |
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
|
|
193 |
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
|
|
194 |
val alpha_bn_names = map (prefix "alpha_") bn_names
|
|
195 |
val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
|
|
196 |
val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
|
|
197 |
val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
|
|
198 |
val alpha_bn_map = bns ~~ alpha_bn_frees
|
1992
|
199 |
|
2296
|
200 |
val constrs_info = all_dtyp_constrs_types descr sorts
|
1992
|
201 |
|
2296
|
202 |
val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss
|
|
203 |
val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
|
1992
|
204 |
|
|
205 |
val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
|
2296
|
206 |
(alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)
|
|
207 |
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
|
|
208 |
|
1992
|
209 |
val (alphas, lthy') = Inductive.add_inductive_i
|
|
210 |
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
|
|
211 |
coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
|
2296
|
212 |
all_alpha_names [] all_alpha_intros [] lthy
|
1996
|
213 |
|
2296
|
214 |
val alpha_trms_loc = #preds alphas;
|
2108
|
215 |
val alpha_induct_loc = #raw_induct alphas;
|
1996
|
216 |
val alpha_intros_loc = #intrs alphas;
|
|
217 |
val alpha_cases_loc = #elims alphas;
|
2296
|
218 |
val phi = ProofContext.export_morphism lthy' lthy;
|
1996
|
219 |
|
2296
|
220 |
val alpha_trms = map (Morphism.term phi) alpha_trms_loc;
|
|
221 |
val alpha_induct = Morphism.thm phi alpha_induct_loc;
|
|
222 |
val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
|
|
223 |
val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
|
1992
|
224 |
in
|
2296
|
225 |
(alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
|
1992
|
226 |
end
|
|
227 |
*}
|
|
228 |
|
2296
|
229 |
ML {* ProofContext.export_morphism *}
|
|
230 |
|
1992
|
231 |
end
|