6 declare [[STEPS = 2]]

     6 declare [[STEPS = 20]]

     7 

     7 

     8 nominal_datatype 'a lam =

     8 class s1

     9 class s2

    10 

    11 nominal_datatype lambda: 

    12  ('a, 'b) lam =

    10 | App "'a lam" "'a lam"

    14 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"

    11 | Lam x::"name" l::"'a lam"  bind x in l

    15 | Lam x::"name" l::"('a, 'b) lam"  bind x in l

    12 

    16 

    13 ML {* Datatype.read_typ *}

    17 term Var_raw

    18 term Var

    19 term App_raw

    20 term App

    21 thm Var_def App_def Lam_def

    22 term abs_lam

    23 

    24 thm distinct

    25 thm lam_raw.inducts

    26 thm lam_raw.exhaust

    27 thm fv_defs

    28 thm bn_defs

    29 thm perm_simps

    30 thm perm_laws

    31 thm lam_raw.size

    32 thm eq_iff

    33 thm eq_iff_simps

    34 thm fv_eqvt

    35 thm bn_eqvt

    36 thm size_eqvt

    37 

    38 ML {*

    39   val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}]

    40 *}

    41 

    42 ML {*

    43   val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})

    44 *}

    45 

    46 ML {* 

    47   val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct}

    48 *}

    49 

    50 ML {* 

    51   val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust}

    52 *}

    53 

    54 ML {*

    55   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}

    56 *}

    57 

    58 ML {*

    59   val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}

    60 *}

    61 

    62 ML {*

    63   val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}

    64 *}

    65 

    66 ML {*

    67   val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

    68     prod.cases}

    69 *}

    70 

    71 (*  HERE *)

    72 

    73 ML {*

    74  val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}

    75 *}

    76 

    77 ML {*

    78  val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps}

    79 *}

    80 

    81 

    82 ML {*

    83   val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}

    84 *}

    85 

    86 ML {*

    87   val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}

    88 *}

    89 

    90 ML {*

    91   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}

    92 *}

    93 

    94 ML {*

    95   val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}

    96 *}

    97 

    98 

    99 

   100 ML {*

   101   space_explode "_raw" "bla_raw2_foo_raw3.0"

   102 *}

   103