# HG changeset patch
# User blanchet
# Date 1346666061 -7200
# Node ID ed769978dc8d6cab4ef5d539de51579b8edc3ba0
# Parent  d8af889dcbe31e3bb974d28e1947f1e2ddca21f3
rearrange dependencies

diff -r d8af889dcbe3 -r ed769978dc8d src/HOL/Codatatype/BNF_Wrap.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/BNF_Wrap.thy	Mon Sep 03 11:54:21 2012 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOL/Codatatype/BNF_Wrap.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Copyright   2012
+
+Wrapping datatypes.
+*)
+
+header {* Wrapping Datatypes *}
+
+theory BNF_Wrap
+imports BNF_Def
+keywords
+  "wrap_data" :: thy_goal
+uses
+  "Tools/bnf_wrap_tactics.ML"
+  "Tools/bnf_wrap.ML"
+begin
+
+end
diff -r d8af889dcbe3 -r ed769978dc8d src/HOL/Codatatype/Codatatype.thy
--- a/src/HOL/Codatatype/Codatatype.thy	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy	Mon Sep 03 11:54:21 2012 +0200
@@ -10,12 +10,7 @@
 header {* The (Co)datatype Package *}
 
 theory Codatatype
-imports BNF_LFP BNF_GFP
-keywords
-  "wrap_data" :: thy_goal
-usesy
-  "Tools/bnf_wrap_tactics.ML"
-  "Tools/bnf_wrap.ML"
+imports BNF_Wrap BNF_LFP BNF_GFP
 begin
 
 end
diff -r d8af889dcbe3 -r ed769978dc8d src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 03 11:54:21 2012 +0200
@@ -75,21 +75,12 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
-  val list_all_free: term list -> term -> term
-  val list_exists_free: term list -> term -> term
-
   val mk_Field: term -> term
   val mk_union: term * term -> term
 
-  val mk_disjIN: int -> int -> thm
-
   val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
-  val interleave: 'a list -> 'a list -> 'a list
-
-  val certifyT: Proof.context -> typ -> ctyp
-  val certify: Proof.context -> term -> cterm
 
   val fp_bnf: (binding list -> typ list list -> BNF_Def.BNF list ->
     Proof.context -> Proof.context) ->
@@ -190,28 +181,9 @@
 
 val mk_union = HOLogic.mk_binop @{const_name sup};
 
-fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
-  | mk_disjIN _ 1 = disjI1
-  | mk_disjIN 2 2 = disjI2
-  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
-
 (*dangerous; use with monotonic, converging functions only!*)
 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
 
-val list_exists_free =
-  fold_rev (fn free => fn P =>
-    let val (x, T) = Term.dest_Free free;
-    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
-
-val list_all_free =
-  fold_rev (fn free => fn P =>
-    let val (x, T) = Term.dest_Free free;
-    in HOLogic.all_const T $ Term.absfree (x, T) P end);
-
-(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
-fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
-fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
-
 (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
 fun split_conj_thm th =
   ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
@@ -225,8 +197,6 @@
 fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
 
-fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
-
 fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
   (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
 
diff -r d8af889dcbe3 -r ed769978dc8d src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 03 11:54:21 2012 +0200
@@ -40,6 +40,7 @@
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
   val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
+  val interleave: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
 
   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
@@ -87,6 +88,9 @@
   val mk_subset: term -> term -> term
   val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
 
+  val list_all_free: term list -> term -> term
+  val list_exists_free: term list -> term -> term
+
   (*parameterized terms*)
   val mk_nthN: int -> term -> int -> term
 
@@ -94,6 +98,7 @@
   val mk_Un_upper: int -> int -> thm
   val mk_conjIN: int -> thm
   val mk_conjunctN: int -> int -> thm
+  val mk_disjIN: int -> int -> thm
   val mk_nthI: int -> int -> thm
   val mk_nth_conv: int -> int -> thm
   val mk_ordLeq_csum: int -> int -> thm -> thm
@@ -108,6 +113,9 @@
   val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
   val find_indices: ''a list -> ''a list -> int list
 
+  val certifyT: Proof.context -> typ -> ctyp
+  val certify: Proof.context -> term -> cterm
+
   val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
   val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
     tactic
@@ -223,6 +231,10 @@
     in (x :: xs, acc'') end
   | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
+(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
+fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
+fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
+
 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
 fun WRAP gen_before gen_after xs core_tac =
   fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
@@ -434,6 +446,16 @@
 
 fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
 
+val list_all_free =
+  fold_rev (fn free => fn P =>
+    let val (x, T) = Term.dest_Free free;
+    in HOLogic.all_const T $ Term.absfree (x, T) P end);
+
+val list_exists_free =
+  fold_rev (fn free => fn P =>
+    let val (x, T) = Term.dest_Free free;
+    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
+
 fun find_indices xs ys = map_filter I
   (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
 
@@ -471,6 +493,11 @@
 fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
   | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
 
+fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
+  | mk_disjIN _ 1 = disjI1
+  | mk_disjIN 2 2 = disjI2
+  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
+
 fun mk_ordLeq_csum 1 1 thm = thm
   | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
   | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
@@ -497,6 +524,8 @@
     | mk_UnN n m = mk_UnN' (n - m)
 end;
 
+fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
+
 fun transpose [] = []
   | transpose ([] :: xss) = transpose xss
   | transpose xss = map hd xss :: transpose (map tl xss);
diff -r d8af889dcbe3 -r ed769978dc8d src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 03 11:54:21 2012 +0200
@@ -13,7 +13,6 @@
 struct
 
 open BNF_Util
-open BNF_FP_Util
 open BNF_Wrap_Tactics
 
 val is_N = "is_";
@@ -29,6 +28,9 @@
 val disc_exhaustN = "disc_exhaust";
 val discsN = "discs";
 val distinctN = "distinct";
+val exhaustN = "exhaust";
+val injectN = "inject";
+val nchotomyN = "nchotomy";
 val selsN = "sels";
 val splitN = "split";
 val split_asmN = "split_asm";
diff -r d8af889dcbe3 -r ed769978dc8d src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Mon Sep 03 11:54:21 2012 +0200
@@ -23,7 +23,6 @@
 
 open BNF_Util
 open BNF_Tactics
-open BNF_FP_Util
 
 fun triangle _ [] = []
   | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss