--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sun Feb 28 20:56:28 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Mon Mar 01 07:35:14 2010 -0800
@@ -817,23 +817,27 @@
(thy : theory) =
let
+ (* utility functions *)
+ fun mk_pair_pat (p1, p2) =
+ let
+ val T1 = fastype_of p1;
+ val T2 = fastype_of p2;
+ val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
+ val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
+ val pat_typ = [T1, T2] --->
+ (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
+ val pat_const = Const (@{const_name cpair_pat}, pat_typ);
+ in
+ pat_const $ p1 $ p2
+ end;
+ fun mk_tuple_pat [] = return_const HOLogic.unitT
+ | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
+ fun branch_const (T,U,V) =
+ Const (@{const_name branch},
+ (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
+
(* define pattern combinators *)
local
- fun mk_pair_pat (p1, p2) =
- let
- val T1 = fastype_of p1;
- val T2 = fastype_of p2;
- val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
- val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
- val pat_typ = [T1, T2] --->
- (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
- val pat_const = Const (@{const_name cpair_pat}, pat_typ);
- in
- pat_const $ p1 $ p2
- end;
- fun mk_tuple_pat [] = return_const HOLogic.unitT
- | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
-
val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
@@ -841,7 +845,7 @@
val pat_bind = Binding.suffix_name "_pat" bind;
val Ts = map snd args;
val Vs =
- (map (K "t") args)
+ (map (K "'t") args)
|> Datatype_Prop.indexify_names
|> Name.variant_list tns
|> map (fn t => TFree (t, @{sort pcpo}));
@@ -902,8 +906,63 @@
val thy = Sign.add_trrules_i trans_rules thy;
end;
+ (* prove strictness and reduction rules of pattern combinators *)
+ local
+ val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val rn = Name.variant tns "'r";
+ val R = TFree (rn, @{sort pcpo});
+ fun pat_lhs (pat, args) =
+ let
+ val Ts = map snd args;
+ val Vs =
+ (map (K "'t") args)
+ |> Datatype_Prop.indexify_names
+ |> Name.variant_list (rn::tns)
+ |> map (fn t => TFree (t, @{sort pcpo}));
+ val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
+ val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
+ val pats = map Free (patNs ~~ patTs);
+ val k = Free ("rhs", mk_tupleT Vs ->> R);
+ val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
+ val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
+ val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
+ val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
+ val taken = "rhs" :: patNs;
+ in (fun1, fun2, taken) end;
+ fun pat_strict (pat, (con, args)) =
+ let
+ val (fun1, fun2, taken) = pat_lhs (pat, args);
+ val defs = @{thm branch_def} :: pat_defs;
+ val goal = mk_trp (mk_strict fun1);
+ val rules = @{thm Fixrec.bind_strict} :: case_rews;
+ val tacs = [simp_tac (beta_ss addsimps rules) 1];
+ in prove thy defs goal (K tacs) end;
+ fun pat_apps (i, (pat, (con, args))) =
+ let
+ val (fun1, fun2, taken) = pat_lhs (pat, args);
+ fun pat_app (j, (con', args')) =
+ let
+ val Ts = map snd args';
+ val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts);
+ val vs = map Free (ns ~~ Ts);
+ val con_app = list_ccomb (con', vs);
+ val nonlazy = map snd (filter_out (fst o fst) (args' ~~ vs));
+ val assms = map (mk_trp o mk_defined) nonlazy;
+ val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R;
+ val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
+ val goal = Logic.list_implies (assms, concl);
+ val defs = @{thm branch_def} :: pat_defs;
+ val rules = @{thms bind_fail left_unit} @ case_rews;
+ val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
+ in prove thy defs goal (K tacs) end;
+ in map_index pat_app spec end;
+ in
+ val pat_stricts = map pat_strict (pat_consts ~~ spec);
+ val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec));
+ end;
+
in
- (pat_defs, thy)
+ (pat_stricts @ pat_apps, thy)
end
(******************************************************************************)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Feb 28 20:56:28 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 01 07:35:14 2010 -0800
@@ -164,7 +164,7 @@
val when_strict = hd when_rews;
val dis_rews = #dis_rews result;
val mat_rews = #match_rews result;
-val axs_pat_def = #pat_rews result;
+val pat_rews = #pat_rews result;
(* ----- theorems concerning the isomorphism -------------------------------- *)
@@ -176,42 +176,6 @@
val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
-(* ----- theorems concerning the constructors, discriminators and selectors - *)
-
-local
- fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
-
- fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
-
- fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
- | pat_rhs (con,_,args) =
- (mk_branch (mk_ctuple_pat (ps args)))
- `(%:"rhs")`(mk_ctuple (map %# args));
-
- fun pat_strict c =
- let
- val axs = @{thm branch_def} :: axs_pat_def;
- val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
- val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs goal (K tacs) end;
-
- fun pat_app c (con, _, args) =
- let
- val axs = @{thm branch_def} :: axs_pat_def;
- val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
- val rhs = if con = first c then pat_rhs c else mk_fail;
- val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
- val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs goal (K tacs) end;
-
- val _ = trace " Proving pat_stricts...";
- val pat_stricts = map pat_strict cons;
- val _ = trace " Proving pat_apps...";
- val pat_apps = maps (fn c => map (pat_app c) cons) cons;
-in
- val pat_rews = pat_stricts @ pat_apps;
-end;
-
(* ----- theorems concerning one induction step ----------------------------- *)
val copy_strict =