Nominal/Ex/SingleLet.thy
changeset 2392 9294d7cec5e2
parent 2389 0f24c961b5f6
child 2393 d9a0cf26a88c
equal deleted inserted replaced
2391:ea143c806db6 2392:9294d7cec5e2
    22   "bn (As x y t) = {atom x}"
    22   "bn (As x y t) = {atom x}"
    23 
    23 
    24 thm alpha_sym_thms
    24 thm alpha_sym_thms
    25 thm alpha_trans_thms
    25 thm alpha_trans_thms
    26 thm size_eqvt
    26 thm size_eqvt
       
    27 thm size_simps
       
    28 thm size_rsp
    27 thm alpha_bn_imps
    29 thm alpha_bn_imps
    28 thm distinct
    30 thm distinct
    29 thm eq_iff
    31 thm eq_iff
    30 thm eq_iff_simps
    32 thm eq_iff_simps
    31 thm fv_defs
    33 thm fv_defs
    40 term App
    42 term App
    41 term Baz
    43 term Baz
    42 term bn
    44 term bn
    43 term fv_trm
    45 term fv_trm
    44 term alpha_bn
    46 term alpha_bn
    45 
       
    46 
    47 
    47 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
    48 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
    48 
    49 
    49 ML {* 
    50 ML {* 
    50   val pre_ss = @{thms fun_rel_def}
    51   val pre_ss = @{thms fun_rel_def}
    75   "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw"
    76   "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw"
    76   "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw"
    77   "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw"
    77   "(alpha_assg_raw ===> op =) bn_raw bn_raw"
    78   "(alpha_assg_raw ===> op =) bn_raw bn_raw"
    78   "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
    79   "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
    79   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
    80   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
    80 apply(simp_all add: alpha_bn_imps funs_rsp)
    81   "(alpha_trm_raw ===> op =) size size"
       
    82 apply(simp_all add: alpha_bn_imps funs_rsp size_rsp)
    81 sorry
    83 sorry
    82 
    84 
    83 ML {*
    85 ML {*
    84   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
    86   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
    85 *}
    87 *}