renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
authorblanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306117ba6cbe414
parent 58305 57752a91eec4
child 58307 8172bbb37b06
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Code_Numeral.thy
src/HOL/HOLCF/Lift.thy
src/HOL/Inductive.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -706,13 +706,13 @@
     1.4  text {*
     1.5    \begin{matharray}{rcl}
     1.6      @{command_def (HOL) "old_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
     1.7 -    @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     1.8 +    @{command_def (HOL) "old_rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     1.9    \end{matharray}
    1.10  
    1.11    @{rail \<open>
    1.12      @@{command (HOL) old_datatype} (spec + @'and')
    1.13      ;
    1.14 -    @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
    1.15 +    @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
    1.16      ;
    1.17  
    1.18      spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
    1.19 @@ -725,7 +725,7 @@
    1.20    \item @{command (HOL) "old_datatype"} defines old-style inductive
    1.21    datatypes in HOL.
    1.22  
    1.23 -  \item @{command (HOL) "rep_datatype"} represents existing types as
    1.24 +  \item @{command (HOL) "old_rep_datatype"} represents existing types as
    1.25    old-style datatypes.
    1.26  
    1.27    \end{description}
     2.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 11 18:54:36 2014 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 11 18:54:36 2014 +0200
     2.3 @@ -800,7 +800,7 @@
     2.4  
     2.5  declare Suc.rep_eq [simp]
     2.6  
     2.7 -rep_datatype "0::natural" Suc
     2.8 +old_rep_datatype "0::natural" Suc
     2.9    by (transfer, fact nat.induct nat.inject nat.distinct)+
    2.10  
    2.11  lemma natural_cases [case_names nat, cases type: natural]:
     3.1 --- a/src/HOL/HOLCF/Lift.thy	Thu Sep 11 18:54:36 2014 +0200
     3.2 +++ b/src/HOL/HOLCF/Lift.thy	Thu Sep 11 18:54:36 2014 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  apply (simp add: Def_def)
     3.5  done
     3.6  
     3.7 -rep_datatype "\<bottom>\<Colon>'a lift" Def
     3.8 +old_rep_datatype "\<bottom>\<Colon>'a lift" Def
     3.9    by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
    3.10  
    3.11  text {* @{term bottom} and @{term Def} *}
     4.1 --- a/src/HOL/Inductive.thy	Thu Sep 11 18:54:36 2014 +0200
     4.2 +++ b/src/HOL/Inductive.thy	Thu Sep 11 18:54:36 2014 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
     4.5    "monos" and
     4.6    "print_inductives" :: diag and
     4.7 -  "rep_datatype" :: thy_goal and
     4.8 +  "old_rep_datatype" :: thy_goal and
     4.9    "primrec" :: thy_decl
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Library/Bit.thy	Thu Sep 11 18:54:36 2014 +0200
     5.2 +++ b/src/HOL/Library/Bit.thy	Thu Sep 11 18:54:36 2014 +0200
     5.3 @@ -27,7 +27,7 @@
     5.4  
     5.5  end
     5.6  
     5.7 -rep_datatype "0::bit" "1::bit"
     5.8 +old_rep_datatype "0::bit" "1::bit"
     5.9  proof -
    5.10    fix P and x :: bit
    5.11    assume "P (0::bit)" and "P (1::bit)"
     6.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     6.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     6.3 @@ -44,7 +44,7 @@
     6.4      by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
     6.5  qed
     6.6   
     6.7 -rep_datatype enat "\<infinity> :: enat"
     6.8 +old_rep_datatype enat "\<infinity> :: enat"
     6.9  proof -
    6.10    fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
    6.11    then show "P i"
     7.1 --- a/src/HOL/Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     7.2 +++ b/src/HOL/Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     7.3 @@ -96,10 +96,10 @@
     7.4    apply (simp only: Suc_not_Zero)
     7.5    done
     7.6  
     7.7 --- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     7.8 +-- {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
     7.9  setup {* Sign.mandatory_path "old" *}
    7.10  
    7.11 -rep_datatype "0 \<Colon> nat" Suc
    7.12 +old_rep_datatype "0 \<Colon> nat" Suc
    7.13    apply (erule nat_induct0, assumption)
    7.14   apply (rule nat.inject)
    7.15  apply (rule nat.distinct(1))
     8.1 --- a/src/HOL/Product_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     8.2 +++ b/src/HOL/Product_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     8.3 @@ -15,11 +15,11 @@
     8.4  free_constructors case_bool for True | False
     8.5    by auto
     8.6  
     8.7 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     8.8 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
     8.9  
    8.10  setup {* Sign.mandatory_path "old" *}
    8.11  
    8.12 -rep_datatype True False by (auto intro: bool_induct)
    8.13 +old_rep_datatype True False by (auto intro: bool_induct)
    8.14  
    8.15  setup {* Sign.parent_path *}
    8.16  
    8.17 @@ -84,11 +84,11 @@
    8.18  free_constructors case_unit for "()"
    8.19    by auto
    8.20  
    8.21 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    8.22 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
    8.23  
    8.24  setup {* Sign.mandatory_path "old" *}
    8.25  
    8.26 -rep_datatype "()" by simp
    8.27 +old_rep_datatype "()" by simp
    8.28  
    8.29  setup {* Sign.parent_path *}
    8.30  
    8.31 @@ -257,11 +257,11 @@
    8.32      by (simp add: Pair_def Abs_prod_inject)
    8.33  qed
    8.34  
    8.35 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    8.36 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
    8.37  
    8.38  setup {* Sign.mandatory_path "old" *}
    8.39  
    8.40 -rep_datatype Pair
    8.41 +old_rep_datatype Pair
    8.42  by (erule prod_cases) (rule prod.inject)
    8.43  
    8.44  setup {* Sign.parent_path *}
     9.1 --- a/src/HOL/Sum_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     9.2 +++ b/src/HOL/Sum_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     9.3 @@ -90,11 +90,11 @@
     9.4    | Inr projr
     9.5    by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
     9.6  
     9.7 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     9.8 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
     9.9  
    9.10  setup {* Sign.mandatory_path "old" *}
    9.11  
    9.12 -rep_datatype Inl Inr
    9.13 +old_rep_datatype Inl Inr
    9.14  proof -
    9.15    fix P
    9.16    fix s :: "'a + 'b"
    10.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Sep 11 18:54:36 2014 +0200
    10.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Sep 11 18:54:36 2014 +0200
    10.3 @@ -673,7 +673,8 @@
    10.4  (* outer syntax *)
    10.5  
    10.6  val _ =
    10.7 -  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
    10.8 +  Outer_Syntax.command @{command_spec "old_rep_datatype"}
    10.9 +    "register existing types as old-style datatypes"
   10.10      (Scan.repeat1 Parse.term >> (fn ts =>
   10.11        Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));
   10.12