78 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
78 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
79 end; |
79 end; |
80 (* Copy from Term *) |
80 (* Copy from Term *) |
81 fun is_funtype (Type ("fun", [_, _])) = true |
81 fun is_funtype (Type ("fun", [_, _])) = true |
82 | is_funtype _ = false; |
82 | is_funtype _ = false; |
|
83 (* Similar to one in USyntax *) |
|
84 fun mk_pair (fst, snd) = |
|
85 let val ty1 = fastype_of fst |
|
86 val ty2 = fastype_of snd |
|
87 val c = HOLogic.pair_const ty1 ty2 |
|
88 in c $ fst $ snd |
|
89 end; |
|
90 |
83 *} |
91 *} |
84 |
|
85 |
92 |
86 ML {* |
93 ML {* |
87 (* Currently needs just one full_tname to access Datatype *) |
94 (* Currently needs just one full_tname to access Datatype *) |
88 fun define_raw_fv full_tname bindsall lthy = |
95 fun define_fv_alpha full_tname bindsall lthy = |
89 let |
96 let |
90 val thy = ProofContext.theory_of lthy; |
97 val thy = ProofContext.theory_of lthy; |
91 val {descr, ...} = Datatype.the_info thy full_tname; |
98 val {descr, ...} = Datatype.the_info thy full_tname; |
92 val sorts = []; (* TODO *) |
99 val sorts = []; (* TODO *) |
93 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
100 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
94 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
101 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
95 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
102 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
96 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
103 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
97 val fv_frees = map Free (fv_names ~~ fv_types); |
104 val fv_frees = map Free (fv_names ~~ fv_types); |
98 fun fv_eq_constr i (cname, dts) bindcs = |
105 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
|
106 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
|
107 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
|
108 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
|
109 fun fv_alpha_constr i (cname, dts) bindcs = |
99 let |
110 let |
100 val Ts = map (typ_of_dtyp descr sorts) dts; |
111 val Ts = map (typ_of_dtyp descr sorts) dts; |
101 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
112 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
102 val args = map Free (names ~~ Ts); |
113 val args = map Free (names ~~ Ts); |
|
114 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
|
115 val args2 = map Free (names2 ~~ Ts); |
103 val c = Const (cname, Ts ---> (nth_dtyp i)); |
116 val c = Const (cname, Ts ---> (nth_dtyp i)); |
104 val fv_c = nth fv_frees i; |
117 val fv_c = nth fv_frees i; |
105 fun fv_bind (NONE, i) = |
118 val alpha = nth alpha_frees i; |
|
119 fun fv_bind args (NONE, i) = |
106 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
120 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
107 (* TODO we assume that all can be 'atomized' *) |
121 (* TODO we assume that all can be 'atomized' *) |
108 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
122 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
109 mk_single_atom (nth args i) |
123 mk_single_atom (nth args i) |
110 | fv_bind (SOME f, i) = f $ (nth args i); |
124 | fv_bind args (SOME f, i) = f $ (nth args i); |
111 fun fv_arg ((dt, x), bindxs) = |
125 fun fv_arg ((dt, x), bindxs) = |
112 let |
126 let |
113 val arg = |
127 val arg = |
114 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
128 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
115 (* TODO: we just assume everything can be 'atomized' *) |
129 (* TODO: we just assume everything can be 'atomized' *) |
116 if (is_funtype o fastype_of) x then mk_atoms x else |
130 if (is_funtype o fastype_of) x then mk_atoms x else |
117 HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] |
131 HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] |
118 val sub = mk_union (map fv_bind bindxs) |
132 val sub = mk_union (map (fv_bind args) bindxs) |
119 in |
133 in |
120 mk_diff arg sub |
134 mk_diff arg sub |
121 end; |
135 end; |
122 val _ = tracing ("d" ^ string_of_int (length dts)); |
136 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
123 val _ = tracing (string_of_int (length args)); |
137 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))) |
124 val _ = tracing (string_of_int (length bindcs)); |
138 val alpha_rhs = |
|
139 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
|
140 fun alpha_arg ((dt, bindxs), (arg, arg2)) = |
|
141 if bindxs = [] then ( |
|
142 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
|
143 else (HOLogic.mk_eq (arg, arg2))) |
|
144 else |
|
145 if is_rec_type dt then let |
|
146 (* THE HARD CASE *) |
|
147 val lhs_binds = mk_union (map (fv_bind args) bindxs); |
|
148 val lhs = mk_pair (lhs_binds, arg); |
|
149 val rhs_binds = mk_union (map (fv_bind args2) bindxs); |
|
150 val rhs = mk_pair (rhs_binds, arg2); |
|
151 val alpha = nth alpha_frees (body_index dt); |
|
152 val fv = nth fv_frees (body_index dt); |
|
153 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs; |
|
154 val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre |
|
155 in |
|
156 HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t) |
|
157 (* TODO Add some test that is makes sense *) |
|
158 end else @{term "True"} |
|
159 val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2)) |
|
160 val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs) |
125 in |
161 in |
126 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
162 (fv_eq, alpha_eq) |
127 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
|
128 end; |
163 end; |
129 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
164 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds; |
130 val fv_eqs = flat (map2 fv_eq descr bindsall) |
165 val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall)) |
|
166 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
|
167 val (fvs, lthy') = (Primrec.add_primrec |
|
168 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
|
169 val (alphas, lthy'') = (Inductive.add_inductive_i |
|
170 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |
|
171 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
|
172 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
|
173 (add_binds alpha_eqs) [] lthy') |
131 in |
174 in |
132 (* The snd will be removed later *) |
175 ((fvs, alphas), lthy'') |
133 snd (Primrec.add_primrec |
|
134 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
|
135 end |
176 end |
136 *} |
177 *} |
137 |
178 |
138 ML {* |
179 (* tests |
139 fun define_alpha full_tname bindsall lthy = |
|
140 let |
|
141 val thy = ProofContext.theory_of lthy; |
|
142 val {descr, ...} = Datatype.the_info thy full_tname; |
|
143 val sorts = []; (* TODO *) |
|
144 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
145 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
|
146 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
|
147 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
|
148 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
|
149 fun alpha_eq_constr i (cname, dts) bindcs = |
|
150 let |
|
151 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
152 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
|
153 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
|
154 val args = map Free (names ~~ Ts); |
|
155 val args2 = map Free (names2 ~~ Ts); |
|
156 val c = Const (cname, Ts ---> (nth_dtyp i)); |
|
157 val alpha = nth alpha_frees i; |
|
158 in |
|
159 (Attrib.empty_binding, HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)))) |
|
160 end; |
|
161 fun alpha_eq (i, (_, _, constrs)) binds = map2 (alpha_eq_constr i) constrs binds; |
|
162 val alpha_eqs = flat (map2 alpha_eq descr bindsall) |
|
163 in |
|
164 (* The snd will be removed later *) |
|
165 snd (Inductive.add_inductive_i |
|
166 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |
|
167 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
|
168 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] (alpha_eqs) [] lthy) |
|
169 end |
|
170 *} |
|
171 |
|
172 atom_decl name |
180 atom_decl name |
173 |
181 |
174 (*datatype ty = |
182 datatype ty = |
175 Var "name set" |
183 Var "name set" |
176 |
184 |
177 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
185 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
178 |
186 |
179 local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *} |
187 local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *} |
180 print_theorems |
188 print_theorems |
181 *) |
189 |
182 |
190 |
183 datatype rtrm1 = |
191 datatype rtrm1 = |
184 rVr1 "name" |
192 rVr1 "name" |
185 | rAp1 "rtrm1" "rtrm1" |
193 | rAp1 "rtrm1" "rtrm1" |
186 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
194 | rLm1 "name" "rtrm1" --"name is bound in trm1" |