2 imports "Abs" "Perm" "Nominal2_FSet"

     2 imports "Abs" "Perm"

     3 uses ("nominal_dt_rawperm.ML")

     4      ("nominal_dt_rawfuns.ML")

     7 use "nominal_dt_rawperm.ML"

     5 ML {*

     8 use "nominal_dt_rawfuns.ML"

     6 fun mk_prod_fv (t1, t2) =

     9 

     7 let

    10 ML {*

     8   val ty1 = fastype_of t1

    11 open Nominal_Dt_RawPerm

     9   val ty2 = fastype_of t2 

    12 open Nominal_Dt_RawFuns

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

    13 *}

    11 in

    14 

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

    15 

    13 end

    16 ML {*

    14 *}

    17 fun mk_binop2 ctxt s (l, r) =

    15 

    18   Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)

    16 ML {*

    19 *}

    17 fun mk_prod_alpha (t1, t2) =

    20 

    18 let

    21 ML {*

    19   val ty1 = fastype_of t1

    22 fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv})

    20   val ty2 = fastype_of t2 

    23 fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel})

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

    24 *}

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

    25 

    23 in

    26 ML {*

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

    27 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees

    25 end

    28   bn_alphabn alpha_const binds bodys =

    26 *}

    29 let

    27 

    30   fun bind_set args (NONE, no) = setify lthy (nth args no)

    28 ML {*

    31     | bind_set args (SOME f, no) = f $ (nth args no)

    29 fun mk_binders lthy bmode args bodies = 

    32   fun bind_lst args (NONE, no) = listify lthy (nth args no)

    30 let  

    33     | bind_lst args (SOME f, no) = f $ (nth args no)

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

    34   fun append (t1, t2) =

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

    35     Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2;

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

    36   fun binds_fn args nos =

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

    37     if alpha_const = @{const_name alpha_lst}

    35 

    38     then foldr1 append (map (bind_lst args) nos)

    36   val (connect_fn, bind_fn) =

    39     else fold_union (map (bind_set args) nos);

    37     case bmode of

    40   val lhs_binds = binds_fn args binds;

    38       Lst => (mk_append, bind_lst) 

    41   val rhs_binds = binds_fn args2 binds;

    39     | Set => (mk_union,  bind_set)

    42   val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);

    40     | Res => (mk_union,  bind_set)

    43   val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys);

    41 in

    44   val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys);

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

    45   val rhs = HOLogic.mk_prod (rhs_binds, rhs_bodys);

    43 end

    46   val body_dts = map (nth dts) bodys;

    44 *}

    47   fun fv_for_dt dt =

    45 

    48     if Datatype_Aux.is_rec_type dt

    46 ML {* 

    49     then nth fv_frees (Datatype_Aux.body_index dt)

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

    50     else Const (@{const_name supp},

    48 let

    51       Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"})

    49   val (alpha_name, binder_ty) = 

    52   val fvs = map fv_for_dt body_dts;

    50     case bmode of

    53   val fv = mk_compound_fv' lthy fvs;

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

    54   fun alpha_for_dt dt =

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

    55     if Datatype_Aux.is_rec_type dt

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

    56     then nth alpha_frees (Datatype_Aux.body_index dt)

    54   val ty = fastype_of args

    57     else Const (@{const_name "op ="},

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

    58       Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->

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

    59       Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool})

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

    60   val alphas = map alpha_for_dt body_dts;

    58 in

    61   val alpha = mk_compound_alpha' lthy alphas;

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

    62   val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs

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

    63   val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)

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

    64   val t = Syntax.check_term lthy alpha_gen_ex

    62 end

    65   fun alpha_bn_bind (SOME bn, i) =

    63 *}

    66       if member (op =) bodys i then NONE

    64 

    67       else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)

    65 ML {*

    68     | alpha_bn_bind (NONE, _) = NONE

    66 fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = 

    69 in

    67   case binder of

    70   t :: (map_filter alpha_bn_bind binds)

    68     (NONE, i) => []

    71 end

    69   | (SOME bn, i) =>

    72 *}

    70      if member (op=) bodies i

    73 

    71      then [] 

    74 ML {*

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

    75 fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm =

    73 *}

    76 case bm of

    74 

    77   BC (_, [], [i]) =>

    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       val arg = nth args i;

    80       val arg = nth args i

    80       val arg2 = nth args2 i;

    81       val arg' = nth args' i

    81       val dt = nth dts i;

    82       val ty = fastype_of arg

    83       case AList.lookup (op=) args_in_bn i of

    84       if nth is_rec i

    84         NONE => if Datatype_Aux.is_rec_type dt

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

    85                 then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]

    86       else HOLogic.mk_eq (arg, arg')

    86                 else [HOLogic.mk_eq (arg, arg2)]

    87       | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2]

    88       | SOME NONE => []

    90 | BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

    88   fun mk_alpha_fv i = 

    91     fv_frees bn_alphabn @{const_name alpha_lst} x y

    89     let

    92 | BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

    90       val ty = fastype_of (nth args i)

    93     fv_frees bn_alphabn @{const_name alpha_gen} x y

    91     in

    94 | BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

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

    95     fv_frees bn_alphabn @{const_name alpha_res} x y

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

    96 *}

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

    97 

    95     end

    98 

    96   

    99 ML {*

    97 in

   100 fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess

    98   case bclause of

   101   (alphabn, (_, ith_dtyp, args_in_bns)) =

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

   102 let

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

   103   fun alpha_bn_constr (cname, dts) (args_in_bn, bclauses) =

   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 = 

   105     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;

   138     val arg = nth args i

   106     val names = Datatype_Prop.make_tnames Ts;

   139     val arg' = nth args' i

   107     val names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts);

   140     val ty = fastype_of arg

   108     val args = map Free (names ~~ Ts);

   109     val args2 = map Free (names2 ~~ Ts);

   110     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));

   111     val alpha_bn_bm = alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees

   112       fv_frees bn_alphabn args_in_bn;

   113     val rhs = HOLogic.mk_Trueprop

   114       (alphabn $ (list_comb (c, args)) $ (list_comb (c, args2)));

   115     val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bn_bm bclauses))

   117     Library.foldr Logic.mk_implies (lhss, rhs)

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

   118   end;

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

   119   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;

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

   120 in

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

   121   map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess)

   146     | SOME (NONE) => []

   122 end

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

   123 *}

   148   end  

   124 

   149 in

   125 ML {*

   150   case bclause of

   126 fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss =

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

   127 let

   152       map HOLogic.mk_Trueprop 

   128   fun mk_alphabn_free (bn, ith, _) =

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

   129     let

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

   130       val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));

   155 end

   131       val ty = nth_dtyp dt_descr sorts ith;

   156 *}

   132       val alphabn_type = ty --> ty --> @{typ bool};

   157 

   133       val alphabn_free = Free(alphabn_name, alphabn_type);

   158 ML {*

   134     in

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

   135       (alphabn_name, alphabn_free)

   160 let

   136     end;

   161   val arg_names = Datatype_Prop.make_tnames arg_tys

   137   val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free bn_funs);

   162   val arg_names' = Name.variant_list arg_names arg_names

   138   val bn_alphabn = (map (fn (bn, _, _) => bn) bn_funs) ~~ alphabn_frees

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

   139   val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;

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

   140   val eqs = map2 (alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausessl

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

   141     (alphabn_frees ~~ bn_funs);

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

   142 in

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

   143   (bn_alphabn, alphabn_names, eqs)

   168 in

   144 end

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

   145 *}

   170 end

   146 

   171 *}

   147 ML {*

   172 

   148 fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =

   173 ML {*

   149 case bm of

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

   150   BC (_, [], [i]) =>

   175 let

   151     let

   176   val nth_constrs_info = nth constrs_info bn_n

   152       val arg = nth args i;

   177   val nth_bclausess = nth bclausesss bn_n

   153       val arg2 = nth args2 i;

   178 in

   154       val dt = nth dts i;

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

   155     in

   180 end

   156       if Datatype_Aux.is_rec_type dt

   181 *}

   157       then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]

   182 

   158       else [HOLogic.mk_eq (arg, arg2)]

   183 ML {*

   159     end

   184 fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy =

   160 | BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   185 let

   161     fv_frees bn_alphabn @{const_name alpha_lst} x y

   186   val alpha_names = prefix_dt_names descr sorts "alpha_"

   162 | BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   187   val alpha_arg_tys = all_dtyps descr sorts

   163     fv_frees bn_alphabn @{const_name alpha_gen} x y

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

   164 | BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

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

   165     fv_frees bn_alphabn @{const_name alpha_res} x y

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

   166 *}

   191 

   167 

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

   168 ML {*

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

   169 fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) =

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

   170 let

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

   171   fun alpha_constr (cname, dts) bclauses =

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

   172   let

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

   173     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;

   198   val alpha_bn_map = bns ~~ alpha_bn_frees

   174     val names = Datatype_Prop.make_tnames Ts;

   199 

   175     val names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts);

   200   val constrs_info = all_dtyp_constrs_types descr sorts

   176     val args = map Free (names ~~ Ts);

   201 

   177     val args2 = map Free (names2 ~~ Ts);

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

   178     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));

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

   179     val alpha_bm = alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn

   180     val rhs = HOLogic.mk_Trueprop

   181       (alpha_free $ (list_comb (c, args)) $ (list_comb (c, args2)));

   182     val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bm bclauses))

   183   in

   184     Library.foldr Logic.mk_implies (lhss, rhs)

   185   end;

   186   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;

   187 in

   188   map2 alpha_constr constrs bclausess

   189 end

   190 *}

   191 

   192 ML {*

   193 fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy =

   194 let

   195   val alpha_names = prefix_dt_names dt_descr sorts "alpha_";

   196   val alpha_types = map (fn (i, _) =>

   197     nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr;

   198   val alpha_frees = map Free (alpha_names ~~ alpha_types);

   199 

   200   val (bn_alphabn, alpha_bn_names, alpha_bn_eqs) =

   201     alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss

   202 

   203   val alpha_bns = map snd bn_alphabn;

   204   val alpha_bn_types = map fastype_of alpha_bns;

   205 

   206   val alpha_nums = 0 upto (length alpha_frees - 1)

   207 

   208   val alpha_eqs = map2 (alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausesss

   209     (alpha_frees ~~ alpha_nums);

   212     (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types)

   206     (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)

   213   val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs)

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

   214 

   208   

   218      all_alpha_names [] all_alpha_eqs [] lthy

   212      all_alpha_names [] all_alpha_intros [] lthy

   219 

   213 

   220   val alpha_ts_loc = #preds alphas;

   214   val alpha_trms_loc = #preds alphas;

   224   val morphism = ProofContext.export_morphism lthy' lthy;

   218   val phi = ProofContext.export_morphism lthy' lthy;

   225 

   219 

   226   val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;

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

   227   val alpha_induct = Morphism.thm morphism alpha_induct_loc;

   221   val alpha_induct = Morphism.thm phi alpha_induct_loc;

   228   val alpha_intros = Morphism.fact morphism alpha_intros_loc

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

   229   val alpha_cases = Morphism.fact morphism alpha_cases_loc

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

   230 in

   224 in

   231   (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy')

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

   232 end

   226 end

   233 handle UnequalLengths => error "Main"

   227 *}

   234 *}

   228 

   235 

   229 ML {* ProofContext.export_morphism *}

   236 end

   230 

   231 end