src/HOLCF/Tools/Domain/domain_axioms.ML
author haftmann
Tue Jul 21 16:14:56 2009 +0200 (2009-07-21)
changeset 32126 a5042f260440
parent 31738 src/HOLCF/Tools/domain/domain_axioms.ML@7b9b9ba532ca
child 32952 aeb1e44fbc19
permissions -rw-r--r--
obey captialized directory names convention
     1 (*  Title:      HOLCF/Tools/Domain/domain_axioms.ML
     2     Author:     David von Oheimb
     3 
     4 Syntax generator for domain command.
     5 *)
     6 
     7 signature DOMAIN_AXIOMS =
     8 sig
     9   val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
    10 
    11   val calc_axioms :
    12       string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
    13       string * (string * term) list * (string * term) list
    14 
    15   val add_axioms :
    16       bstring -> Domain_Library.eq list -> theory -> theory
    17 end;
    18 
    19 
    20 structure Domain_Axioms :> DOMAIN_AXIOMS =
    21 struct
    22 
    23 open Domain_Library;
    24 
    25 infixr 0 ===>;infixr 0 ==>;infix 0 == ; 
    26 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
    27 infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
    28 
    29 (* FIXME: use theory data for this *)
    30 val copy_tab : string Symtab.table =
    31     Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
    32                  (@{type_name "++"}, @{const_name "ssum_fun"}),
    33                  (@{type_name "**"}, @{const_name "sprod_fun"}),
    34                  (@{type_name "*"}, @{const_name "cprod_fun"}),
    35                  (@{type_name "u"}, @{const_name "u_fun"})];
    36 
    37 fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
    38 and copy r (DatatypeAux.DtRec i) = r i
    39   | copy r (DatatypeAux.DtTFree a) = ID
    40   | copy r (DatatypeAux.DtType (c, ds)) =
    41     case Symtab.lookup copy_tab c of
    42       SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
    43     | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
    44 
    45 fun calc_axioms
    46       (comp_dname : string)
    47       (eqs : eq list)
    48       (n : int)
    49       (eqn as ((dname,_),cons) : eq)
    50     : string * (string * term) list * (string * term) list =
    51     let
    52 
    53       (* ----- axioms and definitions concerning the isomorphism ------------------ *)
    54 
    55       val dc_abs = %%:(dname^"_abs");
    56       val dc_rep = %%:(dname^"_rep");
    57       val x_name'= "x";
    58       val x_name = idx_name eqs x_name' (n+1);
    59       val dnam = Long_Name.base_name dname;
    60 
    61       val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
    62       val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
    63 
    64       val when_def = ("when_def",%%:(dname^"_when") == 
    65                                 List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
    66                                                                                         Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
    67           
    68       val copy_def =
    69           let fun r i = cproj (Bound 0) eqs i;
    70           in ("copy_def", %%:(dname^"_copy") ==
    71                           /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
    72 
    73       (* -- definitions concerning the constructors, discriminators and selectors - *)
    74 
    75       fun con_def m n (_,args) = let
    76         fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
    77         fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
    78         fun inj y 1 _ = y
    79           | inj y _ 0 = mk_sinl y
    80           | inj y i j = mk_sinr (inj y (i-1) (j-1));
    81       in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
    82           
    83       val con_defs = mapn (fn n => fn (con,args) =>
    84                                       (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
    85           
    86       val dis_defs = let
    87         fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
    88                                                 list_ccomb(%%:(dname^"_when"),map 
    89                                                                                 (fn (con',args) => (List.foldr /\#
    90       (if con'=con then TT else FF) args)) cons))
    91       in map ddef cons end;
    92 
    93       val mat_defs =
    94           let
    95             fun mdef (con,_) =
    96                 let
    97                   val k = Bound 0
    98                   val x = Bound 1
    99                   fun one_con (con', args') =
   100                       if con'=con then k else List.foldr /\# mk_fail args'
   101                   val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
   102                   val rhs = /\ "x" (/\ "k" (w ` x))
   103                 in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
   104           in map mdef cons end;
   105 
   106       val pat_defs =
   107           let
   108             fun pdef (con,args) =
   109                 let
   110                   val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
   111                   val xs = map (bound_arg args) args;
   112                   val r = Bound (length args);
   113                   val rhs = case args of [] => mk_return HOLogic.unit
   114                                        | _ => mk_ctuple_pat ps ` mk_ctuple xs;
   115                   fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
   116                 in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
   117                                                     list_ccomb(%%:(dname^"_when"), map one_con cons))
   118                 end
   119           in map pdef cons end;
   120 
   121       val sel_defs = let
   122         fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
   123                                                               list_ccomb(%%:(dname^"_when"),map 
   124                                                                                               (fn (con',args) => if con'<>con then UU else
   125                                                                                                                  List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
   126       in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
   127 
   128 
   129       (* ----- axiom and definitions concerning induction ------------------------- *)
   130 
   131       val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
   132                                             `%x_name === %:x_name));
   133       val take_def =
   134           ("take_def",
   135            %%:(dname^"_take") ==
   136               mk_lam("n",cproj
   137                            (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
   138       val finite_def =
   139           ("finite_def",
   140            %%:(dname^"_finite") ==
   141               mk_lam(x_name,
   142                      mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
   143 
   144     in (dnam,
   145         [abs_iso_ax, rep_iso_ax, reach_ax],
   146         [when_def, copy_def] @
   147         con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
   148         [take_def, finite_def])
   149     end; (* let (calc_axioms) *)
   150 
   151 
   152 (* legacy type inference *)
   153 
   154 fun legacy_infer_term thy t =
   155     singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
   156 
   157 fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
   158 
   159 fun infer_props thy = map (apsnd (legacy_infer_prop thy));
   160 
   161 
   162 fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
   163 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
   164 
   165 fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
   166 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
   167 
   168 fun add_matchers (((dname,_),cons) : eq) thy =
   169     let
   170       val con_names = map fst cons;
   171       val mat_names = map mat_name con_names;
   172       fun qualify n = Sign.full_name thy (Binding.name n);
   173       val ms = map qualify con_names ~~ map qualify mat_names;
   174     in Fixrec.add_matchers ms thy end;
   175 
   176 fun add_axioms comp_dnam (eqs : eq list) thy' =
   177     let
   178       val comp_dname = Sign.full_bname thy' comp_dnam;
   179       val dnames = map (fst o fst) eqs;
   180       val x_name = idx_name dnames "x"; 
   181       fun copy_app dname = %%:(dname^"_copy")`Bound 0;
   182       val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
   183                                    /\ "f"(mk_ctuple (map copy_app dnames)));
   184 
   185       fun one_con (con,args) = let
   186         val nonrec_args = filter_out is_rec args;
   187         val    rec_args = List.filter     is_rec args;
   188         val    recs_cnt = length rec_args;
   189         val allargs     = nonrec_args @ rec_args
   190                           @ map (upd_vname (fn s=> s^"'")) rec_args;
   191         val allvns      = map vname allargs;
   192         fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg;
   193         val vns1        = map (vname_arg "" ) args;
   194         val vns2        = map (vname_arg "'") args;
   195         val allargs_cnt = length nonrec_args + 2*recs_cnt;
   196         val rec_idxs    = (recs_cnt-1) downto 0;
   197         val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
   198                                                (allargs~~((allargs_cnt-1) downto 0)));
   199         fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
   200                                 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
   201         val capps =
   202             List.foldr mk_conj
   203                        (mk_conj(
   204                         Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
   205                         Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
   206                        (mapn rel_app 1 rec_args);
   207       in List.foldr mk_ex
   208                     (Library.foldr mk_conj
   209                                    (map (defined o Bound) nonlazy_idxs,capps)) allvns
   210       end;
   211       fun one_comp n (_,cons) =
   212           mk_all(x_name(n+1),
   213                  mk_all(x_name(n+1)^"'",
   214                         mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
   215                                foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
   216                                                ::map one_con cons))));
   217       val bisim_def =
   218           ("bisim_def",
   219            %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
   220           
   221       fun add_one (thy,(dnam,axs,dfs)) =
   222           thy |> Sign.add_path dnam
   223               |> add_defs_infer dfs
   224               |> add_axioms_infer axs
   225               |> Sign.parent_path;
   226 
   227       val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
   228 
   229     in thy |> Sign.add_path comp_dnam  
   230            |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
   231            |> Sign.parent_path
   232            |> fold add_matchers eqs
   233     end; (* let (add_axioms) *)
   234 
   235 end; (* struct *)