src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 46316 1c9a548c0402
parent 46309 693d8d7bc3cd
child 46335 0fd9ab902b5a
equal deleted inserted replaced
46315:40522961d4b1 46316:1c9a548c0402
   386 
   386 
   387 val rewrs =
   387 val rewrs =
   388     map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   388     map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   389       (@{thms all_simps} @ @{thms ex_simps})
   389       (@{thms all_simps} @ @{thms ex_simps})
   390     @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   390     @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   391         [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}]
   391         [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
       
   392          @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
   392 
   393 
   393 fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
   394 fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
   394 
   395 
   395 fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   396 fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   396     apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
   397     apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)