1 (*  Title:      nominal_dt_alpha.ML

     2     Author:     Cezary Kaliszyk

     3     Author:     Christian Urban

     4 

     5   Definitions of the alpha relations.

     6 *)

     7 

     8 signature NOMINAL_DT_ALPHA =

     9 sig

    10   val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->

    11     bclause list list list -> term list -> Proof.context -> 

    12     term list * thm list * thm list * thm * local_theory

    13 end

    14 

    15 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =

    16 struct

    17 

    18 (* construct the compound terms for prod_fv and prod_alpha *)

    19 fun mk_prod_fv (t1, t2) =

    20 let

    21   val ty1 = fastype_of t1

    22   val ty2 = fastype_of t2 

    23   val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}

    24 in

    25   Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2

    26 end

    27 

    28 fun mk_prod_alpha (t1, t2) =

    29 let

    30   val ty1 = fastype_of t1

    31   val ty2 = fastype_of t2 

    32   val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)

    33   val resT = [prodT, prodT] ---> @{typ "bool"}

    34 in

    35   Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2

    36 end

    37 

    38 (* generates the compound binder terms *)

    39 fun mk_binders lthy bmode args bodies = 

    40 let  

    41   fun bind_set lthy args (NONE, i) = setify lthy (nth args i)

    42     | bind_set _ args (SOME bn, i) = bn $ (nth args i)

    43   fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)

    44     | bind_lst _ args (SOME bn, i) = bn $ (nth args i)

    45 

    46   val (combine_fn, bind_fn) =

    47     case bmode of

    48       Lst => (mk_append, bind_lst) 

    49     | Set => (mk_union,  bind_set)

    50     | Res => (mk_union,  bind_set)

    51 in

    52   foldl1 combine_fn (map (bind_fn lthy args) bodies)

    53 end

    54 

    55 (* produces the term for an alpha with abstraction *)

    56 fun mk_alpha_term bmode fv alpha args args' binders binders' =

    57 let

    58   val (alpha_name, binder_ty) = 

    59     case bmode of

    60       Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})

    61     | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})

    62     | Res => (@{const_name "alpha_res"}, @{typ "atom set"})

    63   val ty = fastype_of args

    64   val pair_ty = HOLogic.mk_prodT (binder_ty, ty)

    65   val alpha_ty = [ty, ty] ---> @{typ "bool"}

    66   val fv_ty = ty --> @{typ "atom set"}

    67   val pair_lhs = HOLogic.mk_prod (binders, args)

    68   val pair_rhs = HOLogic.mk_prod (binders', args')

    69 in

    70   HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},

    71     Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) 

    72       $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)

    73 end

    74 

    75 (* for non-recursive binders we have to produce alpha_bn premises *)

    76 fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = 

    77   case binder of

    78     (NONE, _) => []

    79   | (SOME bn, i) =>

    80      if member (op=) bodies i then [] 

    81      else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]

    82 

    83 (* generat the premises for an alpha rule; mk_frees is used

    84    if no binders are present *)

    85 fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =

    86 let

    87   fun mk_frees i =

    88     let

    89       val arg = nth args i

    90       val arg' = nth args' i

    91       val ty = fastype_of arg

    92     in

    93       if nth is_rec i

    94       then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'

    95       else HOLogic.mk_eq (arg, arg')

    96     end

    97 

    98   fun mk_alpha_fv i = 

    99     let

   100       val ty = fastype_of (nth args i)

   101     in

   102       case AList.lookup (op=) alpha_map ty of

   103         NONE => (HOLogic.eq_const ty, supp_const ty) 

   104       | SOME (alpha, fv) => (alpha, fv) 

   105     end  

   106 in

   107   case bclause of

   108     BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies 

   109   | BC (bmode, binders, bodies) => 

   110     let

   111       val (alphas, fvs) = split_list (map mk_alpha_fv bodies)

   112       val comp_fv = foldl1 mk_prod_fv fvs

   113       val comp_alpha = foldl1 mk_prod_alpha alphas

   114       val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)

   115       val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)

   116       val comp_binders = mk_binders lthy bmode args binders

   117       val comp_binders' = mk_binders lthy bmode args' binders

   118       val alpha_prem = 

   119         mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'

   120       val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)

   121     in

   122       map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)

   123     end

   124 end

   125 

   126 (* produces the introduction rule for an alpha rule *)

   127 fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = 

   128 let

   129   val arg_names = Datatype_Prop.make_tnames arg_tys

   130   val arg_names' = Name.variant_list arg_names arg_names

   131   val args = map Free (arg_names ~~ arg_tys)

   132   val args' = map Free (arg_names' ~~ arg_tys)

   133   val alpha = fst (the (AList.lookup (op=) alpha_map ty))

   134   val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))

   135   val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses

   136 in

   137   Library.foldr Logic.mk_implies (flat prems, concl)

   138 end

   139 

   140 (* produces the premise of an alpha-bn rule; we only need to

   141    treat the case special where the binding clause is empty;

   142    

   143    - if the body is not included in the bn_info, then we either

   144      produce an equation or an alpha-premise

   145 

   146    - if the body is included in the bn_info, then we create

   147      either a recursive call to alpha-bn, or no premise  *)

   148 fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =

   149 let

   150   fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i = 

   151   let

   152     val arg = nth args i

   153     val arg' = nth args' i

   154     val ty = fastype_of arg

   155   in

   156     case AList.lookup (op=) bn_args i of

   157       NONE => (case (AList.lookup (op=) alpha_map ty) of

   158                  NONE =>  [HOLogic.mk_eq (arg, arg')]

   159                | SOME (alpha, _) => [alpha $ arg $ arg'])

   160     | SOME (NONE) => []

   161     | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']

   162   end  

   163 in

   164   case bclause of

   165     BC (_, [], bodies) => 

   166       map HOLogic.mk_Trueprop 

   167         (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))

   168   | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause

   169 end

   170 

   171 fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =

   172 let

   173   val arg_names = Datatype_Prop.make_tnames arg_tys

   174   val arg_names' = Name.variant_list arg_names arg_names

   175   val args = map Free (arg_names ~~ arg_tys)

   176   val args' = map Free (arg_names' ~~ arg_tys)

   177   val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)

   178   val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))

   179   val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses

   180 in

   181   Library.foldr Logic.mk_implies (flat prems, concl)

   182 end

   183 

   184 fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 

   185 let

   186   val nth_constrs_info = nth constrs_info bn_n

   187   val nth_bclausess = nth bclausesss bn_n

   188 in

   189   map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess

   190 end

   191 

   192 fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =

   193 let

   194   val alpha_names = prefix_dt_names descr sorts "alpha_"

   195   val alpha_arg_tys = all_dtyps descr sorts

   196   val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys

   197   val alpha_frees = map Free (alpha_names ~~ alpha_tys)

   198   val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)

   199 

   200   val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)

   201   val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns

   202   val alpha_bn_names = map (prefix "alpha_") bn_names

   203   val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys

   204   val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys

   205   val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)

   206   val alpha_bn_map = bns ~~ alpha_bn_frees

   207 

   208   val constrs_info = all_dtyp_constrs_types descr sorts

   209 

   210   val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss 

   211   val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info

   212 

   213   val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))

   214     (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)

   215   val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)

   216   

   217   val (alphas, lthy') = Inductive.add_inductive_i

   218      {quiet_mode = true, verbose = false, alt_name = Binding.empty,

   219       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}

   220      all_alpha_names [] all_alpha_intros [] lthy

   221 

   222   val alpha_trms_loc = #preds alphas;

   223   val alpha_induct_loc = #raw_induct alphas;

   224   val alpha_intros_loc = #intrs alphas;

   225   val alpha_cases_loc = #elims alphas;

   226   val phi = ProofContext.export_morphism lthy' lthy;

   227 

   228   val alpha_trms = map (Morphism.term phi) alpha_trms_loc;

   229   val alpha_induct = Morphism.thm phi alpha_induct_loc;

   230   val alpha_intros = map (Morphism.thm phi) alpha_intros_loc

   231   val alpha_cases = map (Morphism.thm phi) alpha_cases_loc

   232 in

   233   (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')

   234 end

   235 

   236 end (* structure *)

   237