--- /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
--- 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
--- 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;
--- 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);
--- 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";
--- 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