src/HOL/Quickcheck_Narrowing.thy
changeset 65480 5407bc278c9a
parent 61799 4cf66f21b764
child 65481 b11b7ad22684
equal deleted inserted replaced
65479:7ca8810b1d48 65480:5407bc278c9a
   102   "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
   102   "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
   103 
   103 
   104 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
   104 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
   105 where
   105 where
   106   "apply f a d =
   106   "apply f a d =
   107      (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
   107      (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow>
   108        case a (d - 1) of Narrowing_cons ta cas =>
   108        case a (d - 1) of Narrowing_cons ta cas \<Rightarrow>
   109        let
   109        let
   110          shallow = (d > 0 \<and> non_empty ta);
   110          shallow = d > 0 \<and> non_empty ta;
   111          cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
   111          cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs]
   112        in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
   112        in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)"
   113 
   113 
   114 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   114 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   115 where
   115 where
   116   "sum a b d =
   116   "sum a b d =
   117     (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => 
   117     (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca =>