62 match_rews : thm list |
62 match_rews : thm list |
63 } |
63 } |
64 |
64 |
65 (************************** miscellaneous functions ***************************) |
65 (************************** miscellaneous functions ***************************) |
66 |
66 |
67 val simple_ss = HOL_basic_ss addsimps @{thms simp_thms} |
67 val simple_ss = |
|
68 simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms}) |
68 |
69 |
69 val beta_rules = |
70 val beta_rules = |
70 @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ |
71 @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ |
71 @{thms cont2cont_fst cont2cont_snd cont2cont_Pair} |
72 @{thms cont2cont_fst cont2cont_snd cont2cont_Pair} |
72 |
73 |
73 val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules) |
74 val beta_ss = |
|
75 simpset_of (put_simpset HOL_basic_ss @{context} addsimps (@{thms simp_thms} @ beta_rules)) |
74 |
76 |
75 fun define_consts |
77 fun define_consts |
76 (specs : (binding * term * mixfix) list) |
78 (specs : (binding * term * mixfix) list) |
77 (thy : theory) |
79 (thy : theory) |
78 : (term list * thm list) * theory = |
80 : (term list * thm list) * theory = |
266 fun one_strict v' = |
268 fun one_strict v' = |
267 let |
269 let |
268 val bottom = mk_bottom (fastype_of v') |
270 val bottom = mk_bottom (fastype_of v') |
269 val vs' = map (fn v => if v = v' then bottom else v) vs |
271 val vs' = map (fn v => if v = v' then bottom else v) vs |
270 val goal = mk_trp (mk_undef (list_ccomb (con, vs'))) |
272 val goal = mk_trp (mk_undef (list_ccomb (con, vs'))) |
271 val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1] |
273 val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1] |
272 in prove thy con_betas goal (K tacs) end |
274 in prove thy con_betas goal (K tacs) end |
273 in map one_strict nonlazy end |
275 in map one_strict nonlazy end |
274 |
276 |
275 fun con_defin (con, args) = |
277 fun con_defin (con, args) = |
276 let |
278 let |
280 val lhs = mk_undef (list_ccomb (con, vs)) |
282 val lhs = mk_undef (list_ccomb (con, vs)) |
281 val rhss = map mk_undef nonlazy |
283 val rhss = map mk_undef nonlazy |
282 val goal = mk_trp (iff_disj (lhs, rhss)) |
284 val goal = mk_trp (iff_disj (lhs, rhss)) |
283 val rule1 = iso_locale RS @{thm iso.abs_bottom_iff} |
285 val rule1 = iso_locale RS @{thm iso.abs_bottom_iff} |
284 val rules = rule1 :: @{thms con_bottom_iff_rules} |
286 val rules = rule1 :: @{thms con_bottom_iff_rules} |
285 val tacs = [simp_tac (HOL_ss addsimps rules) 1] |
287 val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1] |
286 in prove thy con_betas goal (K tacs) end |
288 in prove thy con_betas goal (K tacs) end |
287 in |
289 in |
288 val con_stricts = maps con_strict spec' |
290 val con_stricts = maps con_strict spec' |
289 val con_defins = map con_defin spec' |
291 val con_defins = map con_defin spec' |
290 val con_rews = con_stricts @ con_defins |
292 val con_rews = con_stricts @ con_defins |
311 let |
313 let |
312 val abs_below = iso_locale RS @{thm iso.abs_below} |
314 val abs_below = iso_locale RS @{thm iso.abs_below} |
313 val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below} |
315 val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below} |
314 val rules2 = @{thms up_defined spair_defined ONE_defined} |
316 val rules2 = @{thms up_defined spair_defined ONE_defined} |
315 val rules = rules1 @ rules2 |
317 val rules = rules1 @ rules2 |
316 val tacs = [asm_simp_tac (simple_ss addsimps rules) 1] |
318 val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1] |
317 in map (fn c => pgterm mk_below c (K tacs)) cons' end |
319 in map (fn c => pgterm mk_below c (K tacs)) cons' end |
318 val injects = |
320 val injects = |
319 let |
321 let |
320 val abs_eq = iso_locale RS @{thm iso.abs_eq} |
322 val abs_eq = iso_locale RS @{thm iso.abs_eq} |
321 val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq} |
323 val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq} |
322 val rules2 = @{thms up_defined spair_defined ONE_defined} |
324 val rules2 = @{thms up_defined spair_defined ONE_defined} |
323 val rules = rules1 @ rules2 |
325 val rules = rules1 @ rules2 |
324 val tacs = [asm_simp_tac (simple_ss addsimps rules) 1] |
326 val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1] |
325 in map (fn c => pgterm mk_eq c (K tacs)) cons' end |
327 in map (fn c => pgterm mk_eq c (K tacs)) cons' end |
326 end |
328 end |
327 |
329 |
328 (* prove distinctness of constructors *) |
330 (* prove distinctness of constructors *) |
329 local |
331 local |
344 val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)) |
346 val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)) |
345 val rhss = map mk_undef zs1 |
347 val rhss = map mk_undef zs1 |
346 val goal = mk_trp (iff_disj (lhs, rhss)) |
348 val goal = mk_trp (iff_disj (lhs, rhss)) |
347 val rule1 = iso_locale RS @{thm iso.abs_below} |
349 val rule1 = iso_locale RS @{thm iso.abs_below} |
348 val rules = rule1 :: @{thms con_below_iff_rules} |
350 val rules = rule1 :: @{thms con_below_iff_rules} |
349 val tacs = [simp_tac (HOL_ss addsimps rules) 1] |
351 val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1] |
350 in prove thy con_betas goal (K tacs) end |
352 in prove thy con_betas goal (K tacs) end |
351 fun dist_eq (con1, args1) (con2, args2) = |
353 fun dist_eq (con1, args1) (con2, args2) = |
352 let |
354 let |
353 val (vs1, zs1) = get_vars args1 |
355 val (vs1, zs1) = get_vars args1 |
354 val (vs2, zs2) = get_vars args2 |> pairself (map prime) |
356 val (vs2, zs2) = get_vars args2 |> pairself (map prime) |
356 val rhss1 = map mk_undef zs1 |
358 val rhss1 = map mk_undef zs1 |
357 val rhss2 = map mk_undef zs2 |
359 val rhss2 = map mk_undef zs2 |
358 val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)) |
360 val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)) |
359 val rule1 = iso_locale RS @{thm iso.abs_eq} |
361 val rule1 = iso_locale RS @{thm iso.abs_eq} |
360 val rules = rule1 :: @{thms con_eq_iff_rules} |
362 val rules = rule1 :: @{thms con_eq_iff_rules} |
361 val tacs = [simp_tac (HOL_ss addsimps rules) 1] |
363 val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1] |
362 in prove thy con_betas goal (K tacs) end |
364 in prove thy con_betas goal (K tacs) end |
363 in |
365 in |
364 val dist_les = map_dist dist_le spec' |
366 val dist_les = map_dist dist_le spec' |
365 val dist_eqs = map_dist dist_eq spec' |
367 val dist_eqs = map_dist dist_eq spec' |
366 end |
368 end |
512 val defs = case_beta :: con_betas |
514 val defs = case_beta :: con_betas |
513 val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1} |
515 val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1} |
514 val rules2 = @{thms con_bottom_iff_rules} |
516 val rules2 = @{thms con_bottom_iff_rules} |
515 val rules3 = @{thms cfcomp2 one_case2} |
517 val rules3 = @{thms cfcomp2 one_case2} |
516 val rules = abs_inverse :: rules1 @ rules2 @ rules3 |
518 val rules = abs_inverse :: rules1 @ rules2 @ rules3 |
517 val tacs = [asm_simp_tac (beta_ss addsimps rules) 1] |
519 val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1] |
518 in prove thy defs goal (K tacs) end |
520 in prove thy defs goal (K tacs) end |
519 in |
521 in |
520 val case_apps = map2 one_case spec fs |
522 val case_apps = map2 one_case spec fs |
521 end |
523 end |
522 |
524 |
580 |
582 |
581 (* prove selector strictness rules *) |
583 (* prove selector strictness rules *) |
582 val sel_stricts : thm list = |
584 val sel_stricts : thm list = |
583 let |
585 let |
584 val rules = rep_strict :: @{thms sel_strict_rules} |
586 val rules = rep_strict :: @{thms sel_strict_rules} |
585 val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1] |
587 val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1] |
586 fun sel_strict sel = |
588 fun sel_strict sel = |
587 let |
589 let |
588 val goal = mk_trp (mk_strict sel) |
590 val goal = mk_trp (mk_strict sel) |
589 in |
591 in |
590 prove thy sel_defs goal (K tacs) |
592 prove thy sel_defs goal (K tacs) |
596 (* prove selector application rules *) |
598 (* prove selector application rules *) |
597 val sel_apps : thm list = |
599 val sel_apps : thm list = |
598 let |
600 let |
599 val defs = con_betas @ sel_defs |
601 val defs = con_betas @ sel_defs |
600 val rules = abs_inv :: @{thms sel_app_rules} |
602 val rules = abs_inv :: @{thms sel_app_rules} |
601 val tacs = [asm_simp_tac (simple_ss addsimps rules) 1] |
603 val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1] |
602 fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) = |
604 fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) = |
603 let |
605 let |
604 val Ts : typ list = map #3 args |
606 val Ts : typ list = map #3 args |
605 val ns : string list = Datatype_Prop.make_tnames Ts |
607 val ns : string list = Datatype_Prop.make_tnames Ts |
606 val vs : term list = map Free (ns ~~ Ts) |
608 val vs : term list = map Free (ns ~~ Ts) |
641 |
643 |
642 (* prove selector definedness rules *) |
644 (* prove selector definedness rules *) |
643 val sel_defins : thm list = |
645 val sel_defins : thm list = |
644 let |
646 let |
645 val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules} |
647 val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules} |
646 val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1] |
648 val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1] |
647 fun sel_defin sel = |
649 fun sel_defin sel = |
648 let |
650 let |
649 val (T, U) = dest_cfunT (fastype_of sel) |
651 val (T, U) = dest_cfunT (fastype_of sel) |
650 val x = Free ("x", T) |
652 val x = Free ("x", T) |
651 val lhs = mk_eq (sel ` x, mk_bottom U) |
653 val lhs = mk_eq (sel ` x, mk_bottom U) |
718 val lhs = dis ` list_ccomb (con, vs) |
720 val lhs = dis ` list_ccomb (con, vs) |
719 val rhs = if i = j then @{term TT} else @{term FF} |
721 val rhs = if i = j then @{term TT} else @{term FF} |
720 val assms = map (mk_trp o mk_defined) nonlazy |
722 val assms = map (mk_trp o mk_defined) nonlazy |
721 val concl = mk_trp (mk_eq (lhs, rhs)) |
723 val concl = mk_trp (mk_eq (lhs, rhs)) |
722 val goal = Logic.list_implies (assms, concl) |
724 val goal = Logic.list_implies (assms, concl) |
723 val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1] |
725 val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1] |
724 in prove thy dis_defs goal (K tacs) end |
726 in prove thy dis_defs goal (K tacs) end |
725 fun one_dis (i, dis) = |
727 fun one_dis (i, dis) = |
726 map_index (dis_app (i, dis)) spec |
728 map_index (dis_app (i, dis)) spec |
727 in |
729 in |
728 val dis_apps = flat (map_index one_dis dis_consts) |
730 val dis_apps = flat (map_index one_dis dis_consts) |
734 let |
736 let |
735 val x = Free ("x", lhsT) |
737 val x = Free ("x", lhsT) |
736 val simps = dis_apps @ @{thms dist_eq_tr} |
738 val simps = dis_apps @ @{thms dist_eq_tr} |
737 val tacs = |
739 val tacs = |
738 [rtac @{thm iffI} 1, |
740 [rtac @{thm iffI} 1, |
739 asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2, |
741 asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps dis_stricts) 2, |
740 rtac exhaust 1, atac 1, |
742 rtac exhaust 1, atac 1, |
741 ALLGOALS (asm_full_simp_tac (simple_ss addsimps simps))] |
743 ALLGOALS (asm_full_simp_tac (Simplifier.global_context thy simple_ss addsimps simps))] |
742 val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)) |
744 val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)) |
743 in prove thy [] goal (K tacs) end |
745 in prove thy [] goal (K tacs) end |
744 in |
746 in |
745 val dis_defins = map dis_defin dis_consts |
747 val dis_defins = map dis_defin dis_consts |
746 end |
748 end |
807 fun match_strict mat = |
809 fun match_strict mat = |
808 let |
810 let |
809 val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)) |
811 val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)) |
810 val k = Free ("k", U) |
812 val k = Free ("k", U) |
811 val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V)) |
813 val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V)) |
812 val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1] |
814 val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1] |
813 in prove thy match_defs goal (K tacs) end |
815 in prove thy match_defs goal (K tacs) end |
814 in |
816 in |
815 val match_stricts = map match_strict match_consts |
817 val match_stricts = map match_strict match_consts |
816 end |
818 end |
817 |
819 |
826 val lhs = mat ` list_ccomb (con, vs) ` k |
828 val lhs = mat ` list_ccomb (con, vs) ` k |
827 val rhs = if i = j then list_ccomb (k, vs) else fail |
829 val rhs = if i = j then list_ccomb (k, vs) else fail |
828 val assms = map (mk_trp o mk_defined) nonlazy |
830 val assms = map (mk_trp o mk_defined) nonlazy |
829 val concl = mk_trp (mk_eq (lhs, rhs)) |
831 val concl = mk_trp (mk_eq (lhs, rhs)) |
830 val goal = Logic.list_implies (assms, concl) |
832 val goal = Logic.list_implies (assms, concl) |
831 val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1] |
833 val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1] |
832 in prove thy match_defs goal (K tacs) end |
834 in prove thy match_defs goal (K tacs) end |
833 fun one_match (i, mat) = |
835 fun one_match (i, mat) = |
834 map_index (match_app (i, mat)) spec |
836 map_index (match_app (i, mat)) spec |
835 in |
837 in |
836 val match_apps = flat (map_index one_match match_consts) |
838 val match_apps = flat (map_index one_match match_consts) |