renamed theory file
authorblanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 540069fe1bd54d437
parent 54005 132640f4c453
child 54007 07028b08045f
renamed theory file
src/HOL/BNF/BNF_Ctr_Sugar.thy
src/HOL/BNF/BNF_FP_Base.thy
src/HOL/BNF/Ctr_Sugar.thy
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
src/HOL/BNF/Tools/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/BNF/BNF_Ctr_Sugar.thy	Tue Oct 01 12:53:24 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,29 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/BNF_Ctr_Sugar.thy
     1.5 -    Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2012
     1.7 -
     1.8 -Wrapping existing freely generated type's constructors.
     1.9 -*)
    1.10 -
    1.11 -header {* Wrapping Existing Freely Generated Type's Constructors *}
    1.12 -
    1.13 -theory BNF_Ctr_Sugar
    1.14 -imports BNF_Util
    1.15 -keywords
    1.16 -  "wrap_free_constructors" :: thy_goal and
    1.17 -  "no_discs_sels" and
    1.18 -  "rep_compat"
    1.19 -begin
    1.20 -
    1.21 -lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    1.22 -by (erule iffI) (erule contrapos_pn)
    1.23 -
    1.24 -lemma iff_contradict:
    1.25 -"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    1.26 -"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.27 -by blast+
    1.28 -
    1.29 -ML_file "Tools/bnf_ctr_sugar_tactics.ML"
    1.30 -ML_file "Tools/bnf_ctr_sugar.ML"
    1.31 -
    1.32 -end
     2.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Tue Oct 01 12:53:24 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Tue Oct 01 14:05:25 2013 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  header {* Shared Fixed Point Operations on Bounded Natural Functors *}
     2.5  
     2.6  theory BNF_FP_Base
     2.7 -imports BNF_Comp BNF_Ctr_Sugar
     2.8 +imports BNF_Comp Ctr_Sugar
     2.9  begin
    2.10  
    2.11  lemma not_TrueE: "\<not> True \<Longrightarrow> P"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/BNF/Ctr_Sugar.thy	Tue Oct 01 14:05:25 2013 +0200
     3.3 @@ -0,0 +1,29 @@
     3.4 +(*  Title:      HOL/BNF/Ctr_Sugar.thy
     3.5 +    Author:     Jasmin Blanchette, TU Muenchen
     3.6 +    Copyright   2012
     3.7 +
     3.8 +Wrapping existing freely generated type's constructors.
     3.9 +*)
    3.10 +
    3.11 +header {* Wrapping Existing Freely Generated Type's Constructors *}
    3.12 +
    3.13 +theory Ctr_Sugar
    3.14 +imports BNF_Util
    3.15 +keywords
    3.16 +  "wrap_free_constructors" :: thy_goal and
    3.17 +  "no_discs_sels" and
    3.18 +  "rep_compat"
    3.19 +begin
    3.20 +
    3.21 +lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    3.22 +by (erule iffI) (erule contrapos_pn)
    3.23 +
    3.24 +lemma iff_contradict:
    3.25 +"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    3.26 +"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    3.27 +by blast+
    3.28 +
    3.29 +ML_file "Tools/bnf_ctr_sugar_tactics.ML"
    3.30 +ML_file "Tools/bnf_ctr_sugar.ML"
    3.31 +
    3.32 +end
     4.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  Wrapping existing freely generated type's constructors.
     4.5  *)
     4.6  
     4.7 -signature BNF_CTR_SUGAR =
     4.8 +signature CTR_SUGAR =
     4.9  sig
    4.10    type ctr_sugar =
    4.11      {ctrs: term list,
    4.12 @@ -57,11 +57,11 @@
    4.13    val parse_bound_term: (binding * string) parser
    4.14  end;
    4.15  
    4.16 -structure BNF_Ctr_Sugar : BNF_CTR_SUGAR =
    4.17 +structure Ctr_Sugar : CTR_SUGAR =
    4.18  struct
    4.19  
    4.20  open BNF_Util
    4.21 -open BNF_Ctr_Sugar_Tactics
    4.22 +open Ctr_Sugar_Tactics
    4.23  
    4.24  type ctr_sugar =
    4.25    {ctrs: term list,
     5.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Tue Oct 01 12:53:24 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Tue Oct 01 14:05:25 2013 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  Tactics for wrapping existing freely generated type's constructors.
     5.5  *)
     5.6  
     5.7 -signature BNF_CTR_SUGAR_TACTICS =
     5.8 +signature CTR_SUGAR_TACTICS =
     5.9  sig
    5.10    val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    5.11    val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
    5.12 @@ -26,7 +26,7 @@
    5.13    val mk_unique_disc_def_tac: int -> thm -> tactic
    5.14  end;
    5.15  
    5.16 -structure BNF_Ctr_Sugar_Tactics : BNF_CTR_SUGAR_TACTICS =
    5.17 +structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
    5.18  struct
    5.19  
    5.20  open BNF_Util
     6.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4       nesting_bnfs: BNF_Def.bnf list,
     6.5       fp_res: BNF_FP_Util.fp_result,
     6.6       ctr_defss: thm list list,
     6.7 -     ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
     6.8 +     ctr_sugars: Ctr_Sugar.ctr_sugar list,
     6.9       co_iterss: term list list,
    6.10       mapss: thm list list,
    6.11       co_inducts: thm list,
    6.12 @@ -87,7 +87,7 @@
    6.13      string * term list * term list list * ((term list list * term list list list)
    6.14        * (typ list * typ list list)) list ->
    6.15      thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
    6.16 -    int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list ->
    6.17 +    int list list -> int list list -> int list -> thm list list -> Ctr_Sugar.ctr_sugar list ->
    6.18      term list list -> thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
    6.19    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    6.20        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    6.21 @@ -105,8 +105,8 @@
    6.22  structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
    6.23  struct
    6.24  
    6.25 +open Ctr_Sugar
    6.26  open BNF_Util
    6.27 -open BNF_Ctr_Sugar
    6.28  open BNF_Comp
    6.29  open BNF_Def
    6.30  open BNF_FP_Util
     7.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
     7.3 @@ -25,9 +25,9 @@
     7.4  structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
     7.5  struct
     7.6  
     7.7 +open Ctr_Sugar
     7.8  open BNF_Util
     7.9  open BNF_Def
    7.10 -open BNF_Ctr_Sugar
    7.11  open BNF_FP_Util
    7.12  open BNF_FP_Def_Sugar
    7.13  open BNF_FP_N2M
     8.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 12:53:24 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 14:05:25 2013 +0200
     8.3 @@ -83,9 +83,9 @@
     8.4  structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
     8.5  struct
     8.6  
     8.7 +open Ctr_Sugar
     8.8  open BNF_Util
     8.9  open BNF_Def
    8.10 -open BNF_Ctr_Sugar
    8.11  open BNF_FP_Util
    8.12  open BNF_FP_Def_Sugar
    8.13  open BNF_FP_N2M_Sugar
     9.1 --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 12:53:24 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 14:05:25 2013 +0200
     9.3 @@ -13,8 +13,8 @@
     9.4  structure BNF_LFP_Compat : BNF_LFP_COMPAT =
     9.5  struct
     9.6  
     9.7 +open Ctr_Sugar
     9.8  open BNF_Util
     9.9 -open BNF_Ctr_Sugar
    9.10  open BNF_FP_Util
    9.11  open BNF_FP_Def_Sugar
    9.12  open BNF_FP_N2M_Sugar