src/HOL/Quickcheck_Narrowing.thy
changeset 65482 721feefce9c6
parent 65481 b11b7ad22684
child 66148 5e60c2d0a1f1
equal deleted inserted replaced
65481:b11b7ad22684 65482:721feefce9c6
    97 where
    97 where
    98   "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
    98   "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
    99 
    99 
   100 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
   100 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
   101 where
   101 where
   102   "apply f a d =
   102   "apply f a d = (if d > 0 then
   103      (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow>
   103      (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow>
   104        case a (d - 1) of Narrowing_cons ta cas \<Rightarrow>
   104        case a (d - 1) of Narrowing_cons ta cas \<Rightarrow>
   105        let
   105        let
   106          shallow = d > 0 \<and> non_empty ta;
   106          shallow = non_empty ta;
   107          cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs]
   107          cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs]
   108        in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)"
   108        in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)
       
   109      else Narrowing_cons (Narrowing_sum_of_products []) [])"
   109 
   110 
   110 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   111 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   111 where
   112 where
   112   "sum a b d =
   113   "sum a b d =
   113     (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => 
   114     (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca =>