# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 5cb95b79a51f6bc7609bd9b23a9cd8ae9ac029a3
# Parent  677569668824f37e93f3396c1bc76e4df189da1c
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
* * *
compile
* * *
tuned imports to prevent merge issues in 'Main'

diff -r 677569668824 -r 5cb95b79a51f src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Extraction.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -5,7 +5,7 @@
 header {* Program extraction for HOL *}
 
 theory Extraction
-imports Option
+imports Datatype Option
 begin
 
 ML_file "Tools/rewrite_hol_proof.ML"
diff -r 677569668824 -r 5cb95b79a51f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Int.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -6,7 +6,7 @@
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
 
 theory Int
-imports Equiv_Relations Wellfounded Power Quotient Fun_Def
+imports Equiv_Relations Power Quotient Fun_Def
 begin
 
 subsection {* Definition of integers as a quotient type *}
diff -r 677569668824 -r 5cb95b79a51f src/HOL/Lifting_Option.thy
--- a/src/HOL/Lifting_Option.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -26,7 +26,7 @@
   unfolding option_rel_def by simp_all
 
 abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
-  "option_pred \<equiv> option_case True"
+  "option_pred \<equiv> case_option True"
 
 lemma option_rel_eq [relator_eq]:
   "option_rel (op =) = (op =)"
@@ -100,8 +100,8 @@
 lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
   unfolding fun_rel_def by simp
 
-lemma option_case_transfer [transfer_rule]:
-  "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
+lemma case_option_transfer [transfer_rule]:
+  "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
   unfolding fun_rel_def split_option_all by simp
 
 lemma option_map_transfer [transfer_rule]:
@@ -115,57 +115,4 @@
 
 end
 
-
-subsubsection {* BNF setup *}
-
-lemma option_rec_conv_option_case: "option_rec = option_case"
-by (simp add: fun_eq_iff split: option.split)
-
-bnf "'a option"
-  map: Option.map
-  sets: Option.set
-  bd: natLeq
-  wits: None
-  rel: option_rel
-proof -
-  show "Option.map id = id" by (rule Option.map.id)
-next
-  fix f g
-  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
-    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
-next
-  fix f g x
-  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
-  thus "Option.map f x = Option.map g x"
-    by (simp cong: Option.map_cong)
-next
-  fix f
-  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
-    by fastforce
-next
-  show "card_order natLeq" by (rule natLeq_card_order)
-next
-  show "cinfinite natLeq" by (rule natLeq_cinfinite)
-next
-  fix x
-  show "|Option.set x| \<le>o natLeq"
-    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
-next
-  fix R S
-  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
-    by (auto simp: option_rel_def split: option.splits)
-next
-  fix z
-  assume "z \<in> Option.set None"
-  thus False by simp
-next
-  fix R
-  show "option_rel R =
-        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
-         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
-  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
-  by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
-           split: option.splits)
-qed
-
 end
diff -r 677569668824 -r 5cb95b79a51f src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -8,10 +8,21 @@
 imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
 begin
 
-datatype 'a list =
+datatype_new 'a list =
     Nil    ("[]")
   | Cons 'a  "'a list"    (infixr "#" 65)
 
+datatype_new_compat list
+
+-- {* Compatibility *}
+setup {* Sign.mandatory_path "list" *}
+
+lemmas inducts = list.induct
+lemmas recs = list.rec
+lemmas cases = list.case
+
+setup {* Sign.parent_path *}
+
 syntax
   -- {* list Enumeration *}
   "_list" :: "args => 'a list"    ("[(_)]")
@@ -4275,12 +4286,12 @@
 by pat_completeness auto
 
 lemma transpose_aux_filter_head:
-  "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
+  "concat (map (case_list [] (\<lambda>h t. [h])) xss) =
   map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
   by (induct xss) (auto split: list.split)
 
 lemma transpose_aux_filter_tail:
-  "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
+  "concat (map (case_list [] (\<lambda>h t. [t])) xss) =
   map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
   by (induct xss) (auto split: list.split)
 
@@ -4354,13 +4365,13 @@
       by (cases x) simp_all
     } note *** = this
 
-    have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"
+    have j_less: "j < length (transpose (xs # concat (map (case_list [] (\<lambda>h t. [t])) xss)))"
       using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)
 
     show ?thesis
       unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less]
       apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
-      apply (rule_tac y=x in list.exhaust)
+      apply (rule list.exhaust)
       by auto
   qed
 qed simp_all
@@ -6672,14 +6683,14 @@
   "(A ===> list_all2 A ===> list_all2 A) Cons Cons"
   unfolding fun_rel_def by simp
 
-lemma list_case_transfer [transfer_rule]:
+lemma case_list_transfer [transfer_rule]:
   "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
-    list_case list_case"
+    case_list case_list"
   unfolding fun_rel_def by (simp split: list.split)
 
-lemma list_rec_transfer [transfer_rule]:
+lemma rec_list_transfer [transfer_rule]:
   "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
-    list_rec list_rec"
+    rec_list rec_list"
   unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
 
 lemma tl_transfer [transfer_rule]:
@@ -6876,46 +6887,4 @@
 
 end
 
-
-subsection {* BNF setup *}
-
-bnf "'a list"
-  map: map
-  sets: set
-  bd: natLeq
-  wits: Nil
-  rel: list_all2
-proof -
-  show "map id = id" by (rule List.map.id)
-next
-  fix f g
-  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
-next
-  fix x f g
-  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
-  thus "map f x = map g x" by simp
-next
-  fix f
-  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
-next
-  show "card_order natLeq" by (rule natLeq_card_order)
-next
-  show "cinfinite natLeq" by (rule natLeq_cinfinite)
-next
-  fix x
-  show "|set x| \<le>o natLeq"
-    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
-next
-  fix R S
-  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
-    by (metis list_all2_OO order_refl)
-next
-  fix R
-  show "list_all2 R =
-         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
-         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
-    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
-    by (force simp: zip_map_fst_snd)
-qed simp
-
 end
diff -r 677569668824 -r 5cb95b79a51f src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -5,10 +5,21 @@
 header {* Datatype option *}
 
 theory Option
-imports Datatype Finite_Set
+imports BNF_LFP Datatype Finite_Set
 begin
 
-datatype 'a option = None | Some 'a
+datatype_new 'a option = None | Some 'a
+
+datatype_new_compat option
+
+-- {* Compatibility *}
+setup {* Sign.mandatory_path "option" *}
+
+lemmas inducts = option.induct
+lemmas recs = option.rec
+lemmas cases = option.case
+
+setup {* Sign.parent_path *}
 
 lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
   by (induct x) auto
@@ -23,7 +34,7 @@
 lemma inj_Some [simp]: "inj_on Some A"
 by (rule inj_onI) simp
 
-lemma option_caseE:
+lemma case_optionE:
   assumes c: "(case x of None => P | Some y => Q y)"
   obtains
     (None) "x = None" and P
@@ -104,8 +115,8 @@
   qed
 qed
 
-lemma option_case_map [simp]:
-  "option_case g h (Option.map f x) = option_case g (h \<circ> f) x"
+lemma case_option_map [simp]:
+  "case_option g h (Option.map f x) = case_option g (h \<circ> f) x"
   by (cases x) simp_all
 
 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
diff -r 677569668824 -r 5cb95b79a51f src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -265,14 +265,14 @@
 
 fun add_case_cong n thy =
   let
-    val cong = #case_cong (Datatype.the_info thy n)
+    val cong = #case_cong (Datatype_Data.the_info thy n)
       |> safe_mk_meta_eq
   in
     Context.theory_map
       (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
   end
 
-val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
+val setup_case_cong = Datatype_Data.interpretation (K (fold add_case_cong))
 
 
 (* setup *)