equal
deleted
inserted
replaced
162 HOLogic.mk_eq (app fs r $ Free p, |
162 HOLogic.mk_eq (app fs r $ Free p, |
163 the (size_of_type tab extra_size size_ofp T) $ Free p); |
163 the (size_of_type tab extra_size size_ofp T) $ Free p); |
164 |
164 |
165 fun prove_unfolded_size_eqs size_ofp fs = |
165 fun prove_unfolded_size_eqs size_ofp fs = |
166 if null recTs2 then [] |
166 if null recTs2 then [] |
167 else split_conj_thm (SkipProof.prove ctxt xs [] |
167 else split_conj_thm (Skip_Proof.prove ctxt xs [] |
168 (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @ |
168 (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @ |
169 map (mk_unfolded_size_eq (AList.lookup op = |
169 map (mk_unfolded_size_eq (AList.lookup op = |
170 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
170 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
171 (xs ~~ recTs2 ~~ rec_combs2)))) |
171 (xs ~~ recTs2 ~~ rec_combs2)))) |
172 (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
172 (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
196 val simpset3 = HOL_basic_ss addsimps |
196 val simpset3 = HOL_basic_ss addsimps |
197 rec_rewrites @ size_def_thms' @ unfolded_size_eqs2; |
197 rec_rewrites @ size_def_thms' @ unfolded_size_eqs2; |
198 |
198 |
199 fun prove_size_eqs p size_fns size_ofp simpset = |
199 fun prove_size_eqs p size_fns size_ofp simpset = |
200 maps (fn (((_, (_, _, constrs)), size_const), T) => |
200 maps (fn (((_, (_, _, constrs)), size_const), T) => |
201 map (fn constr => Drule.standard (SkipProof.prove ctxt [] [] |
201 map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] [] |
202 (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) |
202 (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns)) |
203 size_ofp size_const T constr) |
203 size_ofp size_const T constr) |
204 (fn _ => simp_tac simpset 1))) constrs) |
204 (fn _ => simp_tac simpset 1))) constrs) |
205 (descr' ~~ size_fns ~~ recTs1); |
205 (descr' ~~ size_fns ~~ recTs1); |
206 |
206 |