1 theory NewAlpha

     2 imports "NewFv"

     3 begin

     4 

     5 (* Given [fv1, fv2, fv3]

     6    produces %(x, y, z). fv1 x u fv2 y u fv3 z *)

     7 ML {*

     8 fun mk_compound_fv fvs =

     9 let

    10   val nos = (length fvs - 1) downto 0;

    11   val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);

    12   val fvs_union = mk_union fvs_applied;

    13   val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);

    14   fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))

    15 in

    16   fold fold_fun tys (Abs ("", tyh, fvs_union))

    17 end;

    18 *}

    19 

    20 (* Given [R1, R2, R3]

    21    produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)

    22 ML {*

    23 fun mk_compound_alpha Rs =

    24 let

    25   val nos = (length Rs - 1) downto 0;

    26   val nos2 = (2 * length Rs - 1) downto length Rs;

    27   val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)

    28     (Rs ~~ (nos2 ~~ nos));

    29   val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;

    30   val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);

    31   fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))

    32   val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))

    33 in

    34   fold fold_fun tys (Abs ("", tyh, abs_rhs))

    35 end;

    36 *}

    37 

    38 ML {*

    39 fun mk_pair (fst, snd) =

    40 let

    41   val ty1 = fastype_of fst

    42   val ty2 = fastype_of snd

    43   val c = HOLogic.pair_const ty1 ty2

    44 in

    45   c $ fst $ snd

    46 end;

    47 *}

    48 

    49 ML {*

    50 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees

    51   bn_alphabn alpha_const binds bodys =

    52 let

    53   val thy = ProofContext.theory_of lthy;

    54   fun bind_set args (NONE, no) = setify thy (nth args no)

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

    56   fun bind_lst args (NONE, no) = listify thy (nth args no)

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

    58   fun append (t1, t2) =

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

    60   fun binds_fn args nos =

    61     if alpha_const = @{const_name alpha_lst}

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

    63     else mk_union (map (bind_set args) nos);

    64   val lhs_binds = binds_fn args binds;

    65   val rhs_binds = binds_fn args2 binds;

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

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

    68   val lhs = mk_pair (lhs_binds, lhs_bodys);

    69   val rhs = mk_pair (rhs_binds, rhs_bodys);

    70   val body_dts = map (nth dts) bodys;

    71   fun fv_for_dt dt =

    72     if Datatype_Aux.is_rec_type dt

    73     then nth fv_frees (Datatype_Aux.body_index dt)

    74     else Const (@{const_name supp},

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

    76   val fvs = map fv_for_dt body_dts;

    77   val fv = mk_compound_fv fvs;

    78   fun alpha_for_dt dt =

    79     if Datatype_Aux.is_rec_type dt

    80     then nth alpha_frees (Datatype_Aux.body_index dt)

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

    82       Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->

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

    84   val alphas = map alpha_for_dt body_dts;

    85   val alpha = mk_compound_alpha alphas;

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

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

    88   val t = Syntax.check_term lthy alpha_gen_ex

    89 in

    90   case binds of

    91     [(SOME bn, i)] => if i mem bodys then [t]

    92       else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)]

    93     | _ => [t]

    94 end

    95 *}

    96 

    97 ML {*

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

    99 case bm of

   100   BEmy i =>

   101     let

   102       val arg = nth args i;

   103       val arg2 = nth args2 i;

   104       val dt = nth dts i;

   105     in

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

   107         NONE => if Datatype_Aux.is_rec_type dt

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

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

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

   111       | SOME NONE => []

   112     end

   113 | BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   114     fv_frees bn_alphabn @{const_name alpha_lst} x y

   115 | BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   116     fv_frees bn_alphabn @{const_name alpha_gen} x y

   117 | BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   118     fv_frees bn_alphabn @{const_name alpha_res} x y

   119 *}

   120 

   121 

   122 ML {*

   123 fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess

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

   125 let

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

   127   let

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

   129     val names = Datatype_Prop.make_tnames Ts;

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

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

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

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

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

   135       fv_frees bn_alphabn args_in_bn;

   136     val rhs = HOLogic.mk_Trueprop

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

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

   139   in

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

   141   end;

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

   143 in

   144   map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess)

   145 end

   146 *}

   147 

   148 ML {*

   149 fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss =

   150 let

   151   fun mk_alphabn_free (bn, ith, _) =

   152     let

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

   154       val ty = nth_dtyp dt_descr sorts ith;

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

   156       val alphabn_free = Free(alphabn_name, alphabn_type);

   157     in

   158       (alphabn_name, alphabn_free)

   159     end;

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

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

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

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

   164     (alphabn_frees ~~ bn_funs);

   165 in

   166   (bn_alphabn, alphabn_names, eqs)

   167 end

   168 *}

   169 

   170 ML {*

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

   172 case bm of

   173   BEmy i =>

   174     let

   175       val arg = nth args i;

   176       val arg2 = nth args2 i;

   177       val dt = nth dts i;

   178     in

   179       if Datatype_Aux.is_rec_type dt

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

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

   182     end

   183 | BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   184     fv_frees bn_alphabn @{const_name alpha_lst} x y

   185 | BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   186     fv_frees bn_alphabn @{const_name alpha_gen} x y

   187 | BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

   188     fv_frees bn_alphabn @{const_name alpha_res} x y

   189 *}

   190 

   191 ML {*

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

   193 let

   194   fun alpha_constr (cname, dts) bclauses =

   195   let

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

   197     val names = Datatype_Prop.make_tnames Ts;

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

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

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

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

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

   203     val rhs = HOLogic.mk_Trueprop

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

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

   206   in

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

   208   end;

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

   210 in

   211   map2 alpha_constr constrs bclausess

   212 end

   213 *}

   214 

   215 ML {*

   216 fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy =

   217 let

   218   val {descr as dt_descr, sorts, ...} = dt_info;

   219 

   220   val alpha_names = prefix_dt_names dt_descr sorts "alpha_";

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

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

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

   224 

   225   val (bn_alphabn, alpha_bn_names, alpha_bn_eqs) =

   226     alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss

   227 

   228   val alpha_bns = map snd bn_alphabn;

   229   val alpha_bn_types = map fastype_of alpha_bns;

   230 

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

   232 

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

   234     (alpha_frees ~~ alpha_nums);

   235 

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

   237     (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types)

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

   239 

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

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

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

   243      all_alpha_names [] all_alpha_eqs [] lthy

   244 in

   245   (alphas, lthy')

   246 end

   247 *}

   248 

   249 end