compatibility names
authorblanchet
Wed Feb 12 08:35:56 2014 +0100 (2014-02-12)
changeset 55406186076d100d3
parent 55405 0a155051bd9d
child 55407 81f7e60755c3
compatibility names
src/HOL/List.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -14,6 +14,18 @@
     1.4  
     1.5  datatype_new_compat list
     1.6  
     1.7 +thm list.exhaust[no_vars]
     1.8 +
     1.9 +lemma [case_names Nil Cons, cases type: list]:
    1.10 +  -- {* for backward compatibility -- names of variables differ *}
    1.11 +  "(y = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>a list. y = a # list \<Longrightarrow> P) \<Longrightarrow> P"
    1.12 +by (rule list.exhaust)
    1.13 +
    1.14 +lemma [case_names Nil Cons, induct type: list]:
    1.15 +  -- {* for backward compatibility -- names of variables differ *}
    1.16 +  "P [] \<Longrightarrow> (\<And>a list. P list \<Longrightarrow> P (a # list)) \<Longrightarrow> P list"
    1.17 +by (rule list.induct)
    1.18 +
    1.19  -- {* Compatibility *}
    1.20  setup {* Sign.mandatory_path "list" *}
    1.21  
     2.1 --- a/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
     2.3 @@ -8,10 +8,22 @@
     2.4  imports BNF_LFP Datatype Finite_Set
     2.5  begin
     2.6  
     2.7 -datatype_new 'a option = =: None | Some (the: 'a)
     2.8 +datatype_new 'a option =
     2.9 +    =: None
    2.10 +  | Some (the: 'a)
    2.11  
    2.12  datatype_new_compat option
    2.13  
    2.14 +lemma [case_names None Some, cases type: option]:
    2.15 +  -- {* for backward compatibility -- names of variables differ *}
    2.16 +  "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>option. y = Some option \<Longrightarrow> P) \<Longrightarrow> P"
    2.17 +by (rule option.exhaust)
    2.18 +
    2.19 +lemma [case_names None Some, induct type: option]:
    2.20 +  -- {* for backward compatibility -- names of variables differ *}
    2.21 +  "P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
    2.22 +by (rule option.induct)
    2.23 +
    2.24  -- {* Compatibility *}
    2.25  setup {* Sign.mandatory_path "option" *}
    2.26