# HG changeset patch # User blanchet # Date 1410454476 -7200 # Node ID 117ba6cbe4140f507d8a09d1f79499f5db78a57e # Parent 57752a91eec44712ec639c4d0906528de6af9c08 renamed 'rep_datatype' to 'old_rep_datatype' (HOL) diff -r 57752a91eec4 -r 117ba6cbe414 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200 @@ -706,13 +706,13 @@ text {* \begin{matharray}{rcl} @{command_def (HOL) "old_datatype"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "rep_datatype"} & : & @{text "theory \ proof(prove)"} \\ + @{command_def (HOL) "old_rep_datatype"} & : & @{text "theory \ proof(prove)"} \\ \end{matharray} @{rail \ @@{command (HOL) old_datatype} (spec + @'and') ; - @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) + @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) ; spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|') @@ -725,7 +725,7 @@ \item @{command (HOL) "old_datatype"} defines old-style inductive datatypes in HOL. - \item @{command (HOL) "rep_datatype"} represents existing types as + \item @{command (HOL) "old_rep_datatype"} represents existing types as old-style datatypes. \end{description} diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Code_Numeral.thy Thu Sep 11 18:54:36 2014 +0200 @@ -800,7 +800,7 @@ declare Suc.rep_eq [simp] -rep_datatype "0::natural" Suc +old_rep_datatype "0::natural" Suc by (transfer, fact nat.induct nat.inject nat.distinct)+ lemma natural_cases [case_names nat, cases type: natural]: diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/HOLCF/Lift.thy --- a/src/HOL/HOLCF/Lift.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/HOLCF/Lift.thy Thu Sep 11 18:54:36 2014 +0200 @@ -29,7 +29,7 @@ apply (simp add: Def_def) done -rep_datatype "\\'a lift" Def +old_rep_datatype "\\'a lift" Def by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo) text {* @{term bottom} and @{term Def} *} diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Inductive.thy Thu Sep 11 18:54:36 2014 +0200 @@ -10,7 +10,7 @@ "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and "monos" and "print_inductives" :: diag and - "rep_datatype" :: thy_goal and + "old_rep_datatype" :: thy_goal and "primrec" :: thy_decl begin diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Library/Bit.thy Thu Sep 11 18:54:36 2014 +0200 @@ -27,7 +27,7 @@ end -rep_datatype "0::bit" "1::bit" +old_rep_datatype "0::bit" "1::bit" proof - fix P and x :: bit assume "P (0::bit)" and "P (1::bit)" diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Library/Extended_Nat.thy Thu Sep 11 18:54:36 2014 +0200 @@ -44,7 +44,7 @@ by (rule exI[of _ "to_nat \ Rep_enat"]) (simp add: inj_on_def Rep_enat_inject) qed -rep_datatype enat "\ :: enat" +old_rep_datatype enat "\ :: enat" proof - fix P i assume "\j. P (enat j)" "P \" then show "P i" diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Nat.thy Thu Sep 11 18:54:36 2014 +0200 @@ -96,10 +96,10 @@ apply (simp only: Suc_not_Zero) done --- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} +-- {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *} setup {* Sign.mandatory_path "old" *} -rep_datatype "0 \ nat" Suc +old_rep_datatype "0 \ nat" Suc apply (erule nat_induct0, assumption) apply (rule nat.inject) apply (rule nat.distinct(1)) diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Product_Type.thy Thu Sep 11 18:54:36 2014 +0200 @@ -15,11 +15,11 @@ free_constructors case_bool for True | False by auto -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *} setup {* Sign.mandatory_path "old" *} -rep_datatype True False by (auto intro: bool_induct) +old_rep_datatype True False by (auto intro: bool_induct) setup {* Sign.parent_path *} @@ -84,11 +84,11 @@ free_constructors case_unit for "()" by auto -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *} setup {* Sign.mandatory_path "old" *} -rep_datatype "()" by simp +old_rep_datatype "()" by simp setup {* Sign.parent_path *} @@ -257,11 +257,11 @@ by (simp add: Pair_def Abs_prod_inject) qed -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *} setup {* Sign.mandatory_path "old" *} -rep_datatype Pair +old_rep_datatype Pair by (erule prod_cases) (rule prod.inject) setup {* Sign.parent_path *} diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Sum_Type.thy Thu Sep 11 18:54:36 2014 +0200 @@ -90,11 +90,11 @@ | Inr projr by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *} setup {* Sign.mandatory_path "old" *} -rep_datatype Inl Inr +old_rep_datatype Inl Inr proof - fix P fix s :: "'a + 'b" diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Sep 11 18:54:36 2014 +0200 @@ -673,7 +673,8 @@ (* outer syntax *) val _ = - Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively" + Outer_Syntax.command @{command_spec "old_rep_datatype"} + "register existing types as old-style datatypes" (Scan.repeat1 Parse.term >> (fn ts => Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));