src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35446 b719dad322fa
parent 35444 73f645fdd4ff
child 35448 f9f73f0475eb
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Feb 24 17:37:59 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Feb 25 13:16:28 2010 -0800
     1.3 @@ -161,6 +161,7 @@
     1.4    val axs_dis_def = map (get_def dis_name) cons;
     1.5    val axs_mat_def = map (get_def mat_name) cons;
     1.6    val axs_pat_def = map (get_def pat_name) cons;
     1.7 +(*
     1.8    val axs_sel_def =
     1.9      let
    1.10        fun def_of_sel sel = ga (sel^"_def") dname;
    1.11 @@ -169,6 +170,7 @@
    1.12      in
    1.13        maps defs_of_con cons
    1.14      end;
    1.15 +*)
    1.16    val ax_copy_def = ga "copy_def" dname;
    1.17  end; (* local *)
    1.18  
    1.19 @@ -196,6 +198,7 @@
    1.20      (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
    1.21  
    1.22  val axs_con_def = #con_defs result;
    1.23 +val sel_rews = #sel_rews result;
    1.24  
    1.25  (* ----- theorems concerning the isomorphism -------------------------------- *)
    1.26  
    1.27 @@ -472,79 +475,6 @@
    1.28    val con_compacts = map con_compact cons;
    1.29  end;
    1.30  
    1.31 -local
    1.32 -  fun one_sel sel =
    1.33 -    pg axs_sel_def (mk_trp (strict (%%:sel)))
    1.34 -      (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
    1.35 -
    1.36 -  fun sel_strict (_, _, args) =
    1.37 -    map_filter (Option.map one_sel o sel_of) args;
    1.38 -in
    1.39 -  val _ = trace " Proving sel_stricts...";
    1.40 -  val sel_stricts = maps sel_strict cons;
    1.41 -end;
    1.42 -
    1.43 -local
    1.44 -  fun sel_app_same c n sel (con, args) =
    1.45 -    let
    1.46 -      val nlas = nonlazy args;
    1.47 -      val vns = map vname args;
    1.48 -      val vnn = List.nth (vns, n);
    1.49 -      val nlas' = filter (fn v => v <> vnn) nlas;
    1.50 -      val lhs = (%%:sel)`(con_app con args);
    1.51 -      val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
    1.52 -      fun tacs1 ctxt =
    1.53 -        if vnn mem nlas
    1.54 -                        (* FIXME! case_UU_tac *)
    1.55 -        then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
    1.56 -        else [];
    1.57 -      val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.58 -    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    1.59 -
    1.60 -  fun sel_app_diff c n sel (con, args) =
    1.61 -    let
    1.62 -      val nlas = nonlazy args;
    1.63 -      val goal = mk_trp (%%:sel ` con_app con args === UU);
    1.64 -                        (* FIXME! case_UU_tac *)
    1.65 -      fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
    1.66 -      val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.67 -    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    1.68 -
    1.69 -  fun sel_app c n sel (con, _, args) =
    1.70 -    if con = c
    1.71 -    then sel_app_same c n sel (con, args)
    1.72 -    else sel_app_diff c n sel (con, args);
    1.73 -
    1.74 -  fun one_sel c n sel = map (sel_app c n sel) cons;
    1.75 -  fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
    1.76 -  fun one_con (c, _, args) =
    1.77 -    flat (map_filter I (mapn (one_sel' c) 0 args));
    1.78 -in
    1.79 -  val _ = trace " Proving sel_apps...";
    1.80 -  val sel_apps = maps one_con cons;
    1.81 -end;
    1.82 -
    1.83 -local
    1.84 -  fun sel_defin sel =
    1.85 -    let
    1.86 -      val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
    1.87 -      val tacs = [
    1.88 -        rtac casedist 1,
    1.89 -        contr_tac 1,
    1.90 -        DETERM_UNTIL_SOLVED (CHANGED
    1.91 -          (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
    1.92 -    in pg [] goal (K tacs) end;
    1.93 -in
    1.94 -  val _ = trace " Proving sel_defins...";
    1.95 -  val sel_defins =
    1.96 -    if length cons = 1
    1.97 -    then map_filter (fn arg => Option.map sel_defin (sel_of arg))
    1.98 -                 (filter_out is_lazy (third (hd cons)))
    1.99 -    else [];
   1.100 -end;
   1.101 -
   1.102 -val sel_rews = sel_stricts @ sel_defins @ sel_apps;
   1.103 -
   1.104  val _ = trace " Proving dist_les...";
   1.105  val dist_les =
   1.106    let