src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63731 9f906a2eb0e7
child 69597 ff784d5a5bfb
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
blanchet@63731
     1
theory Quickcheck_Nesting
blanchet@63731
     2
imports Main
blanchet@63731
     3
begin
blanchet@63731
     4
blanchet@63731
     5
ML \<open>
blanchet@63731
     6
let
blanchet@63731
     7
  open BNF_FP_Def_Sugar
blanchet@63731
     8
  open BNF_LFP_Compat
blanchet@63731
     9
blanchet@63731
    10
  val compat_plugin = Plugin_Name.declare_setup @{binding compat};
blanchet@63731
    11
blanchet@63731
    12
  fun compat fp_sugars =
blanchet@63731
    13
    perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars)));
blanchet@63731
    14
in
blanchet@63731
    15
  Theory.setup (fp_sugars_interpretation compat_plugin compat)
blanchet@63731
    16
end
blanchet@63731
    17
\<close>
blanchet@63731
    18
blanchet@63731
    19
end