# HG changeset patch # User blanchet # Date 1429465416 -7200 # Node ID 4e1ba085be4acd2336fb2b3ad79ae01d9a1faf61 # Parent 852f7a49ec0ce619a47d6316585fc2573eb6b9ba suppressed warnings diff -r 852f7a49ec0c -r 4e1ba085be4a src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Sun Apr 19 19:29:38 2015 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Sun Apr 19 19:43:36 2015 +0200 @@ -1183,7 +1183,7 @@ each equation. For example: *} - primrec bool_of_trool :: "trool \ bool" where + primrec (nonexhaustive) bool_of_trool :: "trool \ bool" where "bool_of_trool Faalse \ False" | "bool_of_trool Truue \ True" @@ -1227,7 +1227,7 @@ text {* \blankline *} - primrec at :: "'a list \ nat \ 'a" where + primrec (nonexhaustive) at :: "'a list \ nat \ 'a" where "at (x # xs) j = (case j of Zero \ x @@ -1364,7 +1364,7 @@ text {* \blankline *} - primrec subtree_ft :: "'a \ 'a ftree \ 'a ftree" where + primrec (nonexhaustive) subtree_ft :: "'a \ 'a ftree \ 'a ftree" where "subtree_ft x (FTNode g) = g x" text {* @@ -1390,7 +1390,7 @@ text {* \blankline *} - primrec subtree_ft2 :: "'a \ 'a \ 'a ftree2 \ 'a ftree2" where + primrec (nonexhaustive) subtree_ft2 :: "'a \ 'a \ 'a ftree2 \ 'a ftree2" where "subtree_ft2 x y (FTNode2 g) = g x y" @@ -1409,7 +1409,7 @@ datatypes. For example: *} - primrec + primrec (nonexhaustive) at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \ nat list \ 'a" and ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \ nat \ nat list \ 'a" where @@ -2718,15 +2718,17 @@ show "map_fn id = id" by transfer auto next - fix F G show "map_fn (G \ F) = map_fn G \ map_fn F" + fix f :: "'a \ 'b" and g :: "'b \ 'c" + show "map_fn (g \ f) = map_fn g \ map_fn f" by transfer (auto simp add: comp_def) next - fix F f g + fix F :: "('d, 'a) fn" and f g :: "'a \ 'b" assume "\x. x \ set_fn F \ f x = g x" thus "map_fn f F = map_fn g F" by transfer auto next - fix f show "set_fn \ map_fn f = op ` f \ set_fn" + fix f :: "'a \ 'b" + show "set_fn \ map_fn f = op ` f \ set_fn" by transfer (auto simp add: comp_def) next show "card_order (natLeq +c |UNIV \ 'd set| )" @@ -2746,11 +2748,11 @@ by (rule ordLeq_csum2) (rule card_of_Card_order) finally show "|set_fn F| \o natLeq +c |UNIV \ 'd set|" . next - fix R S + fix R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ bool" show "rel_fn R OO rel_fn S \ rel_fn (R OO S)" by (rule, transfer) (auto simp add: rel_fun_def) next - fix R + fix R :: "'a \ 'b \ bool" show "rel_fn R = (BNF_Def.Grp {x. set_fn x \ Collect (split R)} (map_fn fst))\\ OO BNF_Def.Grp {x. set_fn x \ Collect (split R)} (map_fn snd)"