# HG changeset patch # User blanchet # Date 1380629125 -7200 # Node ID 9fe1bd54d4378eaad72c45e56aff616df7594956 # Parent 132640f4c4534f887986ae08d6c204fd7b073051 renamed theory file diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/BNF_Ctr_Sugar.thy --- a/src/HOL/BNF/BNF_Ctr_Sugar.thy Tue Oct 01 12:53:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: HOL/BNF/BNF_Ctr_Sugar.thy - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Wrapping existing freely generated type's constructors. -*) - -header {* Wrapping Existing Freely Generated Type's Constructors *} - -theory BNF_Ctr_Sugar -imports BNF_Util -keywords - "wrap_free_constructors" :: thy_goal and - "no_discs_sels" and - "rep_compat" -begin - -lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" -by (erule iffI) (erule contrapos_pn) - -lemma iff_contradict: -"\ P \ P \ Q \ Q \ R" -"\ Q \ P \ Q \ P \ R" -by blast+ - -ML_file "Tools/bnf_ctr_sugar_tactics.ML" -ML_file "Tools/bnf_ctr_sugar.ML" - -end diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/BNF_FP_Base.thy --- a/src/HOL/BNF/BNF_FP_Base.thy Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Base.thy Tue Oct 01 14:05:25 2013 +0200 @@ -10,7 +10,7 @@ header {* Shared Fixed Point Operations on Bounded Natural Functors *} theory BNF_FP_Base -imports BNF_Comp BNF_Ctr_Sugar +imports BNF_Comp Ctr_Sugar begin lemma not_TrueE: "\ True \ P" diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Ctr_Sugar.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Ctr_Sugar.thy Tue Oct 01 14:05:25 2013 +0200 @@ -0,0 +1,29 @@ +(* Title: HOL/BNF/Ctr_Sugar.thy + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Wrapping existing freely generated type's constructors. +*) + +header {* Wrapping Existing Freely Generated Type's Constructors *} + +theory Ctr_Sugar +imports BNF_Util +keywords + "wrap_free_constructors" :: thy_goal and + "no_discs_sels" and + "rep_compat" +begin + +lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" +by (erule iffI) (erule contrapos_pn) + +lemma iff_contradict: +"\ P \ P \ Q \ Q \ R" +"\ Q \ P \ Q \ P \ R" +by blast+ + +ML_file "Tools/bnf_ctr_sugar_tactics.ML" +ML_file "Tools/bnf_ctr_sugar.ML" + +end diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Oct 01 14:05:25 2013 +0200 @@ -5,7 +5,7 @@ Wrapping existing freely generated type's constructors. *) -signature BNF_CTR_SUGAR = +signature CTR_SUGAR = sig type ctr_sugar = {ctrs: term list, @@ -57,11 +57,11 @@ val parse_bound_term: (binding * string) parser end; -structure BNF_Ctr_Sugar : BNF_CTR_SUGAR = +structure Ctr_Sugar : CTR_SUGAR = struct open BNF_Util -open BNF_Ctr_Sugar_Tactics +open Ctr_Sugar_Tactics type ctr_sugar = {ctrs: term list, diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Tue Oct 01 14:05:25 2013 +0200 @@ -5,7 +5,7 @@ Tactics for wrapping existing freely generated type's constructors. *) -signature BNF_CTR_SUGAR_TACTICS = +signature CTR_SUGAR_TACTICS = sig val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic @@ -26,7 +26,7 @@ val mk_unique_disc_def_tac: int -> thm -> tactic end; -structure BNF_Ctr_Sugar_Tactics : BNF_CTR_SUGAR_TACTICS = +structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS = struct open BNF_Util diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Oct 01 14:05:25 2013 +0200 @@ -16,7 +16,7 @@ nesting_bnfs: BNF_Def.bnf list, fp_res: BNF_FP_Util.fp_result, ctr_defss: thm list list, - ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, + ctr_sugars: Ctr_Sugar.ctr_sugar list, co_iterss: term list list, mapss: thm list list, co_inducts: thm list, @@ -87,7 +87,7 @@ string * term list * term list list * ((term list list * term list list list) * (typ list * typ list list)) list -> thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> - int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> + int list list -> int list list -> int list -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> @@ -105,8 +105,8 @@ structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = struct +open Ctr_Sugar open BNF_Util -open BNF_Ctr_Sugar open BNF_Comp open BNF_Def open BNF_FP_Util diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Oct 01 14:05:25 2013 +0200 @@ -25,9 +25,9 @@ structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR = struct +open Ctr_Sugar open BNF_Util open BNF_Def -open BNF_Ctr_Sugar open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_FP_N2M diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Oct 01 14:05:25 2013 +0200 @@ -83,9 +83,9 @@ structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL = struct +open Ctr_Sugar open BNF_Util open BNF_Def -open BNF_Ctr_Sugar open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_FP_N2M_Sugar diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_lfp_compat.ML --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Tue Oct 01 12:53:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Tue Oct 01 14:05:25 2013 +0200 @@ -13,8 +13,8 @@ structure BNF_LFP_Compat : BNF_LFP_COMPAT = struct +open Ctr_Sugar open BNF_Util -open BNF_Ctr_Sugar open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_FP_N2M_Sugar