rearrange dependencies
authorblanchet
Mon Sep 03 11:54:21 2012 +0200 (2012-09-03)
changeset 49075ed769978dc8d
parent 49074 d8af889dcbe3
child 49076 d2ed455fa3d2
rearrange dependencies
src/HOL/Codatatype/BNF_Wrap.thy
src/HOL/Codatatype/Codatatype.thy
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_util.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Codatatype/BNF_Wrap.thy	Mon Sep 03 11:54:21 2012 +0200
     1.3 @@ -0,0 +1,19 @@
     1.4 +(*  Title:      HOL/Codatatype/BNF_Wrap.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Wrapping datatypes.
     1.9 +*)
    1.10 +
    1.11 +header {* Wrapping Datatypes *}
    1.12 +
    1.13 +theory BNF_Wrap
    1.14 +imports BNF_Def
    1.15 +keywords
    1.16 +  "wrap_data" :: thy_goal
    1.17 +uses
    1.18 +  "Tools/bnf_wrap_tactics.ML"
    1.19 +  "Tools/bnf_wrap.ML"
    1.20 +begin
    1.21 +
    1.22 +end
     2.1 --- a/src/HOL/Codatatype/Codatatype.thy	Mon Sep 03 11:54:21 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Codatatype.thy	Mon Sep 03 11:54:21 2012 +0200
     2.3 @@ -10,12 +10,7 @@
     2.4  header {* The (Co)datatype Package *}
     2.5  
     2.6  theory Codatatype
     2.7 -imports BNF_LFP BNF_GFP
     2.8 -keywords
     2.9 -  "wrap_data" :: thy_goal
    2.10 -usesy
    2.11 -  "Tools/bnf_wrap_tactics.ML"
    2.12 -  "Tools/bnf_wrap.ML"
    2.13 +imports BNF_Wrap BNF_LFP BNF_GFP
    2.14  begin
    2.15  
    2.16  end
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 03 11:54:21 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 03 11:54:21 2012 +0200
     3.3 @@ -75,21 +75,12 @@
     3.4    val split_conj_thm: thm -> thm list
     3.5    val split_conj_prems: int -> thm -> thm
     3.6  
     3.7 -  val list_all_free: term list -> term -> term
     3.8 -  val list_exists_free: term list -> term -> term
     3.9 -
    3.10    val mk_Field: term -> term
    3.11    val mk_union: term * term -> term
    3.12  
    3.13 -  val mk_disjIN: int -> int -> thm
    3.14 -
    3.15    val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
    3.16  
    3.17    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    3.18 -  val interleave: 'a list -> 'a list -> 'a list
    3.19 -
    3.20 -  val certifyT: Proof.context -> typ -> ctyp
    3.21 -  val certify: Proof.context -> term -> cterm
    3.22  
    3.23    val fp_bnf: (binding list -> typ list list -> BNF_Def.BNF list ->
    3.24      Proof.context -> Proof.context) ->
    3.25 @@ -190,28 +181,9 @@
    3.26  
    3.27  val mk_union = HOLogic.mk_binop @{const_name sup};
    3.28  
    3.29 -fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
    3.30 -  | mk_disjIN _ 1 = disjI1
    3.31 -  | mk_disjIN 2 2 = disjI2
    3.32 -  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
    3.33 -
    3.34  (*dangerous; use with monotonic, converging functions only!*)
    3.35  fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
    3.36  
    3.37 -val list_exists_free =
    3.38 -  fold_rev (fn free => fn P =>
    3.39 -    let val (x, T) = Term.dest_Free free;
    3.40 -    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
    3.41 -
    3.42 -val list_all_free =
    3.43 -  fold_rev (fn free => fn P =>
    3.44 -    let val (x, T) = Term.dest_Free free;
    3.45 -    in HOLogic.all_const T $ Term.absfree (x, T) P end);
    3.46 -
    3.47 -(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
    3.48 -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    3.49 -fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    3.50 -
    3.51  (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
    3.52  fun split_conj_thm th =
    3.53    ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
    3.54 @@ -225,8 +197,6 @@
    3.55  fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
    3.56    [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
    3.57  
    3.58 -fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
    3.59 -
    3.60  fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
    3.61    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
    3.62  
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 03 11:54:21 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 03 11:54:21 2012 +0200
     4.3 @@ -40,6 +40,7 @@
     4.4      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
     4.5    val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
     4.6      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
     4.7 +  val interleave: 'a list -> 'a list -> 'a list
     4.8    val transpose: 'a list list -> 'a list list
     4.9  
    4.10    val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
    4.11 @@ -87,6 +88,9 @@
    4.12    val mk_subset: term -> term -> term
    4.13    val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
    4.14  
    4.15 +  val list_all_free: term list -> term -> term
    4.16 +  val list_exists_free: term list -> term -> term
    4.17 +
    4.18    (*parameterized terms*)
    4.19    val mk_nthN: int -> term -> int -> term
    4.20  
    4.21 @@ -94,6 +98,7 @@
    4.22    val mk_Un_upper: int -> int -> thm
    4.23    val mk_conjIN: int -> thm
    4.24    val mk_conjunctN: int -> int -> thm
    4.25 +  val mk_disjIN: int -> int -> thm
    4.26    val mk_nthI: int -> int -> thm
    4.27    val mk_nth_conv: int -> int -> thm
    4.28    val mk_ordLeq_csum: int -> int -> thm -> thm
    4.29 @@ -108,6 +113,9 @@
    4.30    val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
    4.31    val find_indices: ''a list -> ''a list -> int list
    4.32  
    4.33 +  val certifyT: Proof.context -> typ -> ctyp
    4.34 +  val certify: Proof.context -> term -> cterm
    4.35 +
    4.36    val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    4.37    val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
    4.38      tactic
    4.39 @@ -223,6 +231,10 @@
    4.40      in (x :: xs, acc'') end
    4.41    | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    4.42  
    4.43 +(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
    4.44 +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    4.45 +fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    4.46 +
    4.47  (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
    4.48  fun WRAP gen_before gen_after xs core_tac =
    4.49    fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
    4.50 @@ -434,6 +446,16 @@
    4.51  
    4.52  fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
    4.53  
    4.54 +val list_all_free =
    4.55 +  fold_rev (fn free => fn P =>
    4.56 +    let val (x, T) = Term.dest_Free free;
    4.57 +    in HOLogic.all_const T $ Term.absfree (x, T) P end);
    4.58 +
    4.59 +val list_exists_free =
    4.60 +  fold_rev (fn free => fn P =>
    4.61 +    let val (x, T) = Term.dest_Free free;
    4.62 +    in HOLogic.exists_const T $ Term.absfree (x, T) P end);
    4.63 +
    4.64  fun find_indices xs ys = map_filter I
    4.65    (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
    4.66  
    4.67 @@ -471,6 +493,11 @@
    4.68  fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
    4.69    | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
    4.70  
    4.71 +fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
    4.72 +  | mk_disjIN _ 1 = disjI1
    4.73 +  | mk_disjIN 2 2 = disjI2
    4.74 +  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
    4.75 +
    4.76  fun mk_ordLeq_csum 1 1 thm = thm
    4.77    | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
    4.78    | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
    4.79 @@ -497,6 +524,8 @@
    4.80      | mk_UnN n m = mk_UnN' (n - m)
    4.81  end;
    4.82  
    4.83 +fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
    4.84 +
    4.85  fun transpose [] = []
    4.86    | transpose ([] :: xss) = transpose xss
    4.87    | transpose xss = map hd xss :: transpose (map tl xss);
     5.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 03 11:54:21 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 03 11:54:21 2012 +0200
     5.3 @@ -13,7 +13,6 @@
     5.4  struct
     5.5  
     5.6  open BNF_Util
     5.7 -open BNF_FP_Util
     5.8  open BNF_Wrap_Tactics
     5.9  
    5.10  val is_N = "is_";
    5.11 @@ -29,6 +28,9 @@
    5.12  val disc_exhaustN = "disc_exhaust";
    5.13  val discsN = "discs";
    5.14  val distinctN = "distinct";
    5.15 +val exhaustN = "exhaust";
    5.16 +val injectN = "inject";
    5.17 +val nchotomyN = "nchotomy";
    5.18  val selsN = "sels";
    5.19  val splitN = "split";
    5.20  val split_asmN = "split_asm";
     6.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Mon Sep 03 11:54:21 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Mon Sep 03 11:54:21 2012 +0200
     6.3 @@ -23,7 +23,6 @@
     6.4  
     6.5  open BNF_Util
     6.6  open BNF_Tactics
     6.7 -open BNF_FP_Util
     6.8  
     6.9  fun triangle _ [] = []
    6.10    | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss