# HG changeset patch # User blanchet # Date 1348101769 -7200 # Node ID 83ac281bcdc27552dac73ffadb6e96979027c3c2 # Parent 9ef072c757ca563e58e07d3ebafadbbdabebd014 provide predicator, define relator diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/BNF_Comp.thy --- a/src/HOL/Codatatype/BNF_Comp.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Comp.thy Thu Sep 20 02:42:49 2012 +0200 @@ -82,6 +82,9 @@ lemma pred_def_abs: "rel = Collect (split pred) \ pred = (\x y. (x, y) \ rel)" by auto +lemma mem_Id_eq_eq: "(\x y. (x, y) \ Id) = (op =)" +by simp + ML_file "Tools/bnf_comp_tactics.ML" ML_file "Tools/bnf_comp.ML" diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/BNF_Util.thy --- a/src/HOL/Codatatype/BNF_Util.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Util.thy Thu Sep 20 02:42:49 2012 +0200 @@ -18,11 +18,8 @@ lemma subset_CollectI: "B \ A \ (\x. x \ B \ Q x \ P x) \ ({x \ B. Q x} \ {x \ A. P x})" by blast -lemma mem_Collect_eq_split: "{(x, y). (x, y) \ X} = X" -by simp - definition collect where - "collect F x = (\f \ F. f x)" +"collect F x = (\f \ F. f x)" (* Weak pullbacks: *) definition wpull where @@ -50,6 +47,16 @@ lemma bijI: "\\x y. (f x = f y) = (x = y); \y. \x. y = f x\ \ bij f" unfolding bij_def inj_on_def by auto blast +lemma pair_mem_Collect_split: +"(\x y. (x, y) \ {(x, y). P x y}) = P" +by simp + +lemma Collect_pair_mem_eq: "{(x, y). (x, y) \ R} = R" +by simp + +lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \ A} = A" +by simp + (* Operator: *) definition "Gr A f = {(a, f a) | a. a \ A}" diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Basic_BNFs.thy --- a/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:49 2012 +0200 @@ -25,7 +25,7 @@ unfolding cinfinite_def Field_natLeq by (rule nat_infinite) bnf_def ID: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] - "id :: ('a \ 'b) set \ ('a \ 'b) set" + "\x :: 'a \ 'b \ bool. x" apply auto apply (rule natLeq_card_order) apply (rule natLeq_cinfinite) @@ -51,10 +51,8 @@ apply (auto simp: Gr_def fun_eq_iff) done -definition DEADID_rel :: "('a \ 'a) set" where -"DEADID_rel = {p. \x. p = (x, x)}" - -bnf_def DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] DEADID_rel +bnf_def DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] + "op =::'a \ 'a \ bool" apply (auto simp add: wpull_id) apply (rule card_order_csum) apply (rule natLeq_card_order) @@ -71,7 +69,7 @@ apply (rule card_of_Card_order) apply (rule ctwo_Cnotzero) apply (rule card_of_Card_order) -apply (auto simp: DEADID_rel_def Id_def Gr_def fun_eq_iff) +apply (auto simp: Id_def Gr_def fun_eq_iff) done definition setl :: "'a + 'b \ 'a set" where @@ -82,13 +80,12 @@ lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] -definition sum_rel :: "('a \ 'b) set \ ('c \ 'd) set \ (('a + 'c) \ ('b + 'd)) set" where -"sum_rel R S = - {x. case x of (Inl a, Inl c) \ (a, c) \ R - | (Inr b, Inr d) \ (b, d) \ S - | _ \ False}" +definition sum_pred :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a + 'c \ 'b + 'd \ bool" where +"sum_pred \ \ x y = + (case x of Inl a1 \ (case y of Inl a2 \ \ a1 a2 | Inr _ \ False) + | Inr b1 \ (case y of Inl _ \ False | Inr b2 \ \ b1 b2))" -bnf_def sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] sum_rel +bnf_def sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] sum_pred proof - show "sum_map id id = id" by (rule sum_map.id) next @@ -199,10 +196,10 @@ qed next fix R S - show "sum_rel R S = - (Gr {x. setl x \ R \ setr x \ S} (sum_map fst fst))\ O - Gr {x. setl x \ R \ setr x \ S} (sum_map snd snd)" - unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold + show "{p. sum_pred (\x y. (x, y) \ R) (\x y. (x, y) \ S) (fst p) (snd p)} = + (Gr {x. setl x \ R \ setr x \ S} (sum_map fst fst))\ O + Gr {x. setl x \ R \ setr x \ S} (sum_map snd snd)" + unfolding setl_def setr_def sum_pred_def Gr_def relcomp_unfold converse_unfold by (fastforce split: sum.splits) qed (auto simp: sum_set_defs) @@ -224,10 +221,10 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] -definition prod_rel :: "('a \ 'b) set \ ('c \ 'd) set \ (('a \ 'c) \ 'b \ 'd) set" where -"prod_rel R S = {((a, c), b, d) | a b c d. (a, b) \ R \ (c, d) \ S}" +definition prod_pred :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" where +"prod_pred \ \ p1 p2 = (case p1 of (a1, b1) \ case p2 of (a2, b2) \ \ a1 a2 \ \ b1 b2)" -bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] prod_rel +bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] prod_pred proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) next @@ -304,10 +301,10 @@ unfolding wpull_def by simp fast next fix R S - show "prod_rel R S = - (Gr {x. {fst x} \ R \ {snd x} \ S} (map_pair fst fst))\ O - Gr {x. {fst x} \ R \ {snd x} \ S} (map_pair snd snd)" - unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold + show "{p. prod_pred (\x y. (x, y) \ R) (\x y. (x, y) \ S) (fst p) (snd p)} = + (Gr {x. {fst x} \ R \ {snd x} \ S} (map_pair fst fst))\ O + Gr {x. {fst x} \ R \ {snd x} \ S} (map_pair snd snd)" + unfolding prod_set_defs prod_pred_def Gr_def relcomp_unfold converse_unfold by auto qed simp+ @@ -347,11 +344,11 @@ ultimately show ?thesis using card_of_ordLeq by fast qed -definition fun_rel :: "('a \ 'b) set \ (('c \ 'a) \ ('c \ 'b)) set" where -"fun_rel R = {(f, g) | f g. \x. (f x, g x) \ R}" +definition fun_pred :: "('a \ 'b \ bool) \ ('c \ 'a) \ ('c \ 'b) \ bool" where +"fun_pred \ f g = (\x. \ (f x) (g x))" bnf_def "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] - fun_rel + fun_pred proof fix f show "id \ f = id f" by simp next @@ -410,8 +407,10 @@ using wpull_cat[OF p c r] by simp metis qed next - fix R show "fun_rel R = (Gr {x. range x \ R} (op \ fst))\ O Gr {x. range x \ R} (op \ snd)" - unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold + fix R + show "{p. fun_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + (Gr {x. range x \ R} (op \ fst))\ O Gr {x. range x \ R} (op \ snd)" + unfolding fun_pred_def Gr_def relcomp_unfold converse_unfold by (auto intro!: exI dest!: in_mono) qed auto diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/HFset.thy --- a/src/HOL/Codatatype/Examples/HFset.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/HFset.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/HFset.thy +(* Title: HOL/Codatatype/Examples/HFset.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Gram_Lang.thy +(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,3 +1,12 @@ +(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy + Author: Andrei Popescu, TU Muenchen + Copyright 2012 + +Parallel composition. +*) + +header {* Parallel Composition *} + theory Parallel imports Tree begin diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,10 +1,11 @@ -(* Title: Gram_Tree.thy +(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 -Preliminaries +Preliminaries. *) +header {* Preliminaries *} theory Prelim imports "../../Codatatype/Codatatype" diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,18 +1,18 @@ -(* Title: Gram_Tree.thy +(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 Trees with nonterminal internal nodes and terminal leafs. *) - header {* Trees with nonterminal internal nodes and terminal leafs *} - theory Tree imports Prelim begin +hide_fact (open) Quotient_Product.prod_pred_def + typedecl N typedecl T codata_raw Tree: 'Tree = "N \ (T + 'Tree) fset" @@ -41,7 +41,7 @@ (\ tr2. Inr tr2 \ fset as2 \ (\ tr1. Inr tr1 \ fset as1 \ \ tr1 tr2))" lemma pre_Tree_pred: "pre_Tree_pred \ (n1,as1) (n2,as2) \ n1 = n2 \ llift2 \ as1 as2" -unfolding llift2_def pre_Tree.pred_unfold +unfolding llift2_def pre_Tree_pred_def sum_pred_def[abs_def] prod_pred_def fset_pred_def split_conv apply (auto split: sum.splits) apply (metis sumE) apply (metis sumE) diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/Lambda_Term.thy +(* Title: HOL/Codatatype/Examples/Lambda_Term.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/ListF.thy +(* Title: HOL/Codatatype/Examples/ListF.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Misc_Codata.thy --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/Misc_Data.thy +(* Title: HOL/Codatatype/Examples/Misc_Data.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Misc_Data.thy --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/Misc_Data.thy +(* Title: HOL/Codatatype/Examples/Misc_Data.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 @@ -9,13 +9,9 @@ header {* Miscellaneous Datatype Declarations *} theory Misc_Data -imports (* "../Codatatype" *) "../BNF_LFP" +imports "../Codatatype" begin -bnf_def ID2: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] - "id :: ('a \ 'b) set \ ('a \ 'b) set" -sorry - data simple = X1 | X2 | X3 | X4 data simple' = X1' unit | X2' unit | X3' unit | X4' unit diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/Process.thy +(* Title: HOL/Codatatype/Examples/Process.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 @@ -11,6 +11,8 @@ imports "../Codatatype" begin +hide_fact (open) Quotient_Product.prod_pred_def + codata 'a process = isAction: Action (prefOf: 'a) (contOf: "'a process") | isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process") @@ -21,7 +23,10 @@ subsection {* Basic properties *} -declare pre_process.pred_unfold[simp] +declare + pre_process_pred_def[simp] + sum_pred_def[simp] + prod_pred_def[simp] (* Constructors versus discriminators *) theorem isAction_isChoice: diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/Stream.thy +(* Title: HOL/Codatatype/Examples/Stream.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 @@ -12,6 +12,9 @@ imports TreeFI begin +hide_const (open) Quotient_Product.prod_pred +hide_fact (open) Quotient_Product.prod_pred_def + codata_raw stream: 's = "'a \ 's" (* selectors for streams *) @@ -115,10 +118,10 @@ unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def] map_pair_def o_def prod_case_beta by simp -lemma pre_stream_pred[simp]: "pre_stream_pred \1 \2 a b = (\1 (fst a) (fst b) \ \2 (snd a) (snd b))" -by (auto simp: pre_stream.pred_unfold) +lemma prod_pred[simp]: "prod_pred \1 \2 a b = (\1 (fst a) (fst b) \ \2 (snd a) (snd b))" +unfolding prod_pred_def by auto -lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded pre_stream_pred[abs_def], +lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded prod_pred[abs_def], folded hdd_def tll_def] definition plus :: "nat stream \ nat stream \ nat stream" (infixr "\" 66) where @@ -133,27 +136,22 @@ definition ns :: "nat \ nat stream" where [simp]: "ns n = scalar n ones" lemma "ones \ ones = twos" -by (intro stream_coind[where P="%x1 x2. \x. x1 = ones \ ones \ x2 = twos"]) - auto +by (intro stream_coind[where P="%x1 x2. \x. x1 = ones \ ones \ x2 = twos"]) auto lemma "n \ twos = ns (2 * n)" -by (intro stream_coind[where P="%x1 x2. \n. x1 = n \ twos \ x2 = ns (2 * n)"]) - force+ +by (intro stream_coind[where P="%x1 x2. \n. x1 = n \ twos \ x2 = ns (2 * n)"]) force+ lemma prod_scalar: "(n * m) \ xs = n \ m \ xs" -by (intro stream_coind[where P="%x1 x2. \n m xs. x1 = (n * m) \ xs \ x2 = n \ m \ xs"]) - force+ +by (intro stream_coind[where P="%x1 x2. \n m xs. x1 = (n * m) \ xs \ x2 = n \ m \ xs"]) force+ lemma scalar_plus: "n \ (xs \ ys) = n \ xs \ n \ ys" by (intro stream_coind[where P="%x1 x2. \n xs ys. x1 = n \ (xs \ ys) \ x2 = n \ xs \ n \ ys"]) (force simp: add_mult_distrib2)+ lemma plus_comm: "xs \ ys = ys \ xs" -by (intro stream_coind[where P="%x1 x2. \xs ys. x1 = xs \ ys \ x2 = ys \ xs"]) - force+ +by (intro stream_coind[where P="%x1 x2. \xs ys. x1 = xs \ ys \ x2 = ys \ xs"]) force+ lemma plus_assoc: "(xs \ ys) \ zs = xs \ ys \ zs" -by (intro stream_coind[where P="%x1 x2. \xs ys zs. x1 = (xs \ ys) \ zs \ x2 = xs \ ys \ zs"]) - force+ +by (intro stream_coind[where P="%x1 x2. \xs ys zs. x1 = (xs \ ys) \ zs \ x2 = xs \ ys \ zs"]) force+ end diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/TreeFI.thy +(* Title: HOL/Codatatype/Examples/TreeFI.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Thu Sep 20 02:42:49 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: Codatatype_Examples/TreeFsetI.thy +(* Title: HOL/Codatatype/Examples/TreeFsetI.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 @@ -13,6 +13,7 @@ begin hide_const (open) Sublist.sub +hide_fact (open) Quotient_Product.prod_pred_def definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" @@ -46,7 +47,7 @@ (\t \ fset (snd b). (\u \ fset (snd a). R2 u t)))" apply (cases a) apply (cases b) -apply (simp add: pre_treeFsetI.pred_unfold) +apply (simp add: pre_treeFsetI_pred_def prod_pred_def fset_pred_def) done lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct] diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/More_BNFs.thy --- a/src/HOL/Codatatype/More_BNFs.thy Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/More_BNFs.thy Thu Sep 20 02:42:49 2012 +0200 @@ -22,10 +22,14 @@ lemma option_rec_conv_option_case: "option_rec = option_case" by (simp add: fun_eq_iff split: option.split) -definition option_rel :: "('a \ 'b) set \ ('a option \ 'b option) set" where -"option_rel R = {x. case x of (None, None) \ True | (Some a, Some b) \ (a, b) \ R | _ \ False}" +definition option_pred :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" where +"option_pred R x_opt y_opt = + (case (x_opt, y_opt) of + (None, None) \ True + | (Some x, Some y) \ R x y + | _ \ False)" -bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] option_rel +bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] option_pred proof - show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) next @@ -86,9 +90,9 @@ thus False by simp next fix R - show "option_rel R = + show "{p. option_pred (\x y. (x, y) \ R) (fst p) (snd p)} = (Gr {x. Option.set x \ R} (Option.map fst))\ O Gr {x. Option.set x \ R} (Option.map snd)" - unfolding option_rel_def Gr_def relcomp_unfold converse_unfold + unfolding option_pred_def Gr_def relcomp_unfold converse_unfold by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] split: option.splits) blast qed @@ -356,35 +360,36 @@ lemma fset_to_fset: "finite A \ fset (the_inv fset A) = A" by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset) -lemma fset_pred: -"(a, b) \ (Gr {a. fset a \ {(a, b). R a b}} (map_fset fst))\ O - Gr {a. fset a \ {(a, b). R a b}} (map_fset snd) \ - ((\t \ fset a. \u \ fset b. R t u) \ (\u \ fset b. \t \ fset a. R t u))" (is "?L = ?R") +definition fset_pred :: "('a \ 'b \ bool) \ 'a fset \ 'b fset \ bool" where +"fset_pred R a b \ + (\t \ fset a. \u \ fset b. R t u) \ + (\t \ fset b. \u \ fset a. R u t)" + +lemma fset_pred_aux: +"(\t \ fset a. \u \ fset b. R t u) \ (\u \ fset b. \t \ fset a. R t u) \ + (a, b) \ (Gr {a. fset a \ {(a, b). R a b}} (map_fset fst))\ O + Gr {a. fset a \ {(a, b). R a b}} (map_fset snd)" (is "?L = ?R") proof - assume ?L thus ?R unfolding Gr_def relcomp_unfold converse_unfold + assume ?L + def R' \ "the_inv fset (Collect (split R) \ (fset a \ fset b))" (is "the_inv fset ?L'") + have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto + hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset) + show ?R unfolding Gr_def relcomp_unfold converse_unfold + proof (intro CollectI prod_caseI exI conjI) + from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?L`] + by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) + from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?L`] + by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) + qed (auto simp add: *) +next + assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold apply (simp add: subset_eq Ball_def) apply (rule conjI) apply (clarsimp, metis snd_conv) by (clarsimp, metis fst_conv) -next - assume ?R - def R' \ "the_inv fset (Collect (split R) \ (fset a \ fset b))" (is "the_inv fset ?R'") - have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto - hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset) - show ?L unfolding Gr_def relcomp_unfold converse_unfold - proof (intro CollectI prod_caseI exI conjI) - from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`] - by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) - from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`] - by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) - qed (auto simp add: *) qed -definition fset_rel :: "('a \ 'b) set \ ('a fset \ 'b fset) set" where -"fset_rel R = {(a, b) | a b. (\t \ fset a. \u \ fset b. (t, u) \ R) \ - (\u \ fset b. \t \ fset a. (t, u) \ R)}" - -bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] fset_rel +bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] fset_pred proof - show "map_fset id = id" unfolding map_fset_def2 map_id o_id afset_rfset_id .. @@ -460,11 +465,9 @@ qed next fix R - let ?pred = "\Q x y. (x, y) \ (Gr {x. fset x \ {(x, y). Q x y}} (map_fset fst))\ O Gr {x. fset x \ {(x, y). Q x y}} (map_fset snd)" - have rel_as_pred: "fset_rel R = {(a, b) | a b. ?pred (\t u. (t, u) \ R) a b}" - unfolding fset_rel_def fset_pred by (rule refl) - show "fset_rel R = (Gr {x. fset x \ R} (map_fset fst))\ O Gr {x. fset x \ R} (map_fset snd)" - unfolding rel_as_pred by simp + show "{p. fset_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + (Gr {x. fset x \ R} (map_fset fst))\ O Gr {x. fset x \ R} (map_fset snd)" + unfolding fset_pred_def fset_pred_aux by simp qed auto (* Countable sets *) @@ -534,41 +537,42 @@ lemma rcset_natural': "rcset (cIm f x) = f ` rcset x" unfolding cIm_def[abs_def] by simp -lemma cset_pred: -"(a, b) \ (Gr {x. rcset x \ {(a, b). R a b}} (cIm fst))\ O - Gr {x. rcset x \ {(a, b). R a b}} (cIm snd) \ - ((\t \ rcset a. \u \ rcset b. R t u) \ (\t \ rcset b. \u \ rcset a. R u t))" (is "?L = ?R") +definition cset_pred :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" where +"cset_pred R a b \ + (\t \ rcset a. \u \ rcset b. R t u) \ + (\t \ rcset b. \u \ rcset a. R u t)" + +lemma cset_pred_aux: +"(\t \ rcset a. \u \ rcset b. R t u) \ (\t \ rcset b. \u \ rcset a. R u t) \ + (a, b) \ (Gr {x. rcset x \ {(a, b). R a b}} (cIm fst))\ O + Gr {x. rcset x \ {(a, b). R a b}} (cIm snd)" (is "?L = ?R") proof - assume ?L thus ?R unfolding Gr_def relcomp_unfold converse_unfold + assume ?L + def R' \ "the_inv rcset (Collect (split R) \ (rcset a \ rcset b))" + (is "the_inv rcset ?L'") + have "countable ?L'" by auto + hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset) + show ?R unfolding Gr_def relcomp_unfold converse_unfold + proof (intro CollectI prod_caseI exI conjI) + have "rcset a = fst ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?A") + using conjunct1[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times) + hence "a = acset ?A" by (metis acset_rcset) + thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto + have "rcset b = snd ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?B") + using conjunct2[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times) + hence "b = acset ?B" by (metis acset_rcset) + thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto + qed (auto simp add: *) +next + assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold apply (simp add: subset_eq Ball_def) apply (rule conjI) apply (clarsimp, metis (lifting, no_types) rcset_natural' image_iff surjective_pairing) apply (clarsimp) by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range) -next - assume ?R - def R' \ "the_inv rcset (Collect (split R) \ (rcset a \ rcset b))" - (is "the_inv rcset ?R'") - have "countable ?R'" by auto - hence *: "rcset R' = ?R'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset) - show ?L unfolding Gr_def relcomp_unfold converse_unfold - proof (intro CollectI prod_caseI exI conjI) - have "rcset a = fst ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?A") - using conjunct1[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times) - hence "a = acset ?A" by (metis acset_rcset) - thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto - have "rcset b = snd ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?B") - using conjunct2[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times) - hence "b = acset ?B" by (metis acset_rcset) - thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto - qed (auto simp add: *) qed -definition cset_rel :: "('a \ 'b) set \ ('a cset \ 'b cset) set" where -"cset_rel R = {(a, b) | a b. (\t \ rcset a. \u \ rcset b. (t, u) \ R) \ - (\u \ rcset b. \t \ rcset a. (t, u) \ R)}" - -bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_rel +bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_pred proof - show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto next @@ -632,11 +636,9 @@ qed next fix R - let ?pred = "\Q x y. (x, y) \ (Gr {x. rcset x \ {(x, y). Q x y}} (cIm fst))\ O Gr {x. rcset x \ {(x, y). Q x y}} (cIm snd)" - have rel_as_pred: "cset_rel R = {(a, b) | a b. ?pred (\t u. (t, u) \ R) a b}" - unfolding cset_rel_def cset_pred by (rule refl) - show "cset_rel R = (Gr {x. rcset x \ R} (cIm fst))\ O Gr {x. rcset x \ R} (cIm snd)" - unfolding rel_as_pred by simp + show "{p. cset_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + (Gr {x. rcset x \ R} (cIm fst))\ O Gr {x. rcset x \ R} (cIm snd)" + unfolding cset_pred_def cset_pred_aux by simp qed (unfold cEmp_def, auto) @@ -1302,27 +1304,27 @@ declare multiset.count_inverse[simp] declare union_preserves_multiset[simp] -lemma mmap_Plus[simp]: +lemma mmap_Plus[simp]: assumes "K \ multiset" and "L \ multiset" shows "mmap f (\a. K a + L a) a = mmap f K a + mmap f L a" proof- - have "{aa. f aa = a \ (0 < K aa \ 0 < L aa)} \ + have "{aa. f aa = a \ (0 < K aa \ 0 < L aa)} \ {aa. 0 < K aa} \ {aa. 0 < L aa}" (is "?C \ ?A \ ?B") by auto - moreover have "finite (?A \ ?B)" apply(rule finite_UnI) + moreover have "finite (?A \ ?B)" apply(rule finite_UnI) using assms unfolding multiset_def by auto ultimately have C: "finite ?C" using finite_subset by blast have "setsum K {aa. f aa = a \ 0 < K aa} = setsum K {aa. f aa = a \ 0 < K aa + L aa}" apply(rule setsum_mono_zero_cong_left) using C by auto - moreover + moreover have "setsum L {aa. f aa = a \ 0 < L aa} = setsum L {aa. f aa = a \ 0 < K aa + L aa}" apply(rule setsum_mono_zero_cong_left) using C by auto ultimately show ?thesis unfolding mmap_def unfolding comm_monoid_add_class.setsum.F_fun_f by auto qed -lemma multiset_map_Plus[simp]: +lemma multiset_map_Plus[simp]: "multiset_map f (M1 + M2) = multiset_map f M1 + multiset_map f M2" -unfolding multiset_map_def +unfolding multiset_map_def apply(subst multiset.count_inject[symmetric]) unfolding plus_multiset.rep_eq comp_def by auto @@ -1335,23 +1337,23 @@ by (simp, simp add: single_def) qed -lemma multiset_pred_Plus: +lemma multiset_pred_Plus: assumes ab: "R a b" and MN: "multiset_pred R M N" shows "multiset_pred R (M + {#a#}) (N + {#b#})" proof- {fix y assume "R a b" and "set_of y \ {(x, y). R x y}" - hence "\ya. multiset_map fst y + {#a#} = multiset_map fst ya \ - multiset_map snd y + {#b#} = multiset_map snd ya \ + hence "\ya. multiset_map fst y + {#a#} = multiset_map fst ya \ + multiset_map snd y + {#b#} = multiset_map snd ya \ set_of ya \ {(x, y). R x y}" apply(intro exI[of _ "y + {#(a,b)#}"]) by auto } thus ?thesis - using assms + using assms unfolding multiset_pred_def Gr_def relcomp_unfold by force qed -lemma multiset_pred'_imp_multiset_pred: -"multiset_pred' R M N \ multiset_pred R M N" +lemma multiset_pred'_imp_multiset_pred: +"multiset_pred' R M N \ multiset_pred R M N" apply(induct rule: multiset_pred'.induct) using multiset_pred_Zero multiset_pred_Plus by auto @@ -1364,14 +1366,14 @@ using finite_Collect_mem . ultimately have fin: "finite {b. \a. f a = b \ a \# M}" by(rule finite_subset) have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp - by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54) + by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54) setsum_gt_0_iff setsum_infinite) have 0: "\ b. 0 < setsum (count M) (A b) \ (\ a \ A b. count M a > 0)" apply safe apply (metis less_not_refl setsum_gt_0_iff setsum_infinite) by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff) hence AB: "A ` ?B = {A b | b. \ a \ A b. count M a > 0}" by auto - + have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B" unfolding comp_def .. also have "... = (\x\ A ` ?B. setsum (count M) x)" @@ -1383,7 +1385,7 @@ also have "?J = {a. a \# M}" unfolding AB unfolding A_def by auto finally have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (count M) {a. a \# M}" . - thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def) + thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def) qed lemma multiset_pred_mcard: @@ -1412,7 +1414,7 @@ case True hence "N = {#}" using less.prems by auto thus ?thesis using True empty by auto next - case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) + case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) have "N \ {#}" using False less.prems by auto then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split) have "mcard M1 = mcard N1" using less.prems unfolding M N by auto @@ -1420,7 +1422,7 @@ qed qed -lemma msed_map_invL: +lemma msed_map_invL: assumes "multiset_map f (M + {#a#}) = N" shows "\ N1. N = N1 + {#f a#} \ multiset_map f M = N1" proof- @@ -1431,19 +1433,19 @@ thus ?thesis using N by blast qed -lemma msed_map_invR: +lemma msed_map_invR: assumes "multiset_map f M = N + {#b#}" shows "\ M1 a. M = M1 + {#a#} \ f a = b \ multiset_map f M1 = N" proof- obtain a where a: "a \# M" and fa: "f a = b" using multiset.set_natural'[of f M] unfolding assms - by (metis image_iff mem_set_of_iff union_single_eq_member) + by (metis image_iff mem_set_of_iff union_single_eq_member) then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis have "multiset_map f M1 = N" using assms unfolding M fa[symmetric] by simp thus ?thesis using M fa by blast qed -lemma msed_pred_invL: +lemma msed_pred_invL: assumes "multiset_pred R (M + {#a#}) N" shows "\ N1 b. N = N1 + {#b#} \ R a b \ multiset_pred R M N1" proof- @@ -1451,7 +1453,7 @@ and KN: "multiset_map snd K = N" and sK: "set_of K \ {(a, b). R a b}" using assms unfolding multiset_pred_def Gr_def relcomp_unfold by auto - obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a" + obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a" and K1M: "multiset_map fst K1 = M" using msed_map_invR[OF KM] by auto obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "multiset_map snd K1 = N1" using msed_map_invL[OF KN[unfolded K]] by auto @@ -1461,29 +1463,29 @@ thus ?thesis using N Rab by auto qed -lemma msed_pred_invR: +lemma msed_pred_invR: assumes "multiset_pred R M (N + {#b#})" shows "\ M1 a. M = M1 + {#a#} \ R a b \ multiset_pred R M1 N" proof- obtain K where KN: "multiset_map snd K = N + {#b#}" and KM: "multiset_map fst K = M" and sK: "set_of K \ {(a, b). R a b}" using assms - unfolding multiset_pred_def Gr_def relcomp_unfold by auto - obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" + unfolding multiset_pred_def Gr_def relcomp_unfold by auto + obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" and K1N: "multiset_map snd K1 = N" using msed_map_invR[OF KN] by auto obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "multiset_map fst K1 = M1" using msed_map_invL[OF KM[unfolded K]] by auto have Rab: "R (fst ab) b" using sK b unfolding K by auto - have "multiset_pred R M1 N" using sK K1N K1M1 + have "multiset_pred R M1 N" using sK K1N K1M1 unfolding K multiset_pred_def Gr_def relcomp_unfold by auto thus ?thesis using M Rab by auto qed -lemma multiset_pred_imp_multiset_pred': +lemma multiset_pred_imp_multiset_pred': assumes "multiset_pred R M N" shows "multiset_pred' R M N" using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) - case (less M) + case (less M) have c: "mcard M = mcard N" using multiset_pred_mcard[OF less.prems] . show ?case proof(cases "M = {#}") @@ -1498,12 +1500,12 @@ qed qed -lemma multiset_pred_multiset_pred': +lemma multiset_pred_multiset_pred': "multiset_pred R M N = multiset_pred' R M N" using multiset_pred_imp_multiset_pred' multiset_pred'_imp_multiset_pred by auto (* The main end product for multiset_pred: inductive characterization *) -theorems multiset_pred_induct[case_names empty add, induct pred: multiset_pred] = +theorems multiset_pred_induct[case_names empty add, induct pred: multiset_pred] = multiset_pred'.induct[unfolded multiset_pred_multiset_pred'[symmetric]] end diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:49 2012 +0200 @@ -12,6 +12,7 @@ val empty_unfold: unfold_thms val map_unfolds_of: unfold_thms -> thm list val set_unfoldss_of: unfold_thms -> thm list list + val pred_unfolds_of: unfold_thms -> thm list val rel_unfolds_of: unfold_thms -> thm list val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> @@ -36,6 +37,7 @@ type unfold_thms = { map_unfolds: thm list, set_unfoldss: thm list list, + pred_unfolds: thm list, rel_unfolds: thm list }; @@ -44,17 +46,21 @@ fun adds_to_thms thms NONE = thms | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; -val empty_unfold = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []}; +val empty_unfold = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []}; -fun add_to_unfold_opt map_opt sets_opt rel_opt {map_unfolds, set_unfoldss, rel_unfolds} = { - map_unfolds = add_to_thms map_unfolds map_opt, - set_unfoldss = adds_to_thms set_unfoldss sets_opt, - rel_unfolds = add_to_thms rel_unfolds rel_opt}; +fun add_to_unfold_opt map_opt sets_opt pred_opt rel_opt + {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} = + {map_unfolds = add_to_thms map_unfolds map_opt, + set_unfoldss = adds_to_thms set_unfoldss sets_opt, + pred_unfolds = add_to_thms pred_unfolds pred_opt, + rel_unfolds = add_to_thms rel_unfolds rel_opt}; -fun add_to_unfold map sets rel = add_to_unfold_opt (SOME map) (SOME sets) (SOME rel); +fun add_to_unfold map sets pred rel = + add_to_unfold_opt (SOME map) (SOME sets) (SOME pred) (SOME rel); val map_unfolds_of = #map_unfolds; val set_unfoldss_of = #set_unfoldss; +val pred_unfolds_of = #pred_unfolds; val rel_unfolds_of = #rel_unfolds; val bdTN = "bdT"; @@ -64,8 +70,6 @@ fun mk_permuteN src dest = "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest); -val subst_rel_def = @{thm subst_rel_def}; - (*copied from Envir.expand_term_free*) fun expand_term_const defs = let @@ -99,9 +103,9 @@ (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3); val Bss_repl = replicate olive Bs; - val ((((fs', Rs'), Asets), xs), _(*names_lthy*)) = lthy + val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs) - ||>> apfst snd o mk_Frees' "R" (map2 (curry mk_relT) As Bs) + ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs) ||>> mk_Frees "A" (map HOLogic.mk_setT As) ||>> mk_Frees "x" As; @@ -116,13 +120,13 @@ (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) val mapx = fold_rev Term.abs fs' (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, - map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o + map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o mk_map_of_bnf Ds As Bs) Dss inners)); - (*%R1 ... Rn. outer.rel (inner_1.rel R1 ... Rn) ... (inner_m.rel R1 ... Rn)*) - val rel = fold_rev Term.abs Rs' - (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer, - map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o - mk_rel_of_bnf Ds As Bs) Dss inners)); + (*%Q1 ... Qn. outer.pred (inner_1.pred Q1 ... Qn) ... (inner_m.pred Q1 ... Qn)*) + val pred = fold_rev Term.abs Qs' + (Term.list_comb (mk_pred_of_bnf oDs CAs CBs outer, + map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o + mk_pred_of_bnf Ds As Bs) Dss inners)); (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*) (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) @@ -229,16 +233,20 @@ fun rel_O_Gr_tac _ = let + val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*) val outer_rel_Gr = rel_Gr_of_bnf outer RS sym; val outer_rel_cong = rel_cong_of_bnf outer; + val thm = + (trans OF [in_alt_thm RS @{thm subst_rel_def}, + trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF + [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]}, + rel_converse_of_bnf outer RS sym], outer_rel_Gr], + trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF + (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) + |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners); in - rtac (trans OF [in_alt_thm RS subst_rel_def, - trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF - [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]}, - rel_converse_of_bnf outer RS sym], outer_rel_Gr], - trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF - (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) 1 - end + unfold_defs_tac lthy basic_thms THEN rtac thm 1 + end; val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; @@ -264,10 +272,10 @@ val (bnf', lthy') = bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) - (((((b, mapx), sets), bd), wits), SOME rel) lthy; + (((((b, mapx), sets), bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') - unfold; + val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (rel_def_of_bnf bnf') unfold; in (bnf', (unfold', lthy')) end; @@ -299,8 +307,8 @@ (*bnf.map id ... id*) val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); - (*bnf.rel Id ... Id*) - val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map Id_const killedAs); + (*bnf.pred (op =) ... (op =)*) + val pred = Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = drop n bnf_sets; @@ -312,7 +320,7 @@ fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; fun map_comp_tac {context, ...} = - Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN + unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN rtac refl 1; fun map_cong_tac {context, ...} = mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf); @@ -340,14 +348,17 @@ fun rel_O_Gr_tac _ = let val rel_Gr = rel_Gr_of_bnf bnf RS sym + val thm = + (trans OF [in_alt_thm RS @{thm subst_rel_def}, + trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF + [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, + rel_converse_of_bnf bnf RS sym], rel_Gr], + trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF + (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @ + replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) + |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv}); in - rtac (trans OF [in_alt_thm RS subst_rel_def, - trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF - [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, - rel_converse_of_bnf bnf RS sym], rel_Gr], - trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF - (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @ - replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) 1 + rtac thm 1 end; val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac @@ -362,10 +373,10 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) - (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; + (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') - unfold; + val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (rel_def_of_bnf bnf') unfold; in (bnf', (unfold', lthy')) end; @@ -396,9 +407,8 @@ (*%f1 ... fn. bnf.map*) val mapx = fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); - (*%R1 ... Rn. bnf.rel*) - val rel = - fold_rev Term.absdummy (map2 (curry mk_relT) newAs newBs) (mk_rel_of_bnf Ds As Bs bnf); + (*%Q1 ... Qn. bnf.pred*) + val pred = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_pred_of_bnf Ds As Bs bnf); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets; @@ -407,7 +417,7 @@ fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; fun map_comp_tac {context, ...} = - Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN + unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN rtac refl 1; fun map_cong_tac {context, ...} = rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1); @@ -439,7 +449,7 @@ fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); fun rel_O_Gr_tac _ = - rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1; + mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; @@ -450,10 +460,10 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) - (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; + (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') - unfold; + val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (pred_def_of_bnf bnf') unfold; in (bnf', (unfold', lthy')) end; @@ -483,10 +493,10 @@ (*%f(1) ... f(n). bnf.map f\(1) ... f\(n)*) val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) - (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0)))); - (*%R(1) ... R(n). bnf.rel R\(1) ... R\(n)*) - val rel = fold_rev Term.absdummy (permute (map2 (curry mk_relT) As Bs)) - (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0)))); + (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0)))); + (*%Q(1) ... Q(n). bnf.pred Q\(1) ... Q\(n)*) + val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) + (Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0)))); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = permute bnf_sets; @@ -517,7 +527,7 @@ fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); fun rel_O_Gr_tac _ = - rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1; + mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac; @@ -528,10 +538,10 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) - (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; + (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; - val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') - unfold; + val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') + (pred_def_of_bnf bnf') unfold; in (bnf', (unfold', lthy')) end; @@ -607,22 +617,25 @@ val map_unfolds = map_unfolds_of unfold; val set_unfoldss = set_unfoldss_of unfold; + val pred_unfolds = pred_unfolds_of unfold; val rel_unfolds = rel_unfolds_of unfold; val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds); val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss); - val expand_rels = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) - rel_unfolds); - val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds; - val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss; - val unfold_defs = unfold_sets o unfold_maps; + val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) + pred_unfolds); + val unfold_maps = fold (unfold_defs lthy o single) map_unfolds; + val unfold_sets = fold (unfold_defs lthy) set_unfoldss; + val unfold_preds = unfold_defs lthy pred_unfolds; + val unfold_rels = unfold_defs lthy rel_unfolds; + val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels; val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf); val bnf_sets = map (expand_maps o expand_sets) (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); val bnf_bd = mk_bd_of_bnf Ds As bnf; - val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf); + val bnf_pred = expand_preds (mk_pred_of_bnf Ds As Bs bnf); val T = mk_T_of_bnf Ds As bnf; (*bd should only depend on dead type variables!*) @@ -655,22 +668,24 @@ @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2}, bd_Card_order_of_bnf bnf]]; - fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN' + fun mk_tac thm {context = ctxt, prems = _} = + (rtac (unfold_all thm) THEN' SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd) - (mk_tac (map_wpull_of_bnf bnf)) (mk_tac (rel_O_Gr_of_bnf bnf)); + (mk_tac (map_wpull_of_bnf bnf)) + (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf))); val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); - fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf)); + fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf)); val policy = user_policy Derive_All_Facts; val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads) - (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy; + (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_pred) lthy; in ((bnf', deads), lthy') end; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -35,6 +35,7 @@ val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic val mk_map_wpull_tac: thm -> thm list -> thm -> tactic + val mk_simple_rel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic val mk_simple_wit_tac: thm list -> tactic end; @@ -65,8 +66,8 @@ (* Composition *) fun mk_comp_set_alt_tac ctxt collect_set_natural = - Local_Defs.unfold_tac ctxt @{thms sym[OF o_assoc]} THEN - Local_Defs.unfold_tac ctxt [collect_set_natural RS sym] THEN + unfold_defs_tac ctxt @{thms sym[OF o_assoc]} THEN + unfold_defs_tac ctxt [collect_set_natural RS sym] THEN rtac refl 1; fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps = @@ -139,10 +140,9 @@ rtac bd; fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1}; in - Local_Defs.unfold_tac ctxt [comp_set_alt] THEN + unfold_defs_tac ctxt [comp_set_alt] THEN rtac @{thm comp_set_bd_Union_o_collect} 1 THEN - Local_Defs.unfold_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib - o_apply} THEN + unfold_defs_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN (rtac ctrans THEN' WRAP' gen_before gen_after bds (rtac last_bd) THEN' rtac @{thm ordIso_imp_ordLeq} THEN' @@ -154,12 +154,12 @@ conj_assoc}; fun mk_comp_in_alt_tac ctxt comp_set_alts = - Local_Defs.unfold_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN - Local_Defs.unfold_tac ctxt @{thms set_eq_subset} THEN + unfold_defs_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN + unfold_defs_tac ctxt @{thms set_eq_subset} THEN rtac conjI 1 THEN REPEAT_DETERM ( rtac @{thm subsetI} 1 THEN - Local_Defs.unfold_tac ctxt @{thms mem_Collect_eq Ball_def} THEN + unfold_defs_tac ctxt @{thms mem_Collect_eq Ball_def} THEN (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN REPEAT_DETERM (CHANGED (( (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE' @@ -216,7 +216,7 @@ fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms = ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN - Local_Defs.unfold_tac ctxt (collect_set_natural :: comp_wit_thms) THEN + unfold_defs_tac ctxt (collect_set_natural :: comp_wit_thms) THEN REPEAT_DETERM ( atac 1 ORELSE REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN @@ -409,6 +409,10 @@ WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); +fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm = + rtac (unfold_defs ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym])) + 1; + fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); end; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:49 2012 +0200 @@ -98,6 +98,7 @@ struct open BNF_Util +open BNF_Tactics open BNF_Def_Tactics type axioms = { @@ -140,22 +141,20 @@ fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd, in_bd, map_wpull, rel_O_Gr} = zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull - rel_O_Gr; + rel_O_Gr; -fun map_axioms f - {map_id = map_id, map_comp = map_comp, map_cong = map_cong, set_natural = set_natural, - bd_card_order = bd_card_order, bd_cinfinite = bd_cinfinite, set_bd = set_bd, in_bd = in_bd, - map_wpull = map_wpull, rel_O_Gr} = +fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd, + in_bd, map_wpull, rel_O_Gr} = {map_id = f map_id, - map_comp = f map_comp, - map_cong = f map_cong, - set_natural = map f set_natural, - bd_card_order = f bd_card_order, - bd_cinfinite = f bd_cinfinite, - set_bd = map f set_bd, - in_bd = f in_bd, - map_wpull = f map_wpull, - rel_O_Gr = f rel_O_Gr}; + map_comp = f map_comp, + map_cong = f map_cong, + set_natural = map f set_natural, + bd_card_order = f bd_card_order, + bd_cinfinite = f bd_cinfinite, + set_bd = map f set_bd, + in_bd = f in_bd, + map_wpull = f map_wpull, + rel_O_Gr = f rel_O_Gr}; val morph_axioms = map_axioms o Morphism.thm; @@ -168,8 +167,8 @@ fun mk_defs map sets pred rel = {map_def = map, set_defs = sets, pred_def = pred, rel_def = rel}; -fun map_defs f {map_def = map, set_defs = sets, pred_def = pred, rel_def = rel} = - {map_def = f map, set_defs = List.map f sets, pred_def = f pred, rel_def = f rel}; +fun map_defs f {map_def, set_defs, pred_def, rel_def} = + {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, rel_def = f rel_def}; val morph_defs = map_defs o Morphism.thm; @@ -429,8 +428,8 @@ let val thy = Proof_Context.theory_of ctxt; val tyenv = - Sign.typ_match thy (fastype_of pred, - Library.foldr (op -->) (instTs, instA --> instB --> HOLogic.boolT)) Vartab.empty; + Sign.typ_match thy (fastype_of pred, Library.foldr (op -->) (instTs, mk_pred2T instA instB)) + Vartab.empty; in Envir.subst_term (tyenv, Vartab.empty) pred end handle Type.TYPE_MATCH => error "Bad predicator"; @@ -464,8 +463,6 @@ else minimize ((I, wit) :: done) todo; in minimize [] wits end; -fun unfold_defs_tac lthy defs mk_tac context = Local_Defs.unfold_tac lthy defs THEN mk_tac context; - (* Names *) @@ -527,7 +524,7 @@ (* Define new BNFs *) fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt - (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy = + (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_pred_opt) no_defs_lthy = let val fact_policy = mk_fact_policy no_defs_lthy; val b = qualify raw_b; @@ -553,10 +550,10 @@ | T => err T) else (b, Local_Theory.full_name no_defs_lthy b); - fun maybe_define needed_for_extra_facts (b, rhs) lthy = + fun maybe_define user_specified (b, rhs) lthy = let val inline = - (not needed_for_extra_facts orelse fact_policy = Derive_Few_Facts) andalso + (user_specified orelse fact_policy = Derive_Few_Facts) andalso (case const_policy of Dont_Inline => false | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs @@ -593,10 +590,10 @@ (bnf_bd_term, raw_bd_def)), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = no_defs_lthy - |> maybe_define false map_bind_def - ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs - ||>> maybe_define false bd_bind_def - ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs + |> maybe_define true map_bind_def + ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs + ||>> maybe_define true bd_bind_def + ||>> apfst split_list o fold_map (maybe_define true) wit_binds_defs ||> `(maybe_restore no_defs_lthy); val phi = Proof_Context.export_morphism lthy_old lthy; @@ -662,12 +659,13 @@ val setRTsBsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ Cs); val setRT's = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ As'); val self_setRTs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ As'); - val QTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) As' Bs'; + val QTs = map2 mk_pred2T As' Bs'; val CA' = mk_bnf_T As' CA; val CB' = mk_bnf_T Bs' CA; val CC' = mk_bnf_T Cs CA; val CRs' = mk_bnf_T RTs CA; + val CA'CB' = HOLogic.mk_prodT (CA', CB'); val bnf_map_AsAs = mk_bnf_map As' As'; val bnf_map_AsBs = mk_bnf_map As' Bs'; @@ -678,13 +676,14 @@ val bnf_bd_As = mk_bnf_t As' bnf_bd; val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; - val ((((((((((((((((((((((((fs, fs_copy), gs), hs), (x, x')), (y, y')), (z, z')), zs), As), + val (((((((((((((((((((((((((fs, fs_copy), gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As), As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss), (Qs, Qs')), _) = lthy |> mk_Frees "f" (map2 (curry (op -->)) As' Bs') ||>> mk_Frees "f" (map2 (curry (op -->)) As' Bs') ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs) ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts) + ||>> yield_singleton (mk_Frees "p") CA'CB' ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "x") CA' ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "y") CB' ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs' @@ -707,7 +706,7 @@ ||>> mk_Frees' "Q" QTs; (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*) - val rel_O_Gr_rhs = + val O_Gr = let val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs); val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs); @@ -716,9 +715,39 @@ mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2) end; - val rel_rhs = (case raw_rel_opt of - NONE => fold_rev Term.absfree Rs' rel_O_Gr_rhs - | SOME raw_rel => prep_term no_defs_lthy raw_rel); + fun mk_predicate_of_set x_name y_name t = + let + val (T, U) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of t)); + val x = Free (x_name, T); + val y = Free (y_name, U); + in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end; + + val pred_rhs = (case raw_pred_opt of + NONE => + fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y') + (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, map3 (fn Q => fn T => fn U => + HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs'))) + | SOME raw_pred => prep_term no_defs_lthy raw_pred); + + val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs); + + val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) = + lthy + |> maybe_define (is_some raw_pred_opt) pred_bind_def + ||> `(maybe_restore lthy); + + val phi = Proof_Context.export_morphism lthy_old lthy; + val bnf_pred_def = Morphism.thm phi raw_pred_def; + val bnf_pred = Morphism.term phi bnf_pred_term; + + fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred; + + val pred = mk_bnf_pred QTs CA' CB'; + + val rel_rhs = + fold_rev Term.absfree Rs' (HOLogic.Collect_const CA'CB' $ + Term.lambda p (Term.list_comb (pred, map (mk_predicate_of_set (fst x') (fst y')) Rs) $ + HOLogic.mk_fst p $ HOLogic.mk_snd p)); val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs); @@ -735,25 +764,6 @@ val rel = mk_bnf_rel setRTs CA' CB'; - val pred_rhs = fold absfree (y' :: x' :: rev Qs') (HOLogic.mk_mem (HOLogic.mk_prod (x, y), - Term.list_comb (rel, map3 (fn Q => fn T => fn U => - HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) - Qs As' Bs'))); - val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs); - - val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) = - lthy - |> maybe_define true pred_bind_def - ||> `(maybe_restore lthy); - - val phi = Proof_Context.export_morphism lthy_old lthy; - val bnf_pred_def = Morphism.thm phi raw_pred_def; - val bnf_pred = Morphism.term phi bnf_pred_term; - - fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred; - - val pred = mk_bnf_pred QTs CA' CB'; - val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @ raw_wit_defs @ [raw_pred_def, raw_rel_def]) of [] => () @@ -852,8 +862,7 @@ (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull)) end; - val rel_O_Gr_goal = - fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), rel_O_Gr_rhs)); + val rel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), O_Gr)); val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal; @@ -1176,11 +1185,11 @@ | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts; fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds = - (fn (_, goals, wit_goalss, after_qed, lthy, defs) => + (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) => let val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN' - unfold_defs_tac lthy defs wit_tac; + mk_unfold_defs_then_tac lthy one_step_defs wit_tac; val wit_goals = map mk_conjunction_balanced' wit_goalss; val wit_thms = Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac @@ -1189,7 +1198,7 @@ |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); in map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] []) - goals (map (unfold_defs_tac lthy defs) tacs) + goals (map (mk_unfold_defs_then_tac lthy one_step_defs) tacs) |> (fn thms => after_qed (map single thms @ wit_thms) lthy) end) oo prepare_def const_policy fact_policy qualify (K I) Ds; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_def_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -71,8 +71,8 @@ val n = length set_naturals; in if null set_naturals then - Local_Defs.unfold_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 - else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN + unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 + else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN EVERY' [rtac equalityI, rtac subsetI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, @@ -105,7 +105,7 @@ end; fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN + unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN subst_tac ctxt [map_id] 1 THEN (if n = 0 then rtac refl 1 else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]}, @@ -113,7 +113,7 @@ CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1); fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt rel_O_Grs THEN + unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]}, rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; @@ -124,8 +124,8 @@ val n = length set_naturals; in if null set_naturals then - Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 - else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN + unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 + else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN EVERY' [rtac @{thm subrelI}, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, @@ -151,8 +151,8 @@ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; in - if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 - else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN + if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 + else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN EVERY' [rtac equalityI, rtac @{thm subrelI}, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, @@ -197,7 +197,7 @@ let val ls' = replicate (Int.max (1, m)) (); in - Local_Defs.unfold_tac ctxt (rel_O_Grs @ + unfold_defs_tac ctxt (rel_O_Grs @ @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl, diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_fp.ML --- a/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 02:42:49 2012 +0200 @@ -97,8 +97,6 @@ val retype_free: typ -> term -> term - val mk_predT: typ -> typ; - val mk_sumTN: typ list -> typ val mk_sumTN_balanced: typ list -> typ @@ -245,8 +243,6 @@ val mk_common_name = space_implode "_" o map Binding.name_of; -fun mk_predT T = T --> HOLogic.boolT; - fun retype_free T (Free (s, _)) = Free (s, T); fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 02:42:49 2012 +0200 @@ -261,7 +261,7 @@ (*avoid "'a itself" arguments in coiterators and corecursors*) val mss' = map (fn [0] => [1] | ms => ms) mss; - val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_predT) ns Cs; + val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs; fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss); @@ -277,7 +277,7 @@ map3 (fn C => map2 (map (map (curry (op -->) C) o maybe_dest_sumT) oo dest_tupleT)) Cs mss' f_prod_Tss; val q_Tssss = - map (map (map (fn [_] => [] | [_, C] => [mk_predT (domain_type C)]))) f_Tssss; + map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss; val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end; @@ -383,7 +383,7 @@ end; val sumEN_thm' = - Local_Defs.unfold lthy @{thms all_unit_eq} + unfold_defs lthy @{thms all_unit_eq} (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) [] (mk_sumEN_balanced n)) |> Morphism.thm phi; @@ -521,7 +521,7 @@ val (((phis, phis'), vs'), names_lthy) = lthy - |> mk_Frees' "P" (map mk_predT fpTs) + |> mk_Frees' "P" (map mk_pred1T fpTs) ||>> Variable.variant_fixes (map Binding.name_of fp_bs); val vs = map2 (curry Free) vs' fpTs; @@ -756,7 +756,7 @@ coiterss_goal coiter_tacss, map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context) - |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation)) + |> unfold_defs lthy @{thms sum_case_if} |> Thm.close_derivation)) corecss_goal corec_tacss) end; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -43,14 +43,14 @@ val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs; fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = - Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN + unfold_defs_tac ctxt [case_def, ctr_def, unf_fld] THEN (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' rtac refl) 1; fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = - Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN - Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN + unfold_defs_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN + unfold_defs_tac ctxt @{thms all_prod_eq} THEN EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)) 1; @@ -58,33 +58,33 @@ (rtac iffI THEN' EVERY' (map3 (fn cTs => fn cx => fn th => dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN' - SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN' + SELECT_GOAL (unfold_defs_tac ctxt [th]) THEN' atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1; fun mk_half_distinct_tac ctxt fld_inject ctr_defs = - Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN + unfold_defs_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN rtac @{thm sum.distinct(1)} 1; fun mk_inject_tac ctxt ctr_def fld_inject = - Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN - Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; + unfold_defs_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN + unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; val iter_like_thms = @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps split_conv}; fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt = - Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ - iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1; + unfold_defs_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ + iter_like_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1; val coiter_like_ss = ss_only @{thms if_True if_False}; val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases}; fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt = - Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN + unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN - Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN - Local_Defs.unfold_tac ctxt @{thms id_def} THEN + unfold_defs_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN + unfold_defs_tac ctxt @{thms id_def} THEN TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); val solve_prem_prem_tac = @@ -99,7 +99,7 @@ fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs = EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, - SELECT_GOAL (Local_Defs.unfold_tac ctxt + SELECT_GOAL (unfold_defs_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), solve_prem_prem_tac]) (rev kks)) 1; @@ -118,7 +118,7 @@ val nn = length ns; val n = Integer.sum ns; in - Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN + unfold_defs_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) pre_set_defss mss (unflat mss (1 upto n)) kkss) end; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:49 2012 +0200 @@ -220,9 +220,9 @@ val map_comp's = map map_comp'_of_bnf bnfs; val map_congs = map map_cong_of_bnf bnfs; val map_id's = map map_id'_of_bnf bnfs; - val pred_defs = map pred_def_of_bnf bnfs; val rel_congs = map rel_cong_of_bnf bnfs; val rel_converses = map rel_converse_of_bnf bnfs; + val rel_defs = map rel_def_of_bnf bnfs; val rel_Grs = map rel_Gr_of_bnf bnfs; val rel_Ids = map rel_Id_of_bnf bnfs; val rel_monos = map rel_mono_of_bnf bnfs; @@ -1060,9 +1060,9 @@ val sum_card_order = mk_sum_card_order bd_card_orders; - val sbd_ordIso = Local_Defs.fold lthy [sbd_def] + val sbd_ordIso = fold_defs lthy [sbd_def] (@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]); - val sbd_card_order = Local_Defs.fold lthy [sbd_def] + val sbd_card_order = fold_defs lthy [sbd_def] (@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]); val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite]; val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero}; @@ -1873,7 +1873,7 @@ ||>> mk_Frees "f" coiter_fTs ||>> mk_Frees "g" coiter_fTs ||>> mk_Frees "s" corec_sTs - ||>> mk_Frees "P" (map (fn T => T --> mk_predT T) Ts); + ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1)); val unf_name = Binding.name_of o unf_bind; @@ -2070,7 +2070,7 @@ val flds = mk_flds params'; val fld_defs = map (Morphism.thm phi) fld_def_frees; - val fld_o_unf_thms = map2 (Local_Defs.fold lthy o single) fld_defs coiter_o_unf_thms; + val fld_o_unf_thms = map2 (fold_defs lthy o single) fld_defs coiter_o_unf_thms; val unf_o_fld_thms = let @@ -2213,7 +2213,7 @@ val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl)); val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []); - val rel_coinduct = Local_Defs.unfold lthy @{thms diag_UNIV} + val rel_coinduct = unfold_defs lthy @{thms diag_UNIV} (Skip_Proof.prove lthy [] [] rel_coinduct_goal (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm)) |> Thm.close_derivation); @@ -2266,12 +2266,12 @@ (tcoalg_thm RS bis_diag_thm)))) |> Thm.close_derivation; - val pred_coinduct = rel_coinduct - |> Local_Defs.unfold lthy @{thms Id_def'} - |> Local_Defs.fold lthy pred_defs; - val pred_coinduct_upto = rel_coinduct_upto - |> Local_Defs.unfold lthy @{thms Id_def'} - |> Local_Defs.fold lthy pred_defs; + (*### FIXME: get rid of mem_Id_eq_eq? or Id_def'? *) + val pred_of_rel_thms = + rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv mem_Id_eq_eq snd_conv split_conv}; + + val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct; + val pred_coinduct_upto = unfold_defs lthy pred_of_rel_thms rel_coinduct_upto; in (unf_coinduct, rev (Term.add_tfrees unf_coinduct_goal []), rel_coinduct, pred_coinduct, unf_coinduct_upto, rel_coinduct_upto, pred_coinduct_upto) @@ -2291,7 +2291,7 @@ val pTs = map2 (curry op -->) passiveXs passiveCs; val uTs = map2 (curry op -->) Ts Ts'; val JRTs = map2 (curry mk_relT) passiveAs passiveBs; - val JphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs; + val JphiTs = map2 mk_pred2T passiveAs passiveBs; val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts'; val B1Ts = map HOLogic.mk_setT passiveAs; val B2Ts = map HOLogic.mk_setT passiveBs; @@ -2309,7 +2309,7 @@ ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' - ||>> mk_Freess "P" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs) + ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) ||>> mk_Frees "R" JRTs ||>> mk_Frees "P" JphiTs ||>> mk_Frees "B1" B1Ts @@ -2669,10 +2669,10 @@ map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss; - val rel_O_gr_tacs = replicate n (K (rtac refl 1)); + val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context); val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss - bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs; + bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs; val (hset_unf_incl_thmss, hset_hset_unf_incl_thmsss, hset_induct_thms) = let @@ -2714,7 +2714,7 @@ map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => ((set_minimal |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y') - |> Local_Defs.unfold lthy incls) OF + |> unfold_defs lthy incls) OF (replicate n ballI @ maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) |> singleton (Proof_Context.export names_lthy lthy) @@ -2865,10 +2865,10 @@ |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts all_witss lthy; - val fold_maps = Local_Defs.fold lthy (map (fn bnf => + val fold_maps = fold_defs lthy (map (fn bnf => mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs); - val fold_sets = Local_Defs.fold lthy (maps (fn bnf => + val fold_sets = fold_defs lthy (maps (fn bnf => map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs); val timer = time (timer "registered new codatatypes as BNFs"); @@ -2889,6 +2889,7 @@ val in_rels = map in_rel_of_bnf bnfs; val in_Jrels = map in_rel_of_bnf Jbnfs; + val Jrel_defs = map rel_def_of_bnf Jbnfs; val Jpred_defs = map pred_def_of_bnf Jbnfs; val folded_map_simp_thms = map fold_maps map_simp_thms; @@ -2919,10 +2920,11 @@ (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz'))); val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis; in - map3 (fn goal => fn pred_def => fn Jrel_simp => - Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Jpred_defs Jrel_simp) + map3 (fn goal => fn rel_def => fn Jrel_simp => + Skip_Proof.prove lthy [] [] goal + (mk_pred_simp_tac rel_def Jpred_defs Jrel_defs Jrel_simp) |> Thm.close_derivation) - goals pred_defs Jrel_simp_thms + goals rel_defs Jrel_simp_thms end; val timer = time (timer "additional properties"); diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -350,7 +350,7 @@ fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN + unfold_defs_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN EVERY' [rtac conjI, CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images, CONJ_WRAP' (fn (coalg_in, morE) => @@ -363,7 +363,7 @@ val n = length in_monos; val ks = 1 upto n; in - Local_Defs.unfold_tac ctxt [bis_def] THEN + unfold_defs_tac ctxt [bis_def] THEN EVERY' [rtac conjI, CONJ_WRAP' (fn i => EVERY' [rtac @{thm UN_least}, dtac bspec, atac, @@ -426,7 +426,7 @@ rtac conjI, etac @{thm Shift_prefCl}, rtac conjI, rtac ballI, rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1, - SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Succ_Shift shift_def}), + SELECT_GOAL (unfold_defs_tac ctxt @{thms Succ_Shift shift_def}), etac bspec, etac @{thm ShiftD}, CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD}, dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i), @@ -450,7 +450,7 @@ rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift}, rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)]; in - Local_Defs.unfold_tac ctxt defs THEN + unfold_defs_tac ctxt defs THEN CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1 end; @@ -603,7 +603,7 @@ val m = length strT_hsets; in if m = 0 then atac 1 - else (Local_Defs.unfold_tac ctxt [isNode_def] THEN + else (unfold_defs_tac ctxt [isNode_def] THEN EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], rtac exI, rtac conjI, atac, CONJ_WRAP' (fn (thm, i) => if i > m then atac @@ -992,7 +992,7 @@ (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), if n = 1 then K all_tac else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans), - SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl, + SELECT_GOAL (unfold_defs_tac ctxt [from_to_sbd]), rtac refl, rtac refl]) ks to_sbd_injs from_to_sbds)]; in @@ -1049,7 +1049,7 @@ fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt defs THEN + unfold_defs_tac ctxt defs THEN EVERY' [rtac conjI, CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps, CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) => @@ -1061,7 +1061,7 @@ (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1; fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt defs THEN + unfold_defs_tac ctxt defs THEN EVERY' [rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses, CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1; @@ -1116,14 +1116,14 @@ fun mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unfs {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply, + unfold_defs_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL, EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_unfs), rtac sym, rtac @{thm id_apply}] 1; fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong), + unfold_defs_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong), rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong, REPEAT_DETERM_N m o rtac refl, EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1; @@ -1262,7 +1262,7 @@ fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} = rtac coiter_unique 1 THEN - Local_Defs.unfold_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN + unfold_defs_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss @@ -1271,11 +1271,11 @@ val n = length map_simps; in EVERY' [rtac (Drule.instantiate' [] cts nat_induct), - REPEAT_DETERM o rtac allI, SELECT_GOAL (Local_Defs.unfold_tac ctxt rec_0s), + REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_defs_tac ctxt rec_0s), CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s, REPEAT_DETERM o rtac allI, CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY' - [SELECT_GOAL (Local_Defs.unfold_tac ctxt + [SELECT_GOAL (unfold_defs_tac ctxt (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), rtac @{thm Un_cong}, rtac refl, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) @@ -1372,14 +1372,14 @@ fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt [coalg_def] THEN + unfold_defs_tac ctxt [coalg_def] THEN CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) => EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), EVERY' (map (etac o mk_conjunctN m) (1 upto m)), pickWP_assms_tac, - SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}), rtac impI, + SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}), @@ -1394,16 +1394,16 @@ let val n = length map_comps; in - Local_Defs.unfold_tac ctxt [mor_def] THEN + unfold_defs_tac ctxt [mor_def] THEN EVERY' [rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n), CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) => EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], hyp_subst_tac, - SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}), + SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac (map_comp RS trans), - SELECT_GOAL (Local_Defs.unfold_tac ctxt (conv :: @{thms o_id id_o})), + SELECT_GOAL (unfold_defs_tac ctxt (conv :: @{thms o_id id_o})), rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac, pickWP_assms_tac]) (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1 @@ -1413,12 +1413,12 @@ val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)}; fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN + unfold_defs_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN CONJ_WRAP' (fn (coiter, map_comp) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], hyp_subst_tac, - SELECT_GOAL (Local_Defs.unfold_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})), + SELECT_GOAL (unfold_defs_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})), rtac refl]) (coiters ~~ map_comps) 1; @@ -1442,12 +1442,12 @@ rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac ord_eq_le_trans, rtac rec_Suc, rtac @{thm Un_least}, - SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, nth set_naturals (j - 1), + SELECT_GOAL (unfold_defs_tac ctxt [coiter, nth set_naturals (j - 1), @{thm prod.cases}]), etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) => EVERY' [rtac @{thm UN_least}, - SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, set_natural, @{thm prod.cases}]), + SELECT_GOAL (unfold_defs_tac ctxt [coiter, set_natural, @{thm prod.cases}]), etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, etac set_mp, atac]) (ks ~~ rev (drop m set_naturals))]) @@ -1482,7 +1482,7 @@ ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN REPEAT_DETERM (atac 1 ORELSE EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, - K (Local_Defs.unfold_tac ctxt unf_flds), + K (unfold_defs_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE, REPEAT_DETERM o (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN' @@ -1490,11 +1490,11 @@ (dresolve_tac wit THEN' (etac FalseE ORELSE' EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, - K (Local_Defs.unfold_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1); + K (unfold_defs_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1); fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} = rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN - Local_Defs.unfold_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN + unfold_defs_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN ALLGOALS (TRY o FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:49 2012 +0200 @@ -794,7 +794,7 @@ ||>> mk_Frees' "x" init_FTs ||>> mk_Frees "f" init_fTs ||>> mk_Frees "f" init_fTs - ||>> mk_Frees "P" (replicate n (mk_predT initT)); + ||>> mk_Frees "P" (replicate n (mk_pred1T initT)); val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss) (HOLogic.mk_conj (HOLogic.mk_eq (iidx, @@ -991,8 +991,8 @@ ||>> mk_Frees "s" rec_sTs; val Izs = map2 retype_free Ts zs; - val phis = map2 retype_free (map mk_predT Ts) init_phis; - val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis; + val phis = map2 retype_free (map mk_pred1T Ts) init_phis; + val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis; fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1)); val fld_name = Binding.name_of o fld_bind; @@ -1167,7 +1167,7 @@ val unfs = mk_unfs params'; val unf_defs = map (Morphism.thm phi) unf_def_frees; - val fld_o_unf_thms = map2 (Local_Defs.fold lthy o single) unf_defs fld_o_iter_thms; + val fld_o_unf_thms = map2 (fold_defs lthy o single) unf_defs fld_o_iter_thms; val unf_o_fld_thms = let @@ -1356,7 +1356,7 @@ val XTs = mk_Ts passiveXs; val YTs = mk_Ts passiveYs; val IRTs = map2 (curry mk_relT) passiveAs passiveBs; - val IphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs; + val IphiTs = map2 mk_pred2T passiveAs passiveBs; val (((((((((((((((fs, fs'), fs_copy), us), B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis), @@ -1670,10 +1670,10 @@ in_incl_min_alg_thms card_of_min_alg_thms; val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms; - val rel_O_gr_tacs = replicate n (K (rtac refl 1)); + val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context); val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss - bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs; + bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs; val fld_witss = let @@ -1711,10 +1711,10 @@ |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; - val fold_maps = Local_Defs.fold lthy (map (fn bnf => + val fold_maps = fold_defs lthy (map (fn bnf => mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs); - val fold_sets = Local_Defs.fold lthy (maps (fn bnf => + val fold_sets = fold_defs lthy (maps (fn bnf => map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs); val timer = time (timer "registered new datatypes as BNFs"); @@ -1731,7 +1731,8 @@ val in_rels = map in_rel_of_bnf bnfs; val in_Irels = map in_rel_of_bnf Ibnfs; - val pred_defs = map pred_def_of_bnf bnfs; + val rel_defs = map rel_def_of_bnf bnfs; + val Irel_defs = map rel_def_of_bnf Ibnfs; val Ipred_defs = map pred_def_of_bnf Ibnfs; val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; @@ -1764,10 +1765,11 @@ (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF)); val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis; in - map3 (fn goal => fn pred_def => fn Irel_simp => - Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Ipred_defs Irel_simp) + map3 (fn goal => fn rel_def => fn Irel_simp => + Skip_Proof.prove lthy [] [] goal + (mk_pred_simp_tac rel_def Ipred_defs Irel_defs Irel_simp) |> Thm.close_derivation) - goals pred_defs Irel_simp_thms + goals rel_defs Irel_simp_thms end; val timer = time (timer "additional properties"); diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -390,7 +390,7 @@ fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} = EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN - Local_Defs.unfold_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1; + unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1; fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets set_natural's str_init_defs = @@ -435,7 +435,7 @@ rtac mor_select THEN' atac THEN' rtac CollectI THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' atac THEN' - K (Local_Defs.unfold_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN' + K (unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN' etac mor_comp THEN' etac mor_incl_min_alg) 1 end; @@ -490,7 +490,7 @@ end; fun mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} = - (K (Local_Defs.unfold_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN' + (K (unfold_defs_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN' EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN' EVERY' (map rtac inver_Abss) THEN' EVERY' (map rtac inver_Reps)) 1; @@ -526,7 +526,7 @@ rtac sym, rtac id_apply] 1; fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}= - Local_Defs.unfold_tac ctxt + unfold_defs_tac ctxt (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}), rtac @{thm snd_convol'}] 1; @@ -813,8 +813,7 @@ CONJ_WRAP' (fn (set_simp, passive_set_natural) => EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least}, rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]}, - rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, - atac, + rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (active_set_natural, in_Irel) => EVERY' [rtac ord_eq_le_trans, rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least}, diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -16,6 +16,8 @@ val subst_asm_tac: Proof.context -> thm list -> int -> tactic val subst_tac: Proof.context -> thm list -> int -> tactic val substs_tac: Proof.context -> thm list -> int -> tactic + val unfold_defs_tac: Proof.context -> thm list -> tactic + val mk_unfold_defs_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> @@ -24,7 +26,9 @@ val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm - val mk_pred_simp_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic + val simple_rel_O_Gr_tac: Proof.context -> tactic + val mk_pred_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> + tactic val mk_map_comp_id_tac: thm -> tactic val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic @@ -53,13 +57,16 @@ rtac (Drule.instantiate_normalize insts thm) 1 end); -(*unlike "unfold_tac", succeeds when the RHS contains schematic variables not in the LHS*) +fun unfold_defs_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); + +fun mk_unfold_defs_then_tac lthy defs tac x = unfold_defs_tac lthy defs THEN tac x; + +(*unlike "unfold_defs_tac", succeeds when the RHS contains schematic variables not in the LHS*) fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0]; fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0]; fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt; - (* Theorems for open typedefs with UNIV as representing set *) fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I); @@ -91,9 +98,17 @@ gen_tac end; -fun mk_pred_simp_tac pred_def pred_defs rel_simp {context = ctxt, prems = _} = - Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN - rtac rel_simp 1; +fun simple_rel_O_Gr_tac ctxt = + unfold_defs_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1; + +fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} = + unfold_defs_tac ctxt IJpred_defs THEN + subst_tac ctxt [unfold_defs ctxt (IJpred_defs @ IJrel_defs @ + @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN + unfold_defs_tac ctxt (rel_def :: + @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv + split_conv}) THEN + rtac refl 1; fun mk_map_comp_id_tac map_comp = (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 02:42:49 2012 +0200 @@ -62,6 +62,9 @@ val strip_typeN: int -> typ -> typ list * typ + val mk_predT: typ list -> typ + val mk_pred1T: typ -> typ + val mk_pred2T: typ -> typ -> typ val mk_optionT: typ -> typ val mk_relT: typ * typ -> typ val dest_relT: typ -> typ * typ @@ -122,6 +125,9 @@ val mk_trans: thm -> thm -> thm val mk_unabs_def: int -> thm -> thm + val fold_defs: Proof.context -> thm list -> thm -> thm + val unfold_defs: Proof.context -> thm list -> thm -> thm + val mk_permute: ''a list -> ''a list -> 'b list -> 'b list val find_indices: ''a list -> ''a list -> int list @@ -316,8 +322,11 @@ fun strip_typeN 0 T = ([], T) | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T - | strip_typeN n T = raise TYPE ("strip_typeN", [T], []); + | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []); +fun mk_predT Ts = Ts ---> HOLogic.boolT; +fun mk_pred1T T = mk_predT [T]; +fun mk_pred2T T U = mk_predT [T, U]; fun mk_optionT T = Type (@{type_name option}, [T]); val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; @@ -583,4 +592,7 @@ fun mk_unabs_def 0 thm = thm | mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]}; +fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms); +fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); + end; diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 02:42:49 2012 +0200 @@ -166,7 +166,7 @@ ||>> yield_singleton (mk_Frees "w") dataT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; - val q = Free (fst p', B --> HOLogic.boolT); + val q = Free (fst p', mk_pred1T B); fun ap_v t = t $ v; fun mk_v_eq_v () = HOLogic.mk_eq (v, v); @@ -200,7 +200,7 @@ (true, [], [], [], [], [], no_defs_lthy) else let - fun disc_free b = Free (Binding.name_of b, dataT --> HOLogic.boolT); + fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT); fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); @@ -417,7 +417,7 @@ disc_defs'; val not_discI_thms = map2 (fn m => fn def => funpow m (fn thm => allI RS thm) - (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) + (unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) ms disc_defs'; val (disc_thmss', disc_thmss) = diff -r 9ef072c757ca -r 83ac281bcdc2 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Thu Sep 20 02:42:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Thu Sep 20 02:42:49 2012 +0200 @@ -38,7 +38,7 @@ fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' = EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, - hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, + hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct, rtac exhaust'] @ (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |> k = 1 ? swap |> op @)) 1; @@ -64,13 +64,13 @@ else REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' - SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' + SELECT_GOAL (unfold_defs_tac ctxt sel_thms) THEN' rtac refl)) 1; fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss = (rtac exhaust' THEN' EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => - EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)), + EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_disc_thms @ sel_thms)), rtac case_thm]) case_thms (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) disc_thmss') sel_thmss)) 1; @@ -90,6 +90,6 @@ val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; fun mk_split_asm_tac ctxt split = - rtac (split RS trans) 1 THEN Local_Defs.unfold_tac ctxt split_asm_thms THEN rtac refl 1; + rtac (split RS trans) 1 THEN unfold_defs_tac ctxt split_asm_thms THEN rtac refl 1; end;