1 theory NewAlpha

     2 imports "Abs" "Perm"

     3 begin

     4 

     5 ML {*

     6 fun mk_prod_fv (t1, t2) =

     7 let

     8   val ty1 = fastype_of t1

     9   val ty2 = fastype_of t2 

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

    11 in

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

    13 end

    14 *}

    15 

    16 ML {*

    17 fun mk_prod_alpha (t1, t2) =

    18 let

    19   val ty1 = fastype_of t1

    20   val ty2 = fastype_of t2 

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

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

    23 in

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

    25 end

    26 *}

    27 

    28 ML {*

    29 fun mk_binders lthy bmode args bodies = 

    30 let  

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

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

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

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

    35 

    36   val (connect_fn, bind_fn) =

    37     case bmode of

    38       Lst => (mk_append, bind_lst) 

    39     | Set => (mk_union,  bind_set)

    40     | Res => (mk_union,  bind_set)

    41 in

    42   foldl1 connect_fn (map (bind_fn lthy args) bodies)

    43 end

    44 *}

    45 

    46 ML {* 

    47 fun mk_alpha_prem bmode fv alpha args args' binders binders' =

    48 let

    49   val (alpha_name, binder_ty) = 

    50     case bmode of

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

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

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

    54   val ty = fastype_of args

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

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

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

    58 in

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

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

    61       $ HOLogic.mk_prod (binders, args) $ alpha $ fv $ (Bound 0) $ HOLogic.mk_prod (binders', args'))

    62 end

    63 *}

    64 

    65 ML {*

    66 fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = 

    67   case binder of

    68     (NONE, i) => []

    69   | (SOME bn, i) =>

    70      if member (op=) bodies i

    71      then [] 

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

    73 *}

    74 

    75 ML {*

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

    77 let

    78   fun mk_frees i =

    79     let

    80       val arg = nth args i

    81       val arg' = nth args' i

    82       val ty = fastype_of arg

    83     in

    84       if nth is_rec i

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

    86       else HOLogic.mk_eq (arg, arg')

    87     end

    88   fun mk_alpha_fv i = 

    89     let

    90       val ty = fastype_of (nth args i)

    91     in

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

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

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

    95     end

    96   

    97 in

    98   case bclause of

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

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

   101     let

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

   103       val comp_fv = foldl1 mk_prod_fv fvs

   104       val comp_alpha = foldl1 mk_prod_alpha alphas

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

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

   107       val comp_binders = mk_binders lthy bmode args binders

   108       val comp_binders' = mk_binders lthy bmode args' binders

   109       val alpha_prem = 

   110         mk_alpha_prem bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'

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

   112     in

   113       map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)

   114     end

   115 end

   116 *}

   117 

   118 ML {*

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

   120 let

   121   val arg_names = Datatype_Prop.make_tnames arg_tys

   122   val arg_names' = Name.variant_list arg_names arg_names

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

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

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

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

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

   128 in

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

   130 end

   131 *}

   132 

   133 ML {*

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

   135 let

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

   137   let

   138     val arg = nth args i

   139     val arg' = nth args' i

   140     val ty = fastype_of arg

   141   in

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

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

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

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

   146     | SOME (NONE) => []

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

   148   end  

   149 in

   150   case bclause of

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

   152       map HOLogic.mk_Trueprop 

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

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

   155 end

   156 *}

   157 

   158 ML {*

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

   160 let

   161   val arg_names = Datatype_Prop.make_tnames arg_tys

   162   val arg_names' = Name.variant_list arg_names arg_names

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

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

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

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

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

   168 in

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

   170 end

   171 *}

   172 

   173 ML {*

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

   175 let

   176   val nth_constrs_info = nth constrs_info bn_n

   177   val nth_bclausess = nth bclausesss bn_n

   178 in

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

   180 end

   181 *}

   182 

   183 ML {*

   184 fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =

   185 let

   186   val alpha_names = prefix_dt_names descr sorts "alpha_"

   187   val alpha_arg_tys = all_dtyps descr sorts

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

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

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

   191 

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

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

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

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

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

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

   198   val alpha_bn_map = bns ~~ alpha_bn_frees

   199 

   200   val constrs_info = all_dtyp_constrs_types descr sorts

   201 

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

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

   204 

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

   206     (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)

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

   208   

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

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

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

   212      all_alpha_names [] all_alpha_intros [] lthy

   213 

   214   val alpha_trms_loc = #preds alphas;

   215   val alpha_induct_loc = #raw_induct alphas;

   216   val alpha_intros_loc = #intrs alphas;

   217   val alpha_cases_loc = #elims alphas;

   218   val phi = ProofContext.export_morphism lthy' lthy;

   219 

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

   221   val alpha_induct = Morphism.thm phi alpha_induct_loc;

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

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

   224 in

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

   226 end

   227 *}

   228 

   229 end