simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
authorblanchet
Tue Apr 23 17:15:44 2013 +0200 (2013-04-23)
changeset 51745a06a3c777add
parent 51744 0468af6546ff
child 51746 5af40820948b
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
src/HOL/BNF/BNF_FP.thy
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/BNF_FP.thy	Tue Apr 23 17:13:14 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_FP.thy	Tue Apr 23 17:15:44 2013 +0200
     1.3 @@ -116,6 +116,9 @@
     1.4  "\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
     1.5  by blast+
     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/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:13:14 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:15:44 2013 +0200
     2.3 @@ -550,8 +550,8 @@
     2.4  
     2.5              fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
     2.6                fold_thms lthy ctr_defs'
     2.7 -                 (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
     2.8 -                      sum_prod_thms_rel)
     2.9 +                 (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
    2.10 +                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
    2.11                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
    2.12                |> postproc
    2.13                |> singleton (Proof_Context.export names_lthy no_defs_lthy);