Domain package generates match functions for new datatypes, for use with the fixrec package
authorhuffman
Sat Jun 04 00:24:33 2005 +0200 (2005-06-04)
changeset 1622457094b83774e
parent 16223 84a177eeb49c
child 16225 ac993c5998e2
Domain package generates match functions for new datatypes, for use with the fixrec package
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/axioms.ML	Sat Jun 04 00:23:40 2005 +0200
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Sat Jun 04 00:24:33 2005 +0200
     1.3 @@ -61,6 +61,13 @@
     1.4  			   (if con'=con then %%:"TT" else %%:"FF") args)) cons))
     1.5  	in map ddef cons end;
     1.6  
     1.7 +  val mat_defs = let
     1.8 +	fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == 
     1.9 +		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.10 +			(fn (con',args) => (foldr /\#
    1.11 +			   (if con'=con then (%%:"return")`(mk_ctuple (map (bound_arg args) args)) else %%:"fail") args)) cons))
    1.12 +	in map mdef cons end;
    1.13 +
    1.14    val sel_defs = let
    1.15  	fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) == 
    1.16  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.17 @@ -81,7 +88,7 @@
    1.18  in (dnam,
    1.19      [abs_iso_ax, rep_iso_ax, reach_ax],
    1.20      [when_def, copy_def] @
    1.21 -     con_defs @ dis_defs @ sel_defs @
    1.22 +     con_defs @ dis_defs @ mat_defs @ sel_defs @
    1.23      [take_def, finite_def])
    1.24  end; (* let *)
    1.25  
     2.1 --- a/src/HOLCF/domain/library.ML	Sat Jun 04 00:23:40 2005 +0200
     2.2 +++ b/src/HOLCF/domain/library.ML	Sat Jun 04 00:24:33 2005 +0200
     2.3 @@ -56,6 +56,8 @@
     2.4  		   | _ => con;
     2.5  fun dis_name  con = "is_"^ (extern_name con);
     2.6  fun dis_name_ con = "is_"^ (strip_esc   con);
     2.7 +fun mat_name  con = "match_"^ (extern_name con);
     2.8 +fun mat_name_ con = "match_"^ (strip_esc   con);
     2.9  
    2.10  (* make distinct names out of the type list, 
    2.11     forbidding "o","n..","x..","f..","P.." as names *)
    2.12 @@ -174,6 +176,12 @@
    2.13  fun strict f = f`UU === UU;
    2.14  fun defined t = t ~= UU;
    2.15  fun cpair (S,T) = %%:"cpair"`S`T;
    2.16 +fun mk_ctuple [] = %%:"UU" (* used in match_defs *)
    2.17 +|   mk_ctuple (t::[]) = t
    2.18 +|   mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
    2.19 +fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
    2.20 +|   mk_ctupleT (T::[]) = T
    2.21 +|   mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts);
    2.22  fun lift_defined f = lift (fn x => defined (f x));
    2.23  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
    2.24  
     3.1 --- a/src/HOLCF/domain/syntax.ML	Sat Jun 04 00:23:40 2005 +0200
     3.2 +++ b/src/HOLCF/domain/syntax.ML	Sat Jun 04 00:24:33 2005 +0200
     3.3 @@ -47,10 +47,13 @@
     3.4  			(* stricly speaking, these constants have one argument,
     3.5  			   but the mixfix (without arguments) is introduced only
     3.6  			   to generate parse rules for non-alphanumeric names*)
     3.7 +  fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))),
     3.8 +			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
     3.9    fun sel (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
    3.10  in
    3.11    val consts_con = map con cons';
    3.12    val consts_dis = map dis cons';
    3.13 +  val consts_mat = map mat cons';
    3.14    val consts_sel = List.concat(map sel cons');
    3.15  end;
    3.16  
    3.17 @@ -87,7 +90,7 @@
    3.18  end;
    3.19  
    3.20  in ([const_rep, const_abs, const_when, const_copy] @ 
    3.21 -     consts_con @ consts_dis @ consts_sel @
    3.22 +     consts_con @ consts_dis @ consts_mat @ consts_sel @
    3.23      [const_take, const_finite],
    3.24      [case_trans])
    3.25  end; (* let *)
     4.1 --- a/src/HOLCF/domain/theorems.ML	Sat Jun 04 00:23:40 2005 +0200
     4.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jun 04 00:24:33 2005 +0200
     4.3 @@ -69,6 +69,7 @@
     4.4  val ax_when_def   = ga "when_def" dname;
     4.5  val axs_con_def   = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
     4.6  val axs_dis_def   = map (fn (con,_) => ga (   dis_name con^"_def") dname) cons;
     4.7 +val axs_mat_def   = map (fn (con,_) => ga (   mat_name con^"_def") dname) cons;
     4.8  val axs_sel_def   = List.concat(map (fn (_,args) => 
     4.9                      map (fn     arg => ga (sel_of arg     ^"_def") dname) args)
    4.10  									  cons);
    4.11 @@ -83,8 +84,8 @@
    4.12  val x_name = "x";
    4.13  
    4.14  val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
    4.15 -val abs_strict = iso_locale RS iso_abs_strict;
    4.16 -val rep_strict = iso_locale RS iso_rep_strict;
    4.17 +val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
    4.18 +val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    4.19  val abs_defin' = iso_locale RS iso_abs_defin';
    4.20  val rep_defin' = iso_locale RS iso_rep_defin';
    4.21  val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
    4.22 @@ -217,6 +218,18 @@
    4.23                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
    4.24  in dis_stricts @ dis_defins @ dis_apps end;
    4.25  
    4.26 +val mat_rews = let
    4.27 +  val mat_stricts = map (fn (con,_) => pg axs_mat_def (mk_trp(
    4.28 +                             strict(%%:(mat_name con)))) [
    4.29 +                                rtac when_strict 1]) cons;
    4.30 +  val mat_apps = let fun one_mat c (con,args)= pg axs_mat_def
    4.31 +                   (lift_defined %: (nonlazy args,
    4.32 +                        (mk_trp((%%:(mat_name c))`(con_app con args) ===
    4.33 +                              (if con=c then (%%:"return")`(mk_ctuple (map %# args)) else %%:"fail"))))) [
    4.34 +                                asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    4.35 +        in List.concat(map (fn (c,_) => map (one_mat c) cons) cons) end;
    4.36 +in mat_stricts @ mat_apps end;
    4.37 +
    4.38  val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
    4.39                          pg con_appls
    4.40                             (mk_trp(con_app2 con (fn arg => if vname arg = vn 
    4.41 @@ -263,7 +276,7 @@
    4.42                (lift_defined %: ((nonlazy args1),
    4.43                          (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
    4.44                          rtac rev_contrapos 1,
    4.45 -                        eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
    4.46 +                        eres_inst_tac[("f",dis_name con1)] monofun_cfun_arg 1]
    4.47                        @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
    4.48                        @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
    4.49      fun distinct (con1,args1) (con2,args2) =
    4.50 @@ -304,7 +317,7 @@
    4.51  val inverts = map (fn (con,args) => 
    4.52                  pgterm (op <<) con args (List.concat(map (fn arg => [
    4.53                                  TRY(rtac conjI 1),
    4.54 -                                dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
    4.55 +                                dres_inst_tac [("f",sel_of arg)] monofun_cfun_arg 1,
    4.56                                  asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
    4.57                                                        ) args))) cons';
    4.58  val injects = map (fn ((con,args),inv_thm) => 
    4.59 @@ -320,8 +333,7 @@
    4.60  (* ----- theorems concerning one induction step ----------------------------- *)
    4.61  
    4.62  val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
    4.63 -                   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
    4.64 -                                                   cfst_strict,csnd_strict]) 1];
    4.65 +                   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict]) 1];
    4.66  val copy_apps = map (fn (con,args) => pg [ax_copy_def]
    4.67                      (lift_defined %: (nonlazy_rec args,
    4.68                          mk_trp(dc_copy`%"f"`(con_app con args) ===
    4.69 @@ -333,7 +345,7 @@
    4.70                            simp_tac (HOLCF_ss addsimps con_appls) 1]))cons;
    4.71  val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
    4.72                                          (con_app con args) ===UU))
    4.73 -     (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
    4.74 +     (let val rews = copy_strict::copy_apps@con_rews
    4.75                           in map (case_UU_tac rews 1) (nonlazy args) @ [
    4.76                               asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
    4.77                          (List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
    4.78 @@ -347,6 +359,7 @@
    4.79  		("con_rews", con_rews),
    4.80  		("sel_rews", sel_rews),
    4.81  		("dis_rews", dis_rews),
    4.82 +		("match_rews", mat_rews),
    4.83  		("dist_les", dist_les),
    4.84  		("dist_eqs", dist_eqs),
    4.85  		("inverts" , inverts ),
    4.86 @@ -390,8 +403,7 @@
    4.87  (* ----- theorems concerning finite approximation and finite induction ------ *)
    4.88  
    4.89  local
    4.90 -  val iterate_Cprod_ss = simpset_of Fix.thy
    4.91 -                         addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
    4.92 +  val iterate_Cprod_ss = simpset_of Fix.thy;
    4.93    val copy_con_rews  = copy_rews @ con_rews;
    4.94    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
    4.95    val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>