--- a/src/HOLCF/Domain.thy Fri Feb 26 10:54:52 2010 -0800
+++ b/src/HOLCF/Domain.thy Sat Feb 27 08:30:11 2010 -0800
@@ -87,7 +87,10 @@
lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
-lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
+lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
+ by (simp add: rep_defined_iff)
+
+lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
proof (unfold compact_def)
assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
with cont_Rep_CFun2
@@ -249,10 +252,10 @@
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
-use "Tools/Domain/domain_constructors.ML"
use "Tools/Domain/domain_library.ML"
use "Tools/Domain/domain_syntax.ML"
use "Tools/Domain/domain_axioms.ML"
+use "Tools/Domain/domain_constructors.ML"
use "Tools/Domain/domain_theorems.ML"
use "Tools/Domain/domain_extender.ML"
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Feb 26 10:54:52 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 08:30:11 2010 -0800
@@ -15,6 +15,8 @@
-> theory
-> { con_consts : term list,
con_betas : thm list,
+ exhaust : thm,
+ casedist : thm,
con_compacts : thm list,
con_rews : thm list,
inverts : thm list,
@@ -43,7 +45,9 @@
val mk_snd = HOLogic.mk_snd;
val mk_not = HOLogic.mk_not;
val mk_conj = HOLogic.mk_conj;
+val mk_disj = HOLogic.mk_disj;
+fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
(*** Basic HOLCF concepts ***)
@@ -332,6 +336,9 @@
(* get theorems about rep and abs *)
val abs_strict = iso_locale RS @{thm iso.abs_strict};
+ (* get types of type isomorphism *)
+ val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const);
+
fun vars_of args =
let
val Ts = map snd args;
@@ -361,6 +368,53 @@
let fun one_con con (b, args, mx) = (con, args);
in map2 one_con con_consts spec end;
+ (* prove exhaustiveness of constructors *)
+ local
+ fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
+ | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}));
+ fun args2typ n [] = (n, oneT)
+ | args2typ n [arg] = arg2typ n arg
+ | args2typ n (arg::args) =
+ let
+ val (n1, t1) = arg2typ n arg;
+ val (n2, t2) = args2typ n1 args
+ in (n2, mk_sprodT (t1, t2)) end;
+ fun cons2typ n [] = (n, oneT)
+ | cons2typ n [con] = args2typ n (snd con)
+ | cons2typ n (con::cons) =
+ let
+ val (n1, t1) = args2typ n (snd con);
+ val (n2, t2) = cons2typ n1 cons
+ in (n2, mk_ssumT (t1, t2)) end;
+ val ct = ctyp_of thy (snd (cons2typ 1 spec'));
+ val thm1 = instantiate' [SOME ct] [] @{thm exh_start};
+ val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
+ val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
+
+ val x = Free ("x", lhsT);
+ fun one_con (con, args) =
+ let
+ val Ts = map snd args;
+ val ns = Name.variant_list ["x"] (Datatype_Prop.make_tnames Ts);
+ val vs = map Free (ns ~~ Ts);
+ val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
+ val eqn = mk_eq (x, list_ccomb (con, vs));
+ val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy);
+ in Library.foldr mk_ex (vs, conj) end;
+ val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec'));
+ (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+ val tacs = [
+ rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
+ rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
+ rtac thm3 1];
+ in
+ val exhaust = prove thy con_betas goal (K tacs);
+ val casedist =
+ (exhaust RS @{thm exh_casedist0})
+ |> rewrite_rule @{thms exh_casedists}
+ |> Drule.export_without_context;
+ end;
+
(* prove compactness rules for constructors *)
val con_compacts =
let
@@ -459,6 +513,8 @@
{
con_consts = con_consts,
con_betas = con_betas,
+ exhaust = exhaust,
+ casedist = casedist,
con_compacts = con_compacts,
con_rews = con_rews,
inverts = inverts,
@@ -631,8 +687,7 @@
val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
(* define constructor functions *)
- val ({con_consts, con_betas, con_compacts, con_rews, inverts, injects},
- thy) =
+ val (con_result, thy) =
let
fun prep_arg (lazy, sel, T) = (lazy, T);
fun prep_con (b, args, mx) = (b, map prep_arg args, mx);
@@ -640,6 +695,7 @@
in
add_constructors con_spec abs_const iso_locale thy
end;
+ val {con_consts, con_betas, ...} = con_result;
(* TODO: enable this earlier *)
val thy = Sign.add_path dname thy;
@@ -659,10 +715,12 @@
val result =
{ con_consts = con_consts,
con_betas = con_betas,
- con_compacts = con_compacts,
- con_rews = con_rews,
- inverts = inverts,
- injects = injects,
+ exhaust = #exhaust con_result,
+ casedist = #casedist con_result,
+ con_compacts = #con_compacts con_result,
+ con_rews = #con_rews con_result,
+ inverts = #inverts con_result,
+ injects = #injects con_result,
sel_rews = sel_thms };
in
(result, thy)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Feb 26 10:54:52 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 08:30:11 2010 -0800
@@ -198,11 +198,10 @@
(rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
val con_appls = #con_betas result;
-val con_compacts = #con_compacts result;
-val con_rews = #con_rews result;
-val sel_rews = #sel_rews result;
-val inverts = #inverts result;
-val injects = #injects result;
+val {exhaust, casedist, ...} = result;
+val {con_compacts, con_rews, inverts, injects, ...} = result;
+val {sel_rews, ...} = result;
+
(* ----- theorems concerning the isomorphism -------------------------------- *)
@@ -248,61 +247,6 @@
val _ = trace "Proving when_appl...";
val when_appl = appl_of_def ax_when_def;
-local
- fun arg2typ n arg =
- let val t = TVar (("'a", n), pcpoS)
- in (n + 1, if is_lazy arg then mk_uT t else t) end;
-
- fun args2typ n [] = (n, oneT)
- | args2typ n [arg] = arg2typ n arg
- | args2typ n (arg::args) =
- let
- val (n1, t1) = arg2typ n arg;
- val (n2, t2) = args2typ n1 args
- in (n2, mk_sprodT (t1, t2)) end;
-
- fun cons2typ n [] = (n,oneT)
- | cons2typ n [con] = args2typ n (third con)
- | cons2typ n (con::cons) =
- let
- val (n1, t1) = args2typ n (third con);
- val (n2, t2) = cons2typ n1 cons
- in (n2, mk_ssumT (t1, t2)) end;
-in
- fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
-end;
-
-local
- val iso_swap = iso_locale RS iso_iso_swap;
- fun one_con (con, _, args) =
- let
- val vns = Name.variant_list ["x"] (map vname args);
- val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
- val eqn = %:x_name === con_app2 con %: vns;
- val conj = foldr1 mk_conj (eqn :: map (defined o %:) nonlazy_vns);
- in Library.foldr mk_ex (vns, conj) end;
-
- val conj_assoc = @{thm conj_assoc};
- val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
- val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
- val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
- val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
-
- (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
- val tacs = [
- rtac disjE 1,
- etac (rep_defin' RS disjI1) 2,
- etac disjI2 2,
- rewrite_goals_tac [mk_meta_eq iso_swap],
- rtac thm3 1];
-in
- val _ = trace " Proving exhaust...";
- val exhaust = pg con_appls (mk_trp exh) (K tacs);
- val _ = trace " Proving casedist...";
- val casedist =
- Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
-end;
-
local
fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
fun bound_fun i _ = Bound (length cons - i);