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/Fv.thy
changeset 1288 0203cd5cfd6c
parent 1277 6eacf60ce41d
child 1301 c145c380e195
equal deleted inserted replaced
1287:8557af71724e 1288:0203cd5cfd6c 
     1 theory Fv
 
     1 theory Fv
 
     2 imports "Nominal2_Atoms" "Abs"
 
     2 imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *)
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 (* Bindings are given as a list which has a length being equal
 
     5 (* Bindings are given as a list which has a length being equal
 
     6    to the length of the number of constructors.
 
     6    to the length of the number of constructors.
 
     7 
     7 
    52     (* TODO: This one is not implemented *)
 
    52     (* TODO: This one is not implemented *)
 
    53     For other arguments it should be an appropriate fv function stored
 
    53     For other arguments it should be an appropriate fv function stored
 
    54       in the database.
 
    54       in the database.
 
    55 *)
 
    55 *)
 
    56 
    56 
       
    57 (* TODO: should be const_name union *)
 
    57 ML {*
 
    58 ML {*
 
    58   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
 
    59   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
 
    59   (* TODO: It is the same as one in 'nominal_atoms' *)
 
    60   (* TODO: It is the same as one in 'nominal_atoms' *)
 
    60   fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
 
    61   fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
 
    61   val noatoms = @{term "{} :: atom set"};
 
    62   val noatoms = @{term "{} :: atom set"};
 
    62   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
 
    63   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
 
    63   fun mk_union sets =
 
    64   fun mk_union sets =
 
    64     fold (fn a => fn b =>
 
    65     fold (fn a => fn b =>
 
    65       if a = noatoms then b else
 
    66       if a = noatoms then b else
 
    66       if b = noatoms then a else
 
    67       if b = noatoms then a else
 
    67       HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms;
 
    68       HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms;
 
       
    69   fun mk_conjl props =
 
       
    70     fold (fn a => fn b =>
 
       
    71       if a = @{term True} then b else
 
       
    72       if b = @{term True} then a else
 
       
    73       HOLogic.mk_conj (a, b)) props @{term True};
 
    68   fun mk_diff a b =
 
    74   fun mk_diff a b =
 
    69     if b = noatoms then a else
 
    75     if b = noatoms then a else
 
    70     if b = a then noatoms else
 
    76     if b = a then noatoms else
 
    71     HOLogic.mk_binop @{const_name minus} (a, b);
 
    77     HOLogic.mk_binop @{const_name minus} (a, b);
 
    72   fun mk_atoms t =
 
    78   fun mk_atoms t =
 
    88     in c $ fst $ snd
 
    94     in c $ fst $ snd
 
    89     end;
 
    95     end;
 
    90 
    96 
    91 *}
 
    97 *}
 
    92 
    98 
       
    99 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
       
   100 
    93 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 
   101 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 
    94 ML {*
 
   102 ML {*
 
    95 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
 
   103 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
 
    96 let
 
   104 let
 
    97   val thy = ProofContext.theory_of lthy;
 
   105   val thy = ProofContext.theory_of lthy;
 
   103   val fv_frees = map Free (fv_names ~~ fv_types);
 
   111   val fv_frees = map Free (fv_names ~~ fv_types);
 
   104   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
 
   112   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
 
   105     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
 
   113     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
 
   106   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
 
   114   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
 
   107   val alpha_frees = map Free (alpha_names ~~ alpha_types);
 
   115   val alpha_frees = map Free (alpha_names ~~ alpha_types);
 
   108   fun fv_alpha_constr i (cname, dts) bindcs =
 
   116   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
 
   109     let
 
   117     let
 
   110       val Ts = map (typ_of_dtyp descr sorts) dts;
 
   118       val Ts = map (typ_of_dtyp descr sorts) dts;
 
   111       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
 
   119       val bindslen = length bindcs
 
       
   120       val pi_strs = replicate bindslen "pi"
 
       
   121       val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
 
       
   122       val bind_pis = bindcs ~~ pis;
 
       
   123       val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
 
   112       val args = map Free (names ~~ Ts);
 
   124       val args = map Free (names ~~ Ts);
 
   113       val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
 
   125       val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
 
   114       val args2 = map Free (names2 ~~ Ts);
 
   126       val args2 = map Free (names2 ~~ Ts);
 
   115       val c = Const (cname, Ts ---> (nth_dtyp i));
 
   127       val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 
   116       val fv_c = nth fv_frees i;
 
   128       val fv_c = nth fv_frees ith_dtyp;
 
   117       val alpha = nth alpha_frees i;
 
   129       val alpha = nth alpha_frees ith_dtyp;
 
   118       fun fv_bind args (NONE, i) =
 
   130       val arg_nos = 0 upto (length dts - 1)
 
       
   131       fun fv_bind args (NONE, i, _) =
 
   119             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
 
   132             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
 
   120             (* TODO we assume that all can be 'atomized' *)
 
   133             (* TODO we assume that all can be 'atomized' *)
 
   121             if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
 
   134             if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
 
   122             mk_single_atom (nth args i)
 
   135             mk_single_atom (nth args i)
 
   123         | fv_bind args (SOME f, i) = f $ (nth args i);
 
   136         | fv_bind args (SOME f, i, _) = f $ (nth args i);
 
   124       fun fv_arg ((dt, x), bindxs) =
 
   137       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
 
       
   138       fun fv_arg ((dt, x), arg_no) =
 
   125         let
 
   139         let
 
   126           val arg =
 
   140           val arg =
 
   127             if is_rec_type dt then nth fv_frees (body_index dt) $ x else
 
   141             if is_rec_type dt then nth fv_frees (body_index dt) $ x else
 
   128             (* TODO: we just assume everything can be 'atomized' *)
 
   142             (* TODO: we just assume everything can be 'atomized' *)
 
   129             if (is_funtype o fastype_of) x then mk_atoms x else
 
   143             if (is_funtype o fastype_of) x then mk_atoms x else
 
   130             HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
 
   144             HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x];
 
   131           val sub = mk_union (map (fv_bind args) bindxs)
 
   145           (* If i = j then we generate it only once *)
 
       
   146           val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
 
       
   147           val sub = fv_binds args relevant
 
   132         in
 
   148         in
 
   133           mk_diff arg sub
 
   149           mk_diff arg sub
 
   134         end;
 
   150         end;
 
   135       val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   151       val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   136         (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))
 
   152         (fv_c $ list_comb (c, args), mk_union (map fv_arg  (dts ~~ args ~~ arg_nos))))
 
   137       val alpha_rhs =
 
   153       val alpha_rhs =
 
   138         HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
 
   154         HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
 
   139       fun alpha_arg ((dt, bindxs), (arg, arg2)) =
 
   155       fun alpha_arg ((dt, arg_no), (arg, arg2)) =
 
   140         if bindxs = [] then (
 
   156         let
 
   141           if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
 
   157           val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis;
 
   142           else (HOLogic.mk_eq (arg, arg2)))
 
   158         in
 
   143         else
 
   159           if relevant = [] then (
 
   144           if is_rec_type dt then let
 
   160             if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
 
   145             (* THE HARD CASE *)
 
   161             else (HOLogic.mk_eq (arg, arg2)))
 
   146             val lhs_binds = mk_union (map (fv_bind args) bindxs);
 
   162           else
 
   147             val lhs = mk_pair (lhs_binds, arg);
 
   163             if is_rec_type dt then let
 
   148             val rhs_binds = mk_union (map (fv_bind args2) bindxs);
 
   164               (* THE HARD CASE *)
 
   149             val rhs = mk_pair (rhs_binds, arg2);
 
   165               val (rbinds, rpis) = split_list relevant
 
   150             val alpha = nth alpha_frees (body_index dt);
 
   166               val lhs_binds = fv_binds args rbinds
 
   151             val fv = nth fv_frees (body_index dt);
 
   167               val lhs = mk_pair (lhs_binds, arg);
 
   152             val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;
 
   168               val rhs_binds = fv_binds args2 rbinds;
 
   153             val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre
 
   169               val rhs = mk_pair (rhs_binds, arg2);
 
   154           in
 
   170               val alpha = nth alpha_frees (body_index dt);
 
   155             HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)
 
   171               val fv = nth fv_frees (body_index dt);
 
   156           (* TODO Add some test that is makes sense *)
 
   172               (* TODO: check that pis have empty intersection *)
 
   157           end else @{term "True"}
 
   173               val pi = foldr1 add_perm rpis;
 
   158       val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))
 
   174               val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
 
   159       val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)
 
   175             in
 
       
   176               Syntax.check_term lthy alpha_gen_pre
 
       
   177             (* TODO Add some test that is makes sense *)
 
       
   178             end else @{term "True"}
 
       
   179         end
 
       
   180       val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
 
       
   181       val alpha_lhss = mk_conjl alphas
 
       
   182       val alpha_lhss_ex =
 
       
   183         fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss
 
       
   184       val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs)
 
   160     in
 
   185     in
 
   161       (fv_eq, alpha_eq)
 
   186       (fv_eq, alpha_eq)
 
   162     end;
 
   187     end;
 
   163   fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
 
   188   fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
 
   164   val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
 
   189   val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
nominal2