Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/NewFv.thy
changeset 1965 4a3c05fe2bc5
parent 1963 0c9ef14e9ba4
child 1966 b6b3374a402d
equal deleted inserted replaced
1964:209ee65b2395 1965:4a3c05fe2bc5 
    10 |  BSet of ((term option * int) list) * (int list)
 
    10 |  BSet of ((term option * int) list) * (int list)
 
    11 |  BRes of ((term option * int) list) * (int list)
 
    11 |  BRes of ((term option * int) list) * (int list)
 
    12 *}
 
    12 *}
 
    13 
    13 
    14 ML {*
 
    14 ML {*
 
    15   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
 
    15 fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
 
    16 
    16 
    17   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
 
    17 val noatoms = @{term "{} :: atom set"};
 
    18 
    18 
    19   val noatoms = @{term "{} :: atom set"};
 
    19 fun mk_union sets =
 
    20   fun mk_union sets =
 
    20   fold (fn a => fn b =>
 
    21     fold (fn a => fn b =>
 
    21   if a = noatoms then b else
 
    22       if a = noatoms then b else
 
    22   if b = noatoms then a else
 
    23       if b = noatoms then a else
 
    23   if a = b then a else
 
    24       if a = b then a else
 
    24   HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
 
    25       HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
 
       
    26 *}
 
    25 *}
 
    27 
    26 
    28 ML {*
 
    27 ML {*
 
    29 fun is_atom thy ty =
 
    28 fun is_atom thy ty =
 
    30   Sign.of_sort thy (ty, @{sort at})
 
    29   Sign.of_sort thy (ty, @{sort at})
 
    64 fun atoms thy t =
 
    63 fun atoms thy t =
 
    65 let
 
    64 let
 
    66   val ty = fastype_of t;
 
    65   val ty = fastype_of t;
 
    67 in
 
    66 in
 
    68   if is_atom thy ty 
    67   if is_atom thy ty 
    69     then mk_single_atom t 
    68     then mk_singleton_atom t 
    70   else if is_atom_set thy ty 
    69   else if is_atom_set thy ty 
    71     then mk_atom_set t 
    70     then mk_atom_set t 
    72   else if is_atom_fset thy ty 
    71   else if is_atom_fset thy ty 
    73     then mk_atom_fset t 
    72     then mk_atom_fset t 
    74   else noatoms
 
    73   else noatoms
 
    88   fun fv_body i =
 
    87   fun fv_body i =
 
    89     let
 
    88     let
 
    90       val x = nth args i;
 
    89       val x = nth args i;
 
    91       val dt = nth dts i;
 
    90       val dt = nth dts i;
 
    92     in
 
    91     in
 
    93       if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
 
    92       if Datatype_Aux.is_rec_type dt 
       
    93       then nth fv_frees (Datatype_Aux.body_index dt) $ x 
       
    94       else atoms thy x
 
    94     end
 
    95     end
 
    95   val fv_bodys = mk_union (map fv_body bodys)
 
    96   val fv_bodys = mk_union (map fv_body bodys)
 
    96   val bound_vars =
 
    97   val bound_vars =
 
    97     case binds of
 
    98     case binds of
 
    98       [(SOME bn, i)] => setify (bn $ nth args i)
 
    99       [(SOME bn, i)] => setify (bn $ nth args i)
 
   116     let
 
   117     let
 
   117       val x = nth args i;
 
   118       val x = nth args i;
 
   118       val dt = nth dts i;
 
   119       val dt = nth dts i;
 
   119     in
 
   120     in
 
   120       case AList.lookup (op=) args_in_bn i of
 
   121       case AList.lookup (op=) args_in_bn i of
 
   121         NONE => if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
 
   122         NONE => if Datatype_Aux.is_rec_type dt 
       
   123                 then nth fv_frees (Datatype_Aux.body_index dt) $ x 
       
   124                 else atoms thy x
 
   122       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
 
   125       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
 
   123       | SOME NONE => noatoms
 
   126       | SOME NONE => noatoms
 
   124     end
 
   127     end
 
   125 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   128 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   126 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   129 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   130 ML {*
 
   133 ML {*
 
   131 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees
 
   134 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees
 
   132   bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
 
   135   bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
 
   133 let
 
   136 let
 
   134   val {descr, sorts, ...} = dt_info;
 
   137   val {descr, sorts, ...} = dt_info;
 
   135   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
       
   136   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
 
   138   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
 
   137   let
 
   139   let
 
   138     val Ts = map (typ_of_dtyp descr sorts) dts;
 
   140     val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
 
   139     val names = Datatype_Prop.make_tnames Ts;
 
   141     val names = Datatype_Prop.make_tnames Ts;
 
   140     val args = map Free (names ~~ Ts);
 
   142     val args = map Free (names ~~ Ts);
 
   141     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 
   143     val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp));
 
   142     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
 
   144     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
 
   143   in
 
   145   in
 
   144     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   146     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   145       (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
 
   147       (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
 
   146   end;
 
   148   end;
 
   174   BEmy i =>
 
   176   BEmy i =>
 
   175     let
 
   177     let
 
   176       val x = nth args i;
 
   178       val x = nth args i;
 
   177       val dt = nth dts i;
 
   179       val dt = nth dts i;
 
   178     in
 
   180     in
 
   179       if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
 
   181       if Datatype_Aux.is_rec_type dt 
       
   182       then nth fv_frees (Datatype_Aux.body_index dt) $ x 
       
   183       else atoms thy x
 
   180     end
 
   184     end
 
   181 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   185 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   182 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   186 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   183 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   187 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   184 *}
 
   188 *}
 
   185 
   189 
   186 ML {*
 
   190 ML {*
 
   187 fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
 
   191 fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
 
   188 let
 
   192 let
 
   189   val {descr, sorts, ...} = dt_info;
 
   193   val {descr, sorts, ...} = dt_info;
 
   190   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
       
   191   fun fv_constr (cname, dts) bml =
 
   194   fun fv_constr (cname, dts) bml =
 
   192   let
 
   195   let
 
   193     val Ts = map (typ_of_dtyp descr sorts) dts;
 
   196     val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
 
   194     val names = Datatype_Prop.make_tnames Ts;
 
   197     val names = Datatype_Prop.make_tnames Ts;
 
   195     val args = map Free (names ~~ Ts);
 
   198     val args = map Free (names ~~ Ts);
 
   196     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 
   199     val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp));
 
   197     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
 
   200     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
 
   198   in
 
   201   in
 
   199     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   202     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   200       (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
 
   203       (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
 
   201   end;
 
   204   end;
 
   214 fun termination_by method =
 
   217 fun termination_by method =
 
   215   Function.termination_proof NONE
 
   218   Function.termination_proof NONE
 
   216   #> Proof.global_terminal_proof (Method.Basic method, NONE)
 
   219   #> Proof.global_terminal_proof (Method.Basic method, NONE)
 
   217 *}
 
   220 *}
 
   218 
   221 
   219 
       
   220 
       
   221 ML {*
 
   222 ML {*
 
   222 fun define_raw_fv dt_info bns bmlll lthy =
 
   223 fun define_raw_fv dt_info bns bmlll lthy =
 
   223 let
 
   224 let
 
   224   val thy = ProofContext.theory_of lthy;
 
   225   val thy = ProofContext.theory_of lthy;
 
   225   val {descr, sorts, ...} = dt_info;
 
   226   val {descr, sorts, ...} = dt_info;
 
   226   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
   227 
   227   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
 
   228   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
 
   228     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
 
   229     "fv_" ^ Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)) descr);
 
   229   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
 
   230 
       
   231   val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr;
 
   230   val fv_frees = map Free (fv_names ~~ fv_types);
 
   232   val fv_frees = map Free (fv_names ~~ fv_types);
 
   231   val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll;
 
   233   val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll;
 
       
   234 
   232   val fvbns = map snd bn_fvbn;
 
   235   val fvbns = map snd bn_fvbn;
 
   233   val fv_nums = 0 upto (length fv_frees - 1)
 
   236   val fv_nums = 0 upto (length fv_frees - 1)
 
       
   237 
   234   val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums);
 
   238   val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums);
 
   235   val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
 
   239   val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
 
   236   val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)
 
   240   val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)
 
       
   241 
   237   val lthy' =
 
   242   val lthy' =
 
   238     lthy
 
   243     lthy
 
   239     |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config
 
   244     |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config
 
   240     |> by_pat_completeness_auto
 
   245     |> by_pat_completeness_auto
 
   241     |> Local_Theory.restore
 
   246     |> Local_Theory.restore
nominal2