137 (map (fn th => th RS @{thm eq_reflection}) ths) [] atom |
137 (map (fn th => th RS @{thm eq_reflection}) ths) [] atom |
138 val (f, args) = strip_comb atom |
138 val (f, args) = strip_comb atom |
139 val subst = Pattern.match thy (split_t, atom) (Vartab.empty, Vartab.empty) |
139 val subst = Pattern.match thy (split_t, atom) (Vartab.empty, Vartab.empty) |
140 val (_, split_args) = strip_comb split_t |
140 val (_, split_args) = strip_comb split_t |
141 val match = split_args ~~ args |
141 val match = split_args ~~ args |
142 |
|
143 (* |
|
144 fun mk_prems_of_assm assm = |
|
145 let |
|
146 val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
|
147 val names = [] (* TODO *) |
|
148 val var_names = Name.variant_list names (map fst vTs) |
|
149 val vars = map Free (var_names ~~ (map snd vTs)) |
|
150 val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
|
151 val (HOLogic.dest_eq (HOLogic.dest_Trueprop prem)) |
|
152 val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
|
153 in |
|
154 (*mk_prems' inner_t (var_names @ names, prems' @ prems)*) error "asda" |
|
155 end |
|
156 *) |
|
157 val names = Term.add_free_names atom [] |
142 val names = Term.add_free_names atom [] |
158 val frees = map Free (Term.add_frees atom []) |
143 val frees = map Free (Term.add_frees atom []) |
159 val constname = Name.variant (map (Long_Name.base_name o fst) defs) |
144 val constname = Name.variant (map (Long_Name.base_name o fst) defs) |
160 ((Long_Name.base_name constname) ^ "_aux") |
145 ((Long_Name.base_name constname) ^ "_aux") |
161 val full_constname = Sign.full_bname thy constname |
146 val full_constname = Sign.full_bname thy constname |
165 let |
150 let |
166 val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
151 val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
167 val var_names = Name.variant_list names (map fst vTs) |
152 val var_names = Name.variant_list names (map fst vTs) |
168 val vars = map Free (var_names ~~ (map snd vTs)) |
153 val vars = map Free (var_names ~~ (map snd vTs)) |
169 val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
154 val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
170 fun mk_subst prem = |
155 fun partition_prem_subst prem = |
|
156 case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of |
|
157 (Free (x, T), r) => (NONE, SOME ((x, T), r)) |
|
158 | _ => (SOME prem, NONE) |
|
159 fun partition f xs = |
171 let |
160 let |
172 val (Free (x, T), r) = HOLogic.dest_eq (HOLogic.dest_Trueprop prem) |
161 fun partition' acc1 acc2 [] = (rev acc1, rev acc2) |
173 in |
162 | partition' acc1 acc2 (x :: xs) = |
174 ((x, T), r) |
163 let |
175 end |
164 val (y, z) = f x |
176 val subst = map mk_subst prems' |
165 val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1 |
|
166 val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2 |
|
167 in partition' acc1' acc2' xs end |
|
168 in partition' [] [] xs end |
|
169 val (prems'', subst) = partition partition_prem_subst prems' |
177 val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
170 val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
178 val def = Logic.mk_equals (lhs, inner_t) |
171 val pre_def = Logic.mk_equals (lhs, |
|
172 fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t) |
|
173 val def = Envir.expand_term_frees subst pre_def |
179 in |
174 in |
180 Envir.expand_term_frees subst def |
175 def |
181 end |
176 end |
182 val new_defs = map new_def assms |
177 val new_defs = map new_def assms |
183 val (definition, thy') = thy |
178 val (definition, thy') = thy |
184 |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |
179 |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |
185 |> fold_map Drule.add_axiom (map_index |
180 |> fold_map Drule.add_axiom (map_index |