made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
authorblanchet
Wed Jun 18 17:42:24 2014 +0200 (2014-06-18)
changeset 5727988263522c31e
parent 57278 8f7d6f01a775
child 57280 6907432c47b9
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
     1.3 @@ -71,9 +71,6 @@
     1.4  "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
     1.5  by simp
     1.6  
     1.7 -lemma Inl_Inr_False: "(Inl x = Inr y) = False"
     1.8 -by simp
     1.9 -
    1.10  lemma prod_set_simps:
    1.11  "fsts (x, y) = {x}"
    1.12  "snds (x, y) = {y}"
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jun 18 17:42:24 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jun 18 17:42:24 2014 +0200
     2.3 @@ -1358,7 +1358,7 @@
     2.4                  fold_thms lthy ctr_defs'
     2.5                    (unfold_thms lthy (pre_rel_def :: abs_inverse ::
     2.6                         (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
     2.7 -                       @{thms vimage2p_def sum.inject Inl_Inr_False})
     2.8 +                       @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
     2.9                       (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
    2.10                  |> postproc
    2.11                  |> singleton (Proof_Context.export names_lthy no_defs_lthy);
     3.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Jun 18 17:42:24 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Jun 18 17:42:24 2014 +0200
     3.3 @@ -138,7 +138,8 @@
     3.4      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     3.5      etac notE THEN' atac ORELSE'
     3.6      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
     3.7 -       sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
     3.8 +         sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
     3.9 +       mapsx @ map_comps @ map_idents))) ORELSE'
    3.10      fo_rtac @{thm cong} ctxt ORELSE'
    3.11      rtac @{thm ext}));
    3.12