equal
deleted
inserted
replaced
157 HOLogic.mk_eq (app fs r $ Free p, |
157 HOLogic.mk_eq (app fs r $ Free p, |
158 the (size_of_type tab extra_size size_ofp T) $ Free p); |
158 the (size_of_type tab extra_size size_ofp T) $ Free p); |
159 |
159 |
160 fun prove_unfolded_size_eqs size_ofp fs = |
160 fun prove_unfolded_size_eqs size_ofp fs = |
161 if null recTs2 then [] |
161 if null recTs2 then [] |
162 else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs [] |
162 else Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs [] |
163 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @ |
163 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @ |
164 map (mk_unfolded_size_eq (AList.lookup op = |
164 map (mk_unfolded_size_eq (AList.lookup op = |
165 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
165 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
166 (xs ~~ recTs2 ~~ rec_combs2)))) |
166 (xs ~~ recTs2 ~~ rec_combs2)))) |
167 (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
167 (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
191 val simpset3 = HOL_basic_ss addsimps |
191 val simpset3 = HOL_basic_ss addsimps |
192 rec_rewrites @ size_def_thms' @ unfolded_size_eqs2; |
192 rec_rewrites @ size_def_thms' @ unfolded_size_eqs2; |
193 |
193 |
194 fun prove_size_eqs p size_fns size_ofp simpset = |
194 fun prove_size_eqs p size_fns size_ofp simpset = |
195 maps (fn (((_, (_, _, constrs)), size_const), T) => |
195 maps (fn (((_, (_, _, constrs)), size_const), T) => |
196 map (fn constr => Drule.export_without_context (Skip_Proof.prove ctxt [] [] |
196 map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] [] |
197 (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) |
197 (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) |
198 size_ofp size_const T constr) |
198 size_ofp size_const T constr) |
199 (fn _ => simp_tac simpset 1))) constrs) |
199 (fn _ => simp_tac simpset 1))) constrs) |
200 (descr' ~~ size_fns ~~ recTs1); |
200 (descr' ~~ size_fns ~~ recTs1); |
201 |
201 |