equal
deleted
inserted
replaced
256 map con_compact spec' |
256 map con_compact spec' |
257 end |
257 end |
258 |
258 |
259 (* prove strictness rules for constructors *) |
259 (* prove strictness rules for constructors *) |
260 local |
260 local |
261 fun con_strict (con, args) = |
261 fun con_strict (con, args) = |
262 let |
262 let |
263 val rules = abs_strict :: @{thms con_strict_rules} |
263 val rules = abs_strict :: @{thms con_strict_rules} |
264 val (vs, nonlazy) = get_vars args |
264 val (vs, nonlazy) = get_vars args |
265 fun one_strict v' = |
265 fun one_strict v' = |
266 let |
266 let |
495 val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}] |
495 val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}] |
496 val goal = mk_trp (mk_strict case_app) |
496 val goal = mk_trp (mk_strict case_app) |
497 val rules = @{thms sscase1 ssplit1 strictify1 one_case1} |
497 val rules = @{thms sscase1 ssplit1 strictify1 one_case1} |
498 val tacs = [resolve_tac rules 1] |
498 val tacs = [resolve_tac rules 1] |
499 in prove thy defs goal (K tacs) end |
499 in prove thy defs goal (K tacs) end |
500 |
500 |
501 (* prove rewrites for case combinator *) |
501 (* prove rewrites for case combinator *) |
502 local |
502 local |
503 fun one_case (con, args) f = |
503 fun one_case (con, args) f = |
504 let |
504 let |
505 val (vs, nonlazy) = get_vars args |
505 val (vs, nonlazy) = get_vars args |
735 val simps = dis_apps @ @{thms dist_eq_tr} |
735 val simps = dis_apps @ @{thms dist_eq_tr} |
736 val tacs = |
736 val tacs = |
737 [rtac @{thm iffI} 1, |
737 [rtac @{thm iffI} 1, |
738 asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2, |
738 asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2, |
739 rtac exhaust 1, atac 1, |
739 rtac exhaust 1, atac 1, |
740 DETERM_UNTIL_SOLVED (CHANGED |
740 ALLGOALS (asm_full_simp_tac (simple_ss addsimps simps))] |
741 (asm_full_simp_tac (simple_ss addsimps simps) 1))] |
|
742 val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)) |
741 val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)) |
743 in prove thy [] goal (K tacs) end |
742 in prove thy [] goal (K tacs) end |
744 in |
743 in |
745 val dis_defins = map dis_defin dis_consts |
744 val dis_defins = map dis_defin dis_consts |
746 end |
745 end |