--- a/NEWS Mon Mar 07 23:20:11 2016 +0100
+++ b/NEWS Mon Mar 07 23:20:11 2016 +0100
@@ -48,6 +48,7 @@
rel_prod_apply ~> rel_prod_inject
pred_prod_apply ~> pred_prod_inject
INCOMPATIBILITY.
+ - The "size" plugin has been made compatible again with locales.
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
resemble the f.split naming convention, INCOMPATIBILITY.
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy Mon Mar 07 23:20:11 2016 +0100
@@ -57,11 +57,18 @@
('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
*)
-datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
-and 'a I2 = I21 | I22 "'a I1" "'a I2"
+locale loc =
+ fixes c :: 'a and d :: 'a
+ assumes "c \<noteq> d"
+begin
-datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
-and 'a forest = FNil | FCons "'a tree" "'a forest"
+datatype (discs_sels) 'b I1 = I11 'b "'b I1" | I12 'b "'b I2"
+and 'b I2 = I21 | I22 "'b I1" "'b I2"
+
+datatype (discs_sels) 'b tree = TEmpty | TNode 'b "'b forest"
+and 'b forest = FNil | FCons "'b tree" "'b forest"
+
+end
datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
and 'a branch = Branch 'a "'a tree'"
@@ -217,12 +224,6 @@
by countable_datatype
*)
-instance I1 and I2 :: (countable) countable
- by countable_datatype
-
-instance tree and forest :: (countable) countable
- by countable_datatype
-
instance tree' and branch :: (countable) countable
by countable_datatype
@@ -318,8 +319,6 @@
datatype_compat simple''
datatype_compat mylist
datatype_compat some_passive
-datatype_compat I1 I2
-datatype_compat tree forest
datatype_compat tree' branch
datatype_compat bin_rose_tree
datatype_compat exp trm factor
--- a/src/HOL/Datatype_Examples/Misc_Primrec.thy Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Primrec.thy Mon Mar 07 23:20:11 2016 +0100
@@ -53,15 +53,18 @@
"rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
"rename_lam f (Let SL l) = Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l)"
-primrec
- sum_i1 :: "('a::{zero,plus}) I1 \<Rightarrow> 'a" and
- sum_i2 :: "'a I2 \<Rightarrow> 'a"
+primrec (in loc)
+ sum_i1 :: "('b::{zero,plus}) I1 \<Rightarrow> 'b" and
+ sum_i2 :: "'b I2 \<Rightarrow> 'b"
where
"sum_i1 (I11 n i) = n + sum_i1 i" |
"sum_i1 (I12 n i) = n + sum_i2 i" |
"sum_i2 I21 = 0" |
"sum_i2 (I22 i j) = sum_i1 i + sum_i2 j"
+context loc
+begin
+
primrec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
"forest_of_mylist MyNil = FNil" |
"forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)"
@@ -90,6 +93,8 @@
"mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" |
"mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
+end
+
primrec
id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Mar 07 23:20:11 2016 +0100
@@ -77,7 +77,8 @@
val size_of_global = Symtab.lookup o Data.get o Context.Theory;
fun all_overloaded_size_defs_of ctxt =
- Symtab.fold (fn (_, (_, (overloaded_size_def, _, _))) => cons overloaded_size_def)
+ Symtab.fold (fn (_, (_, (overloaded_size_def, _, _))) =>
+ can (Logic.dest_equals o Thm.prop_of) overloaded_size_def ? cons overloaded_size_def)
(Data.get (Context.Proof ctxt)) [];
val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]};