# HG changeset patch # User blanchet # Date 1377857122 -7200 # Node ID 29c267cb9314a948302774b1ff7f94684b826f6d # Parent cfef783090ebf5d32fd84f51f34e19a0bce86de6 rationalized files diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 11:37:22 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:05:22 2013 +0200 @@ -11,7 +11,10 @@ theory BNF_FP_Basic imports BNF_Comp BNF_Ctr_Sugar keywords - "defaults" + "primrec_new" :: thy_decl and + "primcorec" :: thy_goal and + "defaults" and + "sequential" begin lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" @@ -153,8 +156,21 @@ lemma eq_subset: "op = \ (\a b. P a b \ a = b)" by auto +lemma if_if_True: + "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = + (if b then x else if b' then x' else f y')" + by simp + +lemma if_if_False: + "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) = + (if b then f y else if b' then x' else f y')" + by simp + ML_file "Tools/bnf_fp_util.ML" ML_file "Tools/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/bnf_fp_def_sugar.ML" +ML_file "Tools/bnf_fp_rec_sugar_util.ML" +ML_file "Tools/bnf_fp_rec_sugar_tactics.ML" +ML_file "Tools/bnf_fp_rec_sugar.ML" end diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_FP_Rec_Sugar.thy --- a/src/HOL/BNF/BNF_FP_Rec_Sugar.thy Fri Aug 30 11:37:22 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -(* Title: HOL/BNF/BNF_FP_Rec_Sugar.thy - Author: Lorenz Panny, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Author: Dmitriy Traytel, TU Muenchen - Copyright 2013 - -Recursor and corecursor sugar. -*) - -header {* Recursor and Corecursor Sugar *} - -theory BNF_FP_Rec_Sugar -imports BNF_FP_N2M -keywords - "primrec_new" :: thy_decl and - "primcorec" :: thy_goal and - "sequential" -begin - -lemma if_if_True: -"(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = - (if b then x else if b' then x' else f y')" -by simp - -lemma if_if_False: -"(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) = - (if b then f y else if b' then x' else f y')" -by simp - -ML_file "Tools/bnf_fp_rec_sugar_util.ML" -ML_file "Tools/bnf_fp_rec_sugar_tactics.ML" -ML_file "Tools/bnf_fp_rec_sugar.ML" - -end diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 11:37:22 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:05:22 2013 +0200 @@ -1,6 +1,8 @@ (* Title: HOL/BNF/BNF_LFP.thy Author: Dmitriy Traytel, TU Muenchen - Copyright 2012 + Author: Lorenz Panny, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012, 2013 Least fixed point operation on bounded natural functors. *) @@ -10,7 +12,8 @@ theory BNF_LFP imports BNF_FP_Basic keywords - "datatype_new" :: thy_decl + "datatype_new" :: thy_decl and + "datatype_compat" :: thy_decl begin lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" @@ -232,5 +235,6 @@ ML_file "Tools/bnf_lfp_util.ML" ML_file "Tools/bnf_lfp_tactics.ML" ML_file "Tools/bnf_lfp.ML" +ML_file "Tools/bnf_lfp_compat.ML" end diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_LFP_Compat.thy --- a/src/HOL/BNF/BNF_LFP_Compat.thy Fri Aug 30 11:37:22 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/BNF/BNF_LFP_Compat.thy - Author: Jasmin Blanchette, TU Muenchen - Copyright 2013 - -Compatibility layer with the old datatype package. -*) - -header {* Compatibility Layer with the Old Datatype Package *} - -theory BNF_LFP_Compat -imports BNF_FP_N2M -keywords - "datatype_compat" :: thy_goal -begin - -ML_file "Tools/bnf_lfp_compat.ML" - -end