510 end; |
510 end; |
511 |
511 |
512 val sel_rews = sel_stricts @ sel_defins @ sel_apps; |
512 val sel_rews = sel_stricts @ sel_defins @ sel_apps; |
513 |
513 |
514 val _ = trace " Proving dist_les..."; |
514 val _ = trace " Proving dist_les..."; |
515 val distincts_le = |
515 val dist_les = |
516 let |
516 let |
517 fun dist (con1, args1) (con2, args2) = |
517 fun dist (con1, args1) (con2, args2) = |
518 let |
518 let |
519 val goal = lift_defined %: (nonlazy args1, |
519 fun iff_disj (t, []) = HOLogic.mk_not t |
520 mk_trp (con_app con1 args1 ~<< con_app con2 args2)); |
520 | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; |
521 fun tacs ctxt = [ |
521 val lhs = con_app con1 args1 << con_app con2 args2; |
522 rtac @{thm rev_contrapos} 1, |
522 val rhss = map (fn x => %:x === UU) (nonlazy args1); |
523 eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] |
523 val goal = mk_trp (iff_disj (lhs, rhss)); |
524 @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2) |
524 val rule1 = iso_locale RS @{thm iso.abs_below}; |
525 @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; |
525 val rules = rule1 :: @{thms con_below_iff_rules}; |
526 in pg [] goal tacs end; |
526 val tacs = [simp_tac (HOL_ss addsimps rules) 1]; |
|
527 in pg con_appls goal (K tacs) end; |
527 |
528 |
528 fun distinct (con1, args1) (con2, args2) = |
529 fun distinct (con1, args1) (con2, args2) = |
529 let |
530 let |
530 val arg1 = (con1, args1); |
531 val arg1 = (con1, args1); |
531 val arg2 = |
532 val arg2 = |
532 (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) |
533 (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) |
533 (args2, Name.variant_list (map vname args1) (map vname args2))); |
534 (args2, Name.variant_list (map vname args1) (map vname args2))); |
534 in [dist arg1 arg2, dist arg2 arg1] end; |
535 in [dist arg1 arg2, dist arg2 arg1] end; |
535 fun distincts [] = [] |
536 fun distincts [] = [] |
536 | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; |
537 | distincts (c::cs) = maps (distinct c) cs @ distincts cs; |
537 in distincts cons end; |
538 in distincts cons end; |
538 val dist_les = flat (flat distincts_le); |
|
539 |
539 |
540 val _ = trace " Proving dist_eqs..."; |
540 val _ = trace " Proving dist_eqs..."; |
541 val dist_eqs = |
541 val dist_eqs = |
542 let |
542 let |
543 fun distinct (_,args1) ((_,args2), leqs) = |
543 fun dist (con1, args1) (con2, args2) = |
544 let |
544 let |
545 val (le1,le2) = (hd leqs, hd(tl leqs)); |
545 fun iff_disj (t, [], us) = HOLogic.mk_not t |
546 val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) |
546 | iff_disj (t, ts, []) = HOLogic.mk_not t |
547 in |
547 | iff_disj (t, ts, us) = |
548 if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else |
548 let |
549 if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else |
549 val disj1 = foldr1 HOLogic.mk_disj ts; |
550 [eq1, eq2] |
550 val disj2 = foldr1 HOLogic.mk_disj us; |
551 end; |
551 in t === HOLogic.mk_conj (disj1, disj2) end; |
|
552 val lhs = con_app con1 args1 === con_app con2 args2; |
|
553 val rhss1 = map (fn x => %:x === UU) (nonlazy args1); |
|
554 val rhss2 = map (fn x => %:x === UU) (nonlazy args2); |
|
555 val goal = mk_trp (iff_disj (lhs, rhss1, rhss2)); |
|
556 val rule1 = iso_locale RS @{thm iso.abs_eq}; |
|
557 val rules = rule1 :: @{thms con_eq_iff_rules}; |
|
558 val tacs = [simp_tac (HOL_ss addsimps rules) 1]; |
|
559 in pg con_appls goal (K tacs) end; |
|
560 |
|
561 fun distinct (con1, args1) (con2, args2) = |
|
562 let |
|
563 val arg1 = (con1, args1); |
|
564 val arg2 = |
|
565 (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) |
|
566 (args2, Name.variant_list (map vname args1) (map vname args2))); |
|
567 in [dist arg1 arg2, dist arg2 arg1] end; |
552 fun distincts [] = [] |
568 fun distincts [] = [] |
553 | distincts ((c,leqs)::cs) = |
569 | distincts (c::cs) = maps (distinct c) cs @ distincts cs; |
554 flat |
570 in distincts cons end; |
555 (ListPair.map (distinct c) ((map #1 cs),leqs)) @ |
|
556 distincts cs; |
|
557 in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end; |
|
558 |
571 |
559 local |
572 local |
560 fun pgterm rel con args = |
573 fun pgterm rel con args = |
561 let |
574 let |
562 fun append s = upd_vname (fn v => v^s); |
575 fun append s = upd_vname (fn v => v^s); |