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 1981 9f9c4965b608
parent 1971 8daf6ff5e11a
child 1983 4538d63ecc9b
equal deleted inserted replaced
1978:8feedc0d4ea8 1981:9f9c4965b608 
     1 theory NewFv
 
     1 theory NewFv
 
     2 imports "../Nominal-General/Nominal2_Atoms" 
     2 imports "../Nominal-General/Nominal2_Atoms"
 
     3         "Abs" "Perm" "Rsp" "Nominal2_FSet"
 
     3         "Abs" "Perm" "Nominal2_FSet"
 
     4 begin
 
     4 begin
 
     5 
     5 
     6 ML {*
 
     6 ML {*
 
     7 datatype bmodes =
 
     7 datatype bmodes =
 
     8    BEmy of int
 
     8    BEmy of int
 
    73   else noatoms
 
    73   else noatoms
 
    74 end
 
    74 end
 
    75 *}
 
    75 *}
 
    76 
    76 
    77 ML {*
 
    77 ML {*
 
       
    78 fun mk_supp t =
 
       
    79   Const (@{const_name supp}, fastype_of t --> @{typ "atom set"}) $ t
 
       
    80 *}
 
       
    81 
       
    82 ML {*
 
    78 fun setify x =
 
    83 fun setify x =
 
    79   if fastype_of x = @{typ "atom list"} 
    84   if fastype_of x = @{typ "atom list"} 
    80   then @{term "set::atom list \<Rightarrow> atom set"} $ x 
    85   then @{term "set::atom list \<Rightarrow> atom set"} $ x 
    81   else x
 
    86   else x
 
    82 *}
 
    87 *}
 
    87   fun fv_body i =
 
    92   fun fv_body i =
 
    88     let
 
    93     let
 
    89       val x = nth args i;
 
    94       val x = nth args i;
 
    90       val dt = nth dts i;
 
    95       val dt = nth dts i;
 
    91     in
 
    96     in
 
    92       if Datatype_Aux.is_rec_type dt 
    97       if Datatype_Aux.is_rec_type dt
 
    93       then nth fv_frees (Datatype_Aux.body_index dt) $ x 
    98       then nth fv_frees (Datatype_Aux.body_index dt) $ x
 
    94       else atoms thy x
 
    99       else mk_supp x
 
    95     end
 
   100     end
 
    96   val fv_bodys = mk_union (map fv_body bodys)
 
   101   val fv_bodys = mk_union (map fv_body bodys)
 
    97   val bound_vars =
 
   102   val bound_vars =
 
    98     case binds of
 
   103     case binds of
 
    99       [(SOME bn, i)] => setify (bn $ nth args i)
 
   104       [(SOME bn, i)] => setify (bn $ nth args i)
 
   117     let
 
   122     let
 
   118       val x = nth args i;
 
   123       val x = nth args i;
 
   119       val dt = nth dts i;
 
   124       val dt = nth dts i;
 
   120     in
 
   125     in
 
   121       case AList.lookup (op=) args_in_bn i of
 
   126       case AList.lookup (op=) args_in_bn i of
 
   122         NONE => if Datatype_Aux.is_rec_type dt 
   127         NONE => if Datatype_Aux.is_rec_type dt
 
   123                 then nth fv_frees (Datatype_Aux.body_index dt) $ x 
   128                 then nth fv_frees (Datatype_Aux.body_index dt) $ x
 
   124                 else atoms thy x
 
   129                 else mk_supp x
 
   125       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
 
   130       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
 
   126       | SOME NONE => noatoms
 
   131       | SOME NONE => noatoms
 
   127     end
 
   132     end
 
   128 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   133 | BLst (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
 
   134 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   130 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   135 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   131 *}
 
   136 *}
 
   132 
   137 
   133 ML {*
 
   138 ML {*
 
   134 fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
 
   139 fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) =
 
   135 let
 
   140 let
 
   136   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
 
   141   fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) =
 
   137   let
 
   142   let
 
   138     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
 
   143     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
 
   139     val names = Datatype_Prop.make_tnames Ts;
 
   144     val names = Datatype_Prop.make_tnames Ts;
 
   140     val args = map Free (names ~~ Ts);
 
   145     val args = map Free (names ~~ Ts);
 
   141     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
 
   146     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
 
   142     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
 
   147     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
 
   143   in
 
   148   in
 
   144     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   149     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   145       (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
 
   150       (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
 
   146   end;
 
   151   end;
 
   147   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 
   152   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 
   148 in
 
   153 in
 
   149   map2 fv_bn_constr constrs (args_in_bns ~~ bmll)
 
   154   map2 fv_bn_constr constrs (args_in_bns ~~ bclausess)
 
   150 end
 
   155 end
 
   151 *}
 
   156 *}
 
   152 
   157 
   153 ML {*
 
   158 ML {*
 
   154 fun fv_bns thy dt_descr sorts fv_frees bn_funs bclauses =
 
   159 fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss =
 
   155 let
 
   160 let
 
   156   fun mk_fvbn_free (bn, ith, _) =
 
   161   fun mk_fvbn_free (bn, ith, _) =
 
   157     let
 
   162     let
 
   158       val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
 
   163       val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
 
   159     in
 
   164     in
 
   160       (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
 
   165       (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
 
   161     end;
 
   166     end;
 
   162   val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
 
   167   val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
 
   163   val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
 
   168   val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
 
   164   val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs;
 
   169   val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
 
   165   val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs);
 
   170   val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs);
 
   166 in
 
   171 in
 
   167   (bn_fvbn, fvbn_names, eqs)
 
   172   (bn_fvbn, fvbn_names, eqs)
 
   168 end
 
   173 end
 
   169 *}
 
   174 *}
 
   170 
   175 
   174   BEmy i =>
 
   179   BEmy i =>
 
   175     let
 
   180     let
 
   176       val x = nth args i;
 
   181       val x = nth args i;
 
   177       val dt = nth dts i;
 
   182       val dt = nth dts i;
 
   178     in
 
   183     in
 
   179       if Datatype_Aux.is_rec_type dt 
   184       if Datatype_Aux.is_rec_type dt
 
   180       then nth fv_frees (Datatype_Aux.body_index dt) $ x 
   185       then nth fv_frees (Datatype_Aux.body_index dt) $ x
 
   181       else atoms thy x
 
   186       else mk_supp x
 
   182     end
 
   187     end
 
   183 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   188 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   184 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   189 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   185 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   190 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   186 *}
 
   191 *}
 
   187 
   192 
   188 ML {*
 
   193 ML {*
 
   189 fun fv thy dt_descr sorts fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
 
   194 fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) =
 
   190 let
 
   195 let
 
   191   fun fv_constr (cname, dts) bml =
 
   196   fun fv_constr (cname, dts) bclauses =
 
   192   let
 
   197   let
 
   193     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
 
   198     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
 
   194     val names = Datatype_Prop.make_tnames Ts;
 
   199     val names = Datatype_Prop.make_tnames Ts;
 
   195     val args = map Free (names ~~ Ts);
 
   200     val args = map Free (names ~~ Ts);
 
   196     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
 
   201     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
 
   197     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
 
   202     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
 
   198   in
 
   203   in
 
   199     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   204     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   200       (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
 
   205       (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
 
   201   end;
 
   206   end;
 
   202   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 
   207   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 
   203 in
 
   208 in
 
   204   map2 fv_constr constrs bmll
 
   209   map2 fv_constr constrs bclausess
 
   205 end
 
   210 end
 
   206 *}
 
   211 *}
 
   207 
   212 
   208 ML {*
 
   213 ML {*
 
   209 val by_pat_completeness_auto =
 
       
   210   Proof.global_terminal_proof
 
       
   211     (Method.Basic Pat_Completeness.pat_completeness,
 
       
   212      SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
       
   213 
       
   214 fun termination_by method =
 
       
   215   Function.termination_proof NONE
 
       
   216   #> Proof.global_terminal_proof (Method.Basic method, NONE)
 
       
   217 *}
 
   214 *}
 
   218 
   215 
   219 ML {*
 
   216 ML {*
 
   220 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclauses lthy =
 
   217 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclauses lthy =
 
   221 let
 
   218 let
 
   224 
   221 
   225   val fv_names = prefix_dt_names dt_descr sorts "fv_"
 
   222   val fv_names = prefix_dt_names dt_descr sorts "fv_"
 
   226   val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
 
   223   val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
 
   227   val fv_frees = map Free (fv_names ~~ fv_types);
 
   224   val fv_frees = map Free (fv_names ~~ fv_types);
 
   228 
   225 
   229   val (bn_fvbn, fv_bn_names, fv_bn_eqs) = 
   226   val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
 
   230     fv_bns thy dt_descr sorts fv_frees bn_funs bclauses;
 
   227     fv_bns thy dt_descr sorts fv_frees bn_funs bclauses;
 
   231 
   228 
   232   val fvbns = map snd bn_fvbn;
 
   229   val fvbns = map snd bn_fvbn;
 
   233   val fv_nums = 0 upto (length fv_frees - 1)
 
   230   val fv_nums = 0 upto (length fv_frees - 1)
 
   234 
   231 
   235   val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
 
   232   val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
 
   236   
   233 
   237   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
 
   234   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
 
   238   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
   235   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
   239 
   236 
   240   val lthy' =
 
   237   fun pat_completeness_auto ctxt =
 
   241     lthy
 
   238     Pat_Completeness.pat_completeness_tac ctxt 1
 
   242     |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config
 
   239       THEN auto_tac (clasimpset_of ctxt)
 
   243     |> by_pat_completeness_auto
 
   240 
   244     |> Local_Theory.restore
 
   241   fun prove_termination lthy =
 
   245     |> termination_by (Lexicographic_Order.lexicographic_order)
 
   242     Function.prove_termination NONE
 
   246 in
 
   243       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
   247   (fv_frees @ fvbns, lthy')
 
   244 
   248 end
 
   245   val (info, lthy') = Function.add_function all_fv_names all_fv_eqs
 
   249 *}
 
   246     Function_Common.default_config pat_completeness_auto lthy
 
   250 
   247 
   251 end
 
   248   val lthy'' = prove_termination (Local_Theory.restore lthy')
 
       
   249 in
 
       
   250   ((fv_frees, fvbns), info, lthy'')
 
       
   251 end
 
       
   252 *}
 
       
   253 
       
   254 end
nominal2