1 theory NewFv

     2 imports "../Nominal-General/Nominal2_Atoms"

     3         "Abs" "Perm" "Nominal2_FSet"

     4 begin

     5 

     6 ML {*

     7 (* binding modes  and binding clauses *)

     8 

     9 datatype bmode = Lst | Res | Set

    10 

    11 datatype bclause =

    12   BC of bmode * (term option * int) list * int list

    13 *}

    14 

    15 ML {*

    16 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}

    17   | mk_diff (t1, @{term "{}::atom set"}) = t1

    18   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)

    19 

    20 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}

    21   | mk_union (t1 , @{term "{}::atom set"}) = t1

    22   | mk_union (@{term "{}::atom set"}, t2) = t2

    23   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  

    24  

    25 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}

    26 *}

    27 

    28 ML {*

    29 fun is_atom ctxt ty =

    30   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})

    31 

    32 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t

    33   | is_atom_set _ _ = false;

    34 

    35 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t

    36   | is_atom_fset _ _ = false;

    37 

    38 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t

    39   | is_atom_list _ _ = false

    40 *}

    41 

    42 ML {*

    43 fun mk_atom_set t =

    44 let

    45   val ty = fastype_of t;

    46   val atom_ty = HOLogic.dest_setT ty --> @{typ atom};

    47   val img_ty = atom_ty --> ty --> @{typ "atom set"};

    48 in

    49   (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)

    50 end;

    51 

    52 fun mk_atom_fset t =

    53 let

    54   val ty = fastype_of t;

    55   val atom_ty = dest_fsetT ty --> @{typ atom};

    56   val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};

    57   val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}

    58 in

    59   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)

    60 end;

    61 

    62 fun mk_atom_list t =

    63 let

    64   val ty = fastype_of t;

    65   val atom_ty = dest_listT ty --> @{typ atom};

    66   val map_ty = atom_ty --> ty --> @{typ "atom list"};

    67 in

    68   (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)

    69 end;

    70 *}

    71 

    72 ML {*

    73 fun setify ctxt t =

    74 let

    75   val ty = fastype_of t;

    76 in

    77   if is_atom ctxt ty

    78     then  HOLogic.mk_set @{typ atom} [mk_atom t]

    79   else if is_atom_set ctxt ty

    80     then mk_atom_set t

    81   else if is_atom_fset ctxt ty

    82     then mk_atom_fset t

    83   else error ("setify" ^ (PolyML.makestring (t, ty)))

    84 end

    85 *}

    86 

    87 ML {*

    88 fun listify ctxt t =

    89 let

    90   val ty = fastype_of t;

    91 in

    92   if is_atom ctxt ty

    93     then HOLogic.mk_list @{typ atom} [mk_atom t]

    94   else if is_atom_list ctxt ty

    95     then mk_atom_set t

    96   else error "listify"

    97 end

    98 *}

    99 

   100 ML {*

   101 fun to_set x =

   102   if fastype_of x = @{typ "atom list"}

   103   then @{term "set::atom list \<Rightarrow> atom set"} $ x

   104   else x

   105 *}

   106 

   107 ML {*

   108 fun make_body fv_map args i = 

   109 let

   110   val arg = nth args i

   111   val ty = fastype_of arg

   112 in

   113   case (AList.lookup (op=) fv_map ty) of

   114     NONE => mk_supp arg

   115   | SOME fv => fv $ arg

   116 end  

   117 *}

   118 

   119 ML {*

   120 fun make_binder lthy fv_bn_map args (bn_option, i) = 

   121 let

   122   val arg = nth args i

   123 in

   124   case bn_option of

   125     NONE => (setify lthy arg, @{term "{}::atom set"})

   126   | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)

   127 end  

   128 *}

   129 

   130 ML {*

   131 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =

   132 let

   133   val t1 = map (make_body fv_map args) bodies

   134   val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)

   135 in 

   136   fold_union (mk_diff (fold_union t1, fold_union t2)::t3)

   137 end

   138 *}

   139 

   140 ML {*

   141 fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 

   142 let

   143   val arg_names = Datatype_Prop.make_tnames arg_tys

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

   145   val fv = the (AList.lookup (op=) fv_map ty)

   146   val lhs = fv $ list_comb (constr, args)

   147   val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses

   148   val rhs = fold_union rhs_trms

   149 in

   150   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

   151 end

   152 *}

   153 

   154 ML {*

   155 fun make_bn_body fv_map fv_bn_map bn_args args i = 

   156 let

   157   val arg = nth args i

   158   val ty = fastype_of arg

   159 in

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

   161     NONE => (case (AList.lookup (op=) fv_map ty) of

   162               NONE => mk_supp arg

   163             | SOME fv => fv $ arg)

   164   | SOME (NONE) => @{term "{}::atom set"}

   165   | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg

   166 end  

   167 *}

   168 

   169 ML {*

   170 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =

   171   case bclause of

   172     BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)

   173   | BC (_, binders, bodies) => 

   174       let

   175         val t1 = map (make_body fv_map args) bodies

   176         val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)

   177       in 

   178         fold_union (mk_diff (fold_union t1, fold_union t2)::t3)

   179       end

   180 *}

   181 

   182 ML {*

   183 fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses =

   184 let

   185   val arg_names = Datatype_Prop.make_tnames arg_tys

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

   187   val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)

   188   val lhs = fv_bn $ list_comb (constr, args)

   189   val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses

   190   val rhs = fold_union rhs_trms

   191 in

   192   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

   193 end

   194 *}

   195 

   196 ML {*

   197 fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 

   198 let

   199   val nth_constrs_info = nth constrs_info bn_n

   200   val nth_bclausess = nth bclausesss bn_n

   201 in

   202   map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess

   203 end

   204 *}

   205 

   206 ML {*

   207 fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =

   208 let

   209 

   210   val fv_names = prefix_dt_names dt_descr sorts "fv_"

   211   val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;

   212   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;

   213   val fv_frees = map Free (fv_names ~~ fv_tys);

   214   val fv_map = fv_arg_tys ~~ fv_frees

   215 

   216   val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)

   217   val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)

   218   val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2

   219   val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2

   220   val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2

   221   val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2

   222   val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)

   223   val fv_bn_map2 = bns ~~ fv_bn_frees2

   224   val fv_bn_map3 = bns2 ~~ fv_bn_frees2

   225  

   226   val constrs_info = all_dtyp_constrs_types dt_descr sorts

   227 

   228   val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 

   229   val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2

   230   

   231   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)

   232   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)

   233 

   234   fun pat_completeness_auto lthy =

   235     Pat_Completeness.pat_completeness_tac lthy 1

   236       THEN auto_tac (clasimpset_of lthy)

   237 

   238   fun prove_termination lthy =

   239     Function.prove_termination NONE

   240       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy

   241 

   242   val (_, lthy') = Function.add_function all_fv_names all_fv_eqs

   243     Function_Common.default_config pat_completeness_auto lthy

   244 

   245   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')

   246 

   247   val {fs, simps, ...} = info;

   248 

   249   val morphism = ProofContext.export_morphism lthy'' lthy

   250   val fs_exp = map (Morphism.term morphism) fs

   251 

   252   val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp

   253   val simps_exp = Morphism.fact morphism (the simps)

   254 in

   255   (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')

   256 end

   257 *}

   258 

   259 

   260 

   261 

   262 

   263 end