src/HOLCF/domain/theorems.ML
changeset 16224 57094b83774e
parent 15742 64eae3513064
child 16321 ef32a42f4079
     1.1 --- a/src/HOLCF/domain/theorems.ML	Sat Jun 04 00:23:40 2005 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jun 04 00:24:33 2005 +0200
     1.3 @@ -69,6 +69,7 @@
     1.4  val ax_when_def   = ga "when_def" dname;
     1.5  val axs_con_def   = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
     1.6  val axs_dis_def   = map (fn (con,_) => ga (   dis_name con^"_def") dname) cons;
     1.7 +val axs_mat_def   = map (fn (con,_) => ga (   mat_name con^"_def") dname) cons;
     1.8  val axs_sel_def   = List.concat(map (fn (_,args) => 
     1.9                      map (fn     arg => ga (sel_of arg     ^"_def") dname) args)
    1.10  									  cons);
    1.11 @@ -83,8 +84,8 @@
    1.12  val x_name = "x";
    1.13  
    1.14  val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
    1.15 -val abs_strict = iso_locale RS iso_abs_strict;
    1.16 -val rep_strict = iso_locale RS iso_rep_strict;
    1.17 +val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
    1.18 +val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    1.19  val abs_defin' = iso_locale RS iso_abs_defin';
    1.20  val rep_defin' = iso_locale RS iso_rep_defin';
    1.21  val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
    1.22 @@ -217,6 +218,18 @@
    1.23                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
    1.24  in dis_stricts @ dis_defins @ dis_apps end;
    1.25  
    1.26 +val mat_rews = let
    1.27 +  val mat_stricts = map (fn (con,_) => pg axs_mat_def (mk_trp(
    1.28 +                             strict(%%:(mat_name con)))) [
    1.29 +                                rtac when_strict 1]) cons;
    1.30 +  val mat_apps = let fun one_mat c (con,args)= pg axs_mat_def
    1.31 +                   (lift_defined %: (nonlazy args,
    1.32 +                        (mk_trp((%%:(mat_name c))`(con_app con args) ===
    1.33 +                              (if con=c then (%%:"return")`(mk_ctuple (map %# args)) else %%:"fail"))))) [
    1.34 +                                asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.35 +        in List.concat(map (fn (c,_) => map (one_mat c) cons) cons) end;
    1.36 +in mat_stricts @ mat_apps end;
    1.37 +
    1.38  val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
    1.39                          pg con_appls
    1.40                             (mk_trp(con_app2 con (fn arg => if vname arg = vn 
    1.41 @@ -263,7 +276,7 @@
    1.42                (lift_defined %: ((nonlazy args1),
    1.43                          (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
    1.44                          rtac rev_contrapos 1,
    1.45 -                        eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
    1.46 +                        eres_inst_tac[("f",dis_name con1)] monofun_cfun_arg 1]
    1.47                        @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
    1.48                        @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
    1.49      fun distinct (con1,args1) (con2,args2) =
    1.50 @@ -304,7 +317,7 @@
    1.51  val inverts = map (fn (con,args) => 
    1.52                  pgterm (op <<) con args (List.concat(map (fn arg => [
    1.53                                  TRY(rtac conjI 1),
    1.54 -                                dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
    1.55 +                                dres_inst_tac [("f",sel_of arg)] monofun_cfun_arg 1,
    1.56                                  asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
    1.57                                                        ) args))) cons';
    1.58  val injects = map (fn ((con,args),inv_thm) => 
    1.59 @@ -320,8 +333,7 @@
    1.60  (* ----- theorems concerning one induction step ----------------------------- *)
    1.61  
    1.62  val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
    1.63 -                   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
    1.64 -                                                   cfst_strict,csnd_strict]) 1];
    1.65 +                   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict]) 1];
    1.66  val copy_apps = map (fn (con,args) => pg [ax_copy_def]
    1.67                      (lift_defined %: (nonlazy_rec args,
    1.68                          mk_trp(dc_copy`%"f"`(con_app con args) ===
    1.69 @@ -333,7 +345,7 @@
    1.70                            simp_tac (HOLCF_ss addsimps con_appls) 1]))cons;
    1.71  val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
    1.72                                          (con_app con args) ===UU))
    1.73 -     (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
    1.74 +     (let val rews = copy_strict::copy_apps@con_rews
    1.75                           in map (case_UU_tac rews 1) (nonlazy args) @ [
    1.76                               asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
    1.77                          (List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
    1.78 @@ -347,6 +359,7 @@
    1.79  		("con_rews", con_rews),
    1.80  		("sel_rews", sel_rews),
    1.81  		("dis_rews", dis_rews),
    1.82 +		("match_rews", mat_rews),
    1.83  		("dist_les", dist_les),
    1.84  		("dist_eqs", dist_eqs),
    1.85  		("inverts" , inverts ),
    1.86 @@ -390,8 +403,7 @@
    1.87  (* ----- theorems concerning finite approximation and finite induction ------ *)
    1.88  
    1.89  local
    1.90 -  val iterate_Cprod_ss = simpset_of Fix.thy
    1.91 -                         addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
    1.92 +  val iterate_Cprod_ss = simpset_of Fix.thy;
    1.93    val copy_con_rews  = copy_rews @ con_rews;
    1.94    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
    1.95    val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>