--- a/src/HOL/Divides.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Divides.thy Fri Nov 20 10:40:30 2009 +0100
@@ -2157,6 +2157,10 @@
lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
by (drule zdiv_mono1, auto)
+text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
+conditional upon the sign of @{text a} or @{text b}. There are many more.
+They should all be simp rules unless that causes too much search. *}
+
lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
apply auto
apply (drule_tac [2] zdiv_mono1)
@@ -2166,7 +2170,7 @@
done
lemma neg_imp_zdiv_nonneg_iff:
- "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
+ "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
apply (subst zdiv_zminus_zminus [symmetric])
apply (subst pos_imp_zdiv_nonneg_iff, auto)
done
@@ -2179,6 +2183,16 @@
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
+lemma nonneg1_imp_zdiv_pos_iff:
+ "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
+apply rule
+ apply rule
+ using div_pos_pos_trivial[of a b]apply arith
+ apply(cases "b=0")apply simp
+ using div_nonneg_neg_le0[of a b]apply arith
+using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
+done
+
subsubsection {* The Divides Relation *}
--- a/src/HOL/Library/SML_Quickcheck.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Library/SML_Quickcheck.thy Fri Nov 20 10:40:30 2009 +0100
@@ -6,6 +6,7 @@
begin
setup {*
+ InductiveCodegen.quickcheck_setup #>
Quickcheck.add_generator ("SML", Codegen.test_term)
*}
--- a/src/HOL/Nominal/Examples/ROOT.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML Fri Nov 20 10:40:30 2009 +0100
@@ -1,3 +1,3 @@
use_thys ["Nominal_Examples"];
-setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)
+setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"];
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Nov 20 10:40:30 2009 +0100
@@ -15,9 +15,9 @@
struct
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 20 10:40:30 2009 +0100
@@ -15,9 +15,9 @@
struct
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
--- a/src/HOL/Rational.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Rational.thy Fri Nov 20 10:40:30 2009 +0100
@@ -243,6 +243,160 @@
with Fract `q = Fract a b` `b \<noteq> 0` show C by auto
qed
+subsubsection {* Function @{text normalize} *}
+
+text{*
+Decompose a fraction into normalized, i.e. coprime numerator and denominator:
+*}
+
+definition normalize :: "rat \<Rightarrow> int \<times> int" where
+"normalize x \<equiv> THE pair. x = Fract (fst pair) (snd pair) &
+ snd pair > 0 & gcd (fst pair) (snd pair) = 1"
+
+declare normalize_def[code del]
+
+lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
+proof (cases "a = 0 | b = 0")
+ case True then show ?thesis by (auto simp add: eq_rat)
+next
+ let ?c = "gcd a b"
+ case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
+ then have "?c \<noteq> 0" by simp
+ then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
+ moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
+ by (simp add: semiring_div_class.mod_div_equality)
+ moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
+ moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
+ ultimately show ?thesis
+ by (simp add: mult_rat [symmetric])
+qed
+
+text{* Proof by Ren\'e Thiemann: *}
+lemma normalize_code[code]:
+"normalize (Fract a b) =
+ (if b > 0 then (let g = gcd a b in (a div g, b div g))
+ else if b = 0 then (0,1)
+ else (let g = - gcd a b in (a div g, b div g)))"
+proof -
+ let ?cond = "% r p. r = Fract (fst p) (snd p) & snd p > 0 &
+ gcd (fst p) (snd p) = 1"
+ show ?thesis
+ proof (cases "b = 0")
+ case True
+ thus ?thesis
+ proof (simp add: normalize_def)
+ show "(THE pair. ?cond (Fract a 0) pair) = (0,1)"
+ proof
+ show "?cond (Fract a 0) (0,1)"
+ by (simp add: rat_number_collapse)
+ next
+ fix pair
+ assume cond: "?cond (Fract a 0) pair"
+ show "pair = (0,1)"
+ proof (cases pair)
+ case (Pair den num)
+ with cond have num: "num > 0" by auto
+ with Pair cond have den: "den = 0" by (simp add: eq_rat)
+ show ?thesis
+ proof (cases "num = 1", simp add: Pair den)
+ case False
+ with num have gr: "num > 1" by auto
+ with den have "gcd den num = num" by auto
+ with Pair cond False gr show ?thesis by auto
+ qed
+ qed
+ qed
+ qed
+ next
+ { fix a b :: int assume b: "b > 0"
+ hence b0: "b \<noteq> 0" and "b >= 0" by auto
+ let ?g = "gcd a b"
+ from b0 have g0: "?g \<noteq> 0" by auto
+ then have gp: "?g > 0" by simp
+ then have gs: "?g <= b" by (metis b gcd_le2_int)
+ from gcd_dvd1_int[of a b] obtain a' where a': "a = ?g * a'"
+ unfolding dvd_def by auto
+ from gcd_dvd2_int[of a b] obtain b' where b': "b = ?g * b'"
+ unfolding dvd_def by auto
+ hence b'2: "b' * ?g = b" by (simp add: ring_simps)
+ with b0 have b'0: "b' \<noteq> 0" by auto
+ from b b' zero_less_mult_iff[of ?g b'] gp have b'p: "b' > 0" by arith
+ have "normalize (Fract a b) = (a div ?g, b div ?g)"
+ proof (simp add: normalize_def)
+ show "(THE pair. ?cond (Fract a b) pair) = (a div ?g, b div ?g)"
+ proof
+ have "1 = b div b" using b0 by auto
+ also have "\<dots> <= b div ?g" by (rule zdiv_mono2[OF `b >= 0` gp gs])
+ finally have div0: "b div ?g > 0" by simp
+ show "?cond (Fract a b) (a div ?g, b div ?g)"
+ by (simp add: b0 Fract_norm div_gcd_coprime_int div0)
+ next
+ fix pair assume cond: "?cond (Fract a b) pair"
+ show "pair = (a div ?g, b div ?g)"
+ proof (cases pair)
+ case (Pair den num)
+ with cond
+ have num: "num > 0" and num0: "num \<noteq> 0" and gcd: "gcd den num = 1"
+ by auto
+ obtain g where g: "g = ?g" by auto
+ with gp have gg0: "g > 0" by auto
+ from cond Pair eq_rat(1)[OF b0 num0]
+ have eq: "a * num = den * b" by auto
+ hence "a' * g * num = den * g * b'"
+ using a'[simplified g[symmetric]] b'[simplified g[symmetric]]
+ by simp
+ hence "a' * num * g = b' * den * g" by (simp add: algebra_simps)
+ hence eq2: "a' * num = b' * den" using gg0 by auto
+ have "a div ?g = ?g * a' div ?g" using a' by force
+ hence adiv: "a div ?g = a'" using g0 by auto
+ have "b div ?g = ?g * b' div ?g" using b' by force
+ hence bdiv: "b div ?g = b'" using g0 by auto
+ from div_gcd_coprime_int[of a b] b0
+ have "gcd (a div ?g) (b div ?g) = 1" by auto
+ with adiv bdiv have gcd2: "gcd a' b' = 1" by auto
+ from gcd have gcd3: "gcd num den = 1"
+ by (simp add: gcd_commute_int[of den num])
+ from gcd2 have gcd4: "gcd b' a' = 1"
+ by (simp add: gcd_commute_int[of a' b'])
+ have one: "num dvd b'"
+ by (metis coprime_dvd_mult_int[OF gcd3] dvd_triv_right eq2)
+ have two: "b' dvd num"
+ by (metis coprime_dvd_mult_int[OF gcd4] dvd_triv_left eq2 zmult_commute)
+ from zdvd_antisym_abs[OF one two] b'p num
+ have numb': "num = b'" by auto
+ with eq2 b'0 have "a' = den" by auto
+ with numb' adiv bdiv Pair show ?thesis by simp
+ qed
+ qed
+ qed
+ }
+ note main = this
+ assume "b \<noteq> 0"
+ hence "b > 0 | b < 0" by arith
+ thus ?thesis
+ proof
+ assume b: "b > 0" thus ?thesis by (simp add: Let_def main[OF b])
+ next
+ assume b: "b < 0"
+ thus ?thesis
+ by(simp add:main Let_def minus_rat_cancel[of a b, symmetric]
+ zdiv_zminus2 del:minus_rat_cancel)
+ qed
+ qed
+qed
+
+lemma normalize_id: "normalize (Fract a b) = (p,q) \<Longrightarrow> Fract p q = Fract a b"
+by(auto simp add: normalize_code Let_def Fract_norm dvd_div_neg rat_number_collapse
+ split:split_if_asm)
+
+lemma normalize_denom_pos: "normalize (Fract a b) = (p,q) \<Longrightarrow> q > 0"
+by(auto simp add: normalize_code Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff
+ split:split_if_asm)
+
+lemma normalize_coprime: "normalize (Fract a b) = (p,q) \<Longrightarrow> coprime p q"
+by(auto simp add: normalize_code Let_def dvd_div_neg div_gcd_coprime_int
+ split:split_if_asm)
+
subsubsection {* The field of rational numbers *}
@@ -851,22 +1005,6 @@
subsection {* Implementation of rational numbers as pairs of integers *}
-lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
-proof (cases "a = 0 \<or> b = 0")
- case True then show ?thesis by (auto simp add: eq_rat)
-next
- let ?c = "gcd a b"
- case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
- then have "?c \<noteq> 0" by simp
- then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
- moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
- by (simp add: semiring_div_class.mod_div_equality)
- moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
- moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
- ultimately show ?thesis
- by (simp add: mult_rat [symmetric])
-qed
-
definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
[simp, code del]: "Fract_norm a b = Fract a b"
--- a/src/HOL/Tools/dseq.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Tools/dseq.ML Fri Nov 20 10:40:30 2009 +0100
@@ -6,7 +6,7 @@
signature DSEQ =
sig
- type 'a seq = int -> 'a Seq.seq;
+ type 'a seq = int * int * int -> 'a Seq.seq;
val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
val map: ('a -> 'b) -> 'a seq -> 'b seq
val append: 'a seq -> 'a seq -> 'a seq
@@ -16,37 +16,42 @@
val guard: bool -> unit seq
val of_list: 'a list -> 'a seq
val list_of: 'a seq -> 'a list
- val pull: 'a seq -> ('a * 'a seq) option
+ val pull: 'a seq -> ('a * 'a Seq.seq) option
val hd: 'a seq -> 'a
+ val generator: (int -> 'a * 'b) -> 'a seq
end;
structure DSeq : DSEQ =
struct
-type 'a seq = int -> 'a Seq.seq;
+type 'a seq = int * int * int -> 'a Seq.seq;
-fun maps f s 0 = Seq.empty
- | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
+fun maps f s (0, _, _) = Seq.empty
+ | maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i - 1, j, k));
-fun map f s i = Seq.map f (s i);
+fun map f s p = Seq.map f (s p);
-fun append s1 s2 i = Seq.append (s1 i) (s2 i);
+fun append s1 s2 p = Seq.append (s1 p) (s2 p);
-fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
+fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p);
-fun single x i = Seq.single x;
+fun single x _ = Seq.single x;
-fun empty i = Seq.empty;
+fun empty _ = Seq.empty;
fun guard b = if b then single () else empty;
-fun of_list xs i = Seq.of_list xs;
+fun of_list xs _ = Seq.of_list xs;
-fun list_of s = Seq.list_of (s ~1);
+fun list_of s = Seq.list_of (s (~1, 0, 0));
+
+fun pull s = Seq.pull (s (~1, 0, 0));
-fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*)
+fun hd s = Seq.hd (s (~1, 0, 0));
-fun hd s = Seq.hd (s ~1);
+fun generator g (i, 0, k) = Seq.empty
+ | generator g (i, j, k) =
+ Seq.make (fn () => SOME (fst (g k), generator g (i, j-1, k)));
end;
--- a/src/HOL/Tools/inductive_codegen.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Nov 20 10:40:30 2009 +0100
@@ -7,7 +7,10 @@
signature INDUCTIVE_CODEGEN =
sig
val add : string option -> int option -> attribute
+ val test_fn : (int * int * int -> term list option) Unsynchronized.ref
+ val test_term: Proof.context -> term -> int -> term list option
val setup : theory -> theory
+ val quickcheck_setup : theory -> theory
end;
structure InductiveCodegen : INDUCTIVE_CODEGEN =
@@ -124,7 +127,8 @@
fun print_modes modes = message ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
- string_of_mode ms)) modes));
+ (fn (m, rnd) => string_of_mode m ^
+ (if rnd then " (random)" else "")) ms)) modes));
val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
val terms_vs = distinct (op =) o maps term_vs;
@@ -152,14 +156,17 @@
fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
-datatype mode = Mode of (int list option list * int list) * int list * mode option list;
+datatype mode = Mode of ((int list option list * int list) * bool) * int list * mode option list;
+
+fun needs_random (Mode ((_, b), _, ms)) =
+ b orelse exists (fn NONE => false | SOME m => needs_random m) ms;
fun modes_of modes t =
let
val ks = 1 upto length (binder_types (fastype_of t));
- val default = [Mode (([], ks), ks, [])];
+ val default = [Mode ((([], ks), false), ks, [])];
fun mk_modes name args = Option.map
- (maps (fn (m as (iss, is)) =>
+ (maps (fn (m as ((iss, is), _)) =>
let
val (args1, args2) =
if length args < length iss then
@@ -180,8 +187,8 @@
in (case strip_comb t of
(Const ("op =", Type (_, [T, _])), _) =>
- [Mode (([], [1]), [1], []), Mode (([], [2]), [2], [])] @
- (if is_eqT T then [Mode (([], [1, 2]), [1, 2], [])] else [])
+ [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
+ (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
| (Const (name, _), args) => the_default default (mk_modes name args)
| (Var ((name, _), _), args) => the (mk_modes name args)
| (Free (name, _), args) => the (mk_modes name args)
@@ -190,68 +197,101 @@
datatype indprem = Prem of term list * term * bool | Sidecond of term;
+fun missing_vars vs ts = subtract (fn (x, ((y, _), _)) => x = y) vs
+ (fold Term.add_vars ts []);
+
+fun monomorphic_vars vs = null (fold (Term.add_tvarsT o snd) vs []);
+
+fun mode_ord p = int_ord (pairself (fn (Mode ((_, rnd), _, _), vs) =>
+ length vs + (if null vs then 0 else 1) + (if rnd then 1 else 0)) p);
+
fun select_mode_prem thy modes vs ps =
- find_first (is_some o snd) (ps ~~ map
- (fn Prem (us, t, is_set) => find_first (fn Mode (_, is, _) =>
- let
- val (in_ts, out_ts) = get_args is 1 us;
- val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
- val vTs = maps term_vTs out_ts';
- val dupTs = map snd (duplicates (op =) vTs) @
- map_filter (AList.lookup (op =) vTs) vs;
- in
- subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
- forall (is_eqT o fastype_of) in_ts' andalso
- subset (op =) (term_vs t, vs) andalso
- forall is_eqT dupTs
- end)
- (if is_set then [Mode (([], []), [], [])]
- else modes_of modes t handle Option =>
- error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
- | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
- else NONE) ps);
+ sort (mode_ord o pairself (hd o snd))
+ (filter_out (null o snd) (ps ~~ map
+ (fn Prem (us, t, is_set) => sort mode_ord
+ (List.mapPartial (fn m as Mode (_, is, _) =>
+ let
+ val (in_ts, out_ts) = get_args is 1 us;
+ val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
+ val vTs = maps term_vTs out_ts';
+ val dupTs = map snd (duplicates (op =) vTs) @
+ map_filter (AList.lookup (op =) vTs) vs;
+ val missing_vs = missing_vars vs (t :: in_ts @ in_ts')
+ in
+ if forall (is_eqT o fastype_of) in_ts' andalso forall is_eqT dupTs
+ andalso monomorphic_vars missing_vs
+ then SOME (m, missing_vs)
+ else NONE
+ end)
+ (if is_set then [Mode ((([], []), false), [], [])]
+ else modes_of modes t handle Option =>
+ error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)))
+ | Sidecond t =>
+ let val missing_vs = missing_vars vs [t]
+ in
+ if monomorphic_vars missing_vs
+ then [(Mode ((([], []), false), [], []), missing_vs)]
+ else []
+ end)
+ ps));
-fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
+fun use_random () = "random_ind" mem !Codegen.mode;
+
+fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
let
val modes' = modes @ map_filter
- (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
+ (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
(arg_vs ~~ iss);
- fun check_mode_prems vs [] = SOME vs
- | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
- NONE => NONE
- | SOME (x, _) => check_mode_prems
+ fun check_mode_prems vs rnd [] = SOME (vs, rnd)
+ | check_mode_prems vs rnd ps = (case select_mode_prem thy modes' vs ps of
+ (x, (m, []) :: _) :: _ => check_mode_prems
(case x of Prem (us, _, _) => union (op =) vs (terms_vs us) | _ => vs)
- (filter_out (equal x) ps));
+ (rnd orelse needs_random m)
+ (filter_out (equal x) ps)
+ | (_, (_, vs') :: _) :: _ =>
+ if use_random () then
+ check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps
+ else NONE
+ | _ => NONE);
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
val in_vs = terms_vs in_ts;
- val concl_vs = terms_vs ts
in
- forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
- forall (is_eqT o fastype_of) in_ts' andalso
- (case check_mode_prems (union (op =) arg_vs in_vs) ps of
- NONE => false
- | SOME vs => subset (op =) (concl_vs, vs))
+ if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
+ forall (is_eqT o fastype_of) in_ts'
+ then (case check_mode_prems (union (op =) arg_vs in_vs) rnd ps of
+ NONE => NONE
+ | SOME (vs, rnd') =>
+ let val missing_vs = missing_vars vs ts
+ in
+ if null missing_vs orelse
+ use_random () andalso monomorphic_vars missing_vs
+ then SOME (rnd' orelse not (null missing_vs))
+ else NONE
+ end)
+ else NONE
end;
fun check_modes_pred thy arg_vs preds modes (p, ms) =
let val SOME rs = AList.lookup (op =) preds p
- in (p, filter (fn m => case find_index
- (not o check_mode_clause thy arg_vs modes m) rs of
- ~1 => true
- | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m); false)) ms)
+ in (p, List.mapPartial (fn m as (m', _) =>
+ let val xs = map (check_mode_clause thy arg_vs modes m) rs
+ in case find_index is_none xs of
+ ~1 => SOME (m', exists (fn SOME b => b) xs)
+ | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
+ p ^ " violates mode " ^ string_of_mode m'); NONE)
+ end) ms)
end;
-fun fixp f (x : (string * (int list option list * int list) list) list) =
+fun fixp f (x : (string * ((int list option list * int list) * bool) list) list) =
let val y = f x
in if x = y then x else fixp f y end;
fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
- (map (fn (s, (ks, k)) => (s, cprod (cprods (map
+ (map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map
(fn NONE => [NONE]
| SOME k' => map SOME (subsets 1 k')) ks),
- subsets 1 k))) arities);
+ subsets 1 k)))) arities);
(**** code generation ****)
@@ -318,7 +358,7 @@
apfst single (invoke_codegen thy defs dep module brack t gr)
| compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
([str name], gr)
- | compile_expr thy defs dep module brack modes (SOME (Mode (mode, _, ms)), t) gr =
+ | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
(case strip_comb t of
(Const (name, _), args) =>
if name = @{const_name "op ="} orelse AList.defined op = modes name then
@@ -344,7 +384,7 @@
fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
let
val modes' = modes @ map_filter
- (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
+ (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
(arg_vs ~~ iss);
fun check_constrt t (names, eqs) =
@@ -371,24 +411,41 @@
val (out_ps', gr4) =
fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3;
val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
+ val vs' = distinct (op =) (flat (vs :: map term_vs out_ts'));
+ val missing_vs = missing_vars vs' out_ts;
+ val final_p = Pretty.block
+ [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]
in
- (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
- (Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
- (exists (not o is_exhaustive) out_ts'''), gr5)
+ if null missing_vs then
+ (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
+ final_p (exists (not o is_exhaustive) out_ts'''), gr5)
+ else
+ let
+ val (pat_p, gr6) = invoke_codegen thy defs dep module true
+ (HOLogic.mk_tuple (map Var missing_vs)) gr5;
+ val gen_p = mk_gen gr6 module true [] ""
+ (HOLogic.mk_tupleT (map snd missing_vs))
+ in
+ (compile_match (snd nvs) eq_ps' out_ps'
+ (Pretty.block [str "DSeq.generator ", gen_p,
+ str " :->", Pretty.brk 1,
+ compile_match [] eq_ps [pat_p] final_p false])
+ (exists (not o is_exhaustive) out_ts'''),
+ gr6)
+ end
end
| compile_prems out_ts vs names ps gr =
let
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
- val SOME (p, mode as SOME (Mode (_, js, _))) = select_mode_prem thy modes' vs' ps;
- val ps' = filter_out (equal p) ps;
val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr;
val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
in
- (case p of
- Prem (us, t, is_set) =>
+ (case hd (select_mode_prem thy modes' vs' ps) of
+ (p as Prem (us, t, is_set), (mode as Mode (_, js, _), []) :: _) =>
let
+ val ps' = filter_out (equal p) ps;
val (in_ts, out_ts''') = get_args js 1 us;
val (in_ps, gr2) = fold_map
(invoke_codegen thy defs dep module true) in_ts gr1;
@@ -398,7 +455,7 @@
(if null in_ps then [] else [Pretty.brk 1]) @
separate (Pretty.brk 1) in_ps)
(compile_expr thy defs dep module false modes
- (mode, t) gr2)
+ (SOME mode, t) gr2)
else
apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
str "of", str "Set", str "xs", str "=>", str "xs)"])
@@ -411,8 +468,9 @@
[str " :->", Pretty.brk 1, rest]))
(exists (not o is_exhaustive) out_ts''), gr4)
end
- | Sidecond t =>
+ | (p as Sidecond t, [(_, [])]) =>
let
+ val ps' = filter_out (equal p) ps;
val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1;
val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
in
@@ -420,6 +478,19 @@
(Pretty.block [str "?? ", side_p,
str " :->", Pretty.brk 1, rest])
(exists (not o is_exhaustive) out_ts''), gr3)
+ end
+ | (_, (_, missing_vs) :: _) =>
+ let
+ val T = HOLogic.mk_tupleT (map snd missing_vs);
+ val (_, gr2) = invoke_tycodegen thy defs dep module false T gr1;
+ val gen_p = mk_gen gr2 module true [] "" T;
+ val (rest, gr3) = compile_prems
+ [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2
+ in
+ (compile_match (snd nvs) eq_ps out_ps
+ (Pretty.block [str "DSeq.generator", Pretty.brk 1,
+ gen_p, str " :->", Pretty.brk 1, rest])
+ (exists (not o is_exhaustive) out_ts''), gr3)
end)
end;
@@ -450,7 +521,7 @@
fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
- fold_map (fn mode => fn (gr', prfx') => compile_pred thy defs
+ fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs
dep module prfx' all_vs arg_vs modes s cls mode gr')
(((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
in
@@ -460,7 +531,7 @@
(**** processing of introduction rules ****)
exception Modes of
- (string * (int list option list * int list) list) list *
+ (string * ((int list option list * int list) * bool) list) list *
(string * (int option list * int)) list;
fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip
@@ -480,7 +551,7 @@
(s,
case AList.lookup (op =) cs (s : string) of
NONE => xs
- | SOME xs' => inter (op =) xs' xs) :: constrain cs ys;
+ | SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys;
fun mk_extra_defs thy defs gr dep names module ts =
fold (fn name => fn gr =>
@@ -573,6 +644,8 @@
if is_query then fst (fold mk_mode ts2 (([], []), 1))
else (ts2, 1 upto length (binder_types T) - k);
val mode = find_mode gr1 dep s u modes is;
+ val _ = if is_query orelse not (needs_random (the mode)) then ()
+ else warning ("Illegal use of random data generators in " ^ s);
val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1;
val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
in
@@ -700,4 +773,91 @@
Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
"introduction rules for executable predicates";
+(**** Quickcheck involving inductive predicates ****)
+
+val test_fn : (int * int * int -> term list option) Unsynchronized.ref =
+ Unsynchronized.ref (fn _ => NONE);
+
+fun strip_imp p =
+ let val (q, r) = HOLogic.dest_imp p
+ in strip_imp r |>> cons q end
+ handle TERM _ => ([], p);
+
+fun deepen bound f i =
+ if i > bound then NONE
+ else (case f i of
+ NONE => deepen bound f (i + 1)
+ | SOME x => SOME x);
+
+val depth_bound_value =
+ Config.declare false "ind_quickcheck_depth" (Config.Int 10);
+val depth_bound = Config.int depth_bound_value;
+
+val depth_start_value =
+ Config.declare false "ind_quickcheck_depth_start" (Config.Int 1);
+val depth_start = Config.int depth_start_value;
+
+val random_values_value =
+ Config.declare false "ind_quickcheck_random" (Config.Int 5);
+val random_values = Config.int random_values_value;
+
+val size_offset_value =
+ Config.declare false "ind_quickcheck_size_offset" (Config.Int 0);
+val size_offset = Config.int size_offset_value;
+
+fun test_term ctxt t =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (xs, p) = strip_abs t;
+ val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
+ val args = map Free args';
+ val (ps, q) = strip_imp p;
+ val Ts = map snd xs;
+ val T = Ts ---> HOLogic.boolT;
+ val rl = Logic.list_implies
+ (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @
+ [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))],
+ HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args)));
+ val (_, thy') = Inductive.add_inductive_global
+ {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
+ no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
+ [((Binding.name "quickcheckp", T), NoSyn)] []
+ [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
+ val pred = HOLogic.mk_Trueprop (list_comb
+ (Const (Sign.intern_const thy' "quickcheckp", T),
+ map Term.dummy_pattern Ts));
+ val (code, gr) = setmp_CRITICAL mode ["term_of", "test", "random_ind"]
+ (generate_code_i thy' [] "Generated") [("testf", pred)];
+ val s = "structure TestTerm =\nstruct\n\n" ^
+ cat_lines (map snd code) ^
+ "\nopen Generated;\n\n" ^ string_of
+ (Pretty.block [str "val () = InductiveCodegen.test_fn :=",
+ Pretty.brk 1, str "(fn p =>", Pretty.brk 1,
+ str "case Seq.pull (testf p) of", Pretty.brk 1,
+ str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
+ str " =>", Pretty.brk 1, str "SOME ",
+ Pretty.block (str "[" ::
+ Pretty.commas (map (fn (s, T) => Pretty.block
+ [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
+ [str "]"]), Pretty.brk 1,
+ str "| NONE => NONE);"]) ^
+ "\n\nend;\n";
+ val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
+ val values = Config.get ctxt random_values;
+ val bound = Config.get ctxt depth_bound;
+ val start = Config.get ctxt depth_start;
+ val offset = Config.get ctxt size_offset;
+ val test_fn' = !test_fn;
+ fun test k = deepen bound (fn i =>
+ (priority ("Search depth: " ^ string_of_int i);
+ test_fn' (i, values, k+offset))) start;
+ in test end;
+
+val quickcheck_setup =
+ Attrib.register_config depth_bound_value #>
+ Attrib.register_config depth_start_value #>
+ Attrib.register_config random_values_value #>
+ Attrib.register_config size_offset_value #>
+ Quickcheck.add_generator ("SML_inductive", test_term);
+
end;
--- a/src/HOLCF/Bifinite.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Bifinite.thy Fri Nov 20 10:40:30 2009 +0100
@@ -114,6 +114,9 @@
lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
unfolding cprod_map_def by simp
+lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by auto
+
lemma cprod_map_map:
"cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
@@ -207,6 +210,9 @@
lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
unfolding cfun_map_def by simp
+lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by simp
+
lemma cfun_map_map:
"cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
--- a/src/HOLCF/ConvexPD.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy Fri Nov 20 10:40:30 2009 +0100
@@ -495,6 +495,9 @@
lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: convex_pd_induct, simp_all)
+lemma convex_map_ID: "convex_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def convex_map_ident)
+
lemma convex_map_map:
"convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
by (induct xs rule: convex_pd_induct, simp_all)
--- a/src/HOLCF/Domain.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Domain.thy Fri Nov 20 10:40:30 2009 +0100
@@ -5,7 +5,7 @@
header {* Domain package *}
theory Domain
-imports Ssum Sprod Up One Tr Fixrec
+imports Ssum Sprod Up One Tr Fixrec Representable
uses
("Tools/cont_consts.ML")
("Tools/cont_proc.ML")
--- a/src/HOLCF/IsaMakefile Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/IsaMakefile Fri Nov 20 10:40:30 2009 +0100
@@ -52,6 +52,7 @@
Pcpo.thy \
Porder.thy \
Product_Cpo.thy \
+ Representable.thy \
Sprod.thy \
Ssum.thy \
Sum_Cpo.thy \
@@ -64,11 +65,13 @@
Tools/cont_proc.ML \
Tools/Domain/domain_extender.ML \
Tools/Domain/domain_axioms.ML \
+ Tools/Domain/domain_isomorphism.ML \
Tools/Domain/domain_library.ML \
Tools/Domain/domain_syntax.ML \
Tools/Domain/domain_theorems.ML \
Tools/fixrec.ML \
Tools/pcpodef.ML \
+ Tools/repdef.ML \
holcf_logic.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
@@ -97,6 +100,7 @@
ex/Focus_ex.thy \
ex/Hoare.thy \
ex/Loop.thy \
+ ex/New_Domain.thy \
ex/Powerdomain_ex.thy \
ex/Stream.thy \
ex/ROOT.ML
--- a/src/HOLCF/LowerPD.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/LowerPD.thy Fri Nov 20 10:40:30 2009 +0100
@@ -471,6 +471,9 @@
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: lower_pd_induct, simp_all)
+lemma lower_map_ID: "lower_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def lower_map_ident)
+
lemma lower_map_map:
"lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
by (induct xs rule: lower_pd_induct, simp_all)
--- a/src/HOLCF/Representable.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Representable.thy Fri Nov 20 10:40:30 2009 +0100
@@ -5,8 +5,10 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum Sprod One ConvexPD
-uses ("Tools/repdef.ML")
+imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec
+uses
+ ("Tools/repdef.ML")
+ ("Tools/Domain/domain_isomorphism.ML")
begin
subsection {* Class of representable types *}
@@ -159,6 +161,25 @@
apply simp
done
+text {* Isomorphism lemmas used internally by the domain package: *}
+
+lemma domain_abs_iso:
+ fixes abs and rep
+ assumes REP: "REP('b) = REP('a)"
+ assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "rep\<cdot>(abs\<cdot>x) = x"
+unfolding abs_def rep_def by (simp add: REP)
+
+lemma domain_rep_iso:
+ fixes abs and rep
+ assumes REP: "REP('b) = REP('a)"
+ assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "abs\<cdot>(rep\<cdot>x) = x"
+unfolding abs_def rep_def by (simp add: REP [symmetric])
+
+
subsection {* Proving a subtype is representable *}
text {*
@@ -671,16 +692,14 @@
Abs_fin_defl (udom_emb oo
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
-definition "one_typ = REP(one)"
-definition "tr_typ = REP(tr)"
-definition "cfun_typ = TypeRep_fun2 cfun_map"
-definition "ssum_typ = TypeRep_fun2 ssum_map"
-definition "sprod_typ = TypeRep_fun2 sprod_map"
-definition "cprod_typ = TypeRep_fun2 cprod_map"
-definition "u_typ = TypeRep_fun1 u_map"
-definition "upper_typ = TypeRep_fun1 upper_map"
-definition "lower_typ = TypeRep_fun1 lower_map"
-definition "convex_typ = TypeRep_fun1 convex_map"
+definition "cfun_defl = TypeRep_fun2 cfun_map"
+definition "ssum_defl = TypeRep_fun2 ssum_map"
+definition "sprod_defl = TypeRep_fun2 sprod_map"
+definition "cprod_defl = TypeRep_fun2 cprod_map"
+definition "u_defl = TypeRep_fun1 u_map"
+definition "upper_defl = TypeRep_fun1 upper_map"
+definition "lower_defl = TypeRep_fun1 lower_map"
+definition "convex_defl = TypeRep_fun1 convex_map"
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
unfolding below_fin_defl_def .
@@ -729,138 +748,130 @@
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
-lemma cast_cfun_typ:
- "cast\<cdot>(cfun_typ\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cfun_typ_def
+lemma cast_cfun_defl:
+ "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cfun_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_cfun_map)
done
-lemma cast_ssum_typ:
- "cast\<cdot>(ssum_typ\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding ssum_typ_def
+lemma cast_ssum_defl:
+ "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding ssum_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_ssum_map)
done
-lemma cast_sprod_typ:
- "cast\<cdot>(sprod_typ\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding sprod_typ_def
+lemma cast_sprod_defl:
+ "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding sprod_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_sprod_map)
done
-lemma cast_cprod_typ:
- "cast\<cdot>(cprod_typ\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cprod_typ_def
+lemma cast_cprod_defl:
+ "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cprod_defl_def
apply (rule cast_TypeRep_fun2)
apply (erule (1) finite_deflation_cprod_map)
done
-lemma cast_u_typ:
- "cast\<cdot>(u_typ\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding u_typ_def
+lemma cast_u_defl:
+ "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding u_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_u_map)
done
-lemma cast_upper_typ:
- "cast\<cdot>(upper_typ\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding upper_typ_def
+lemma cast_upper_defl:
+ "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding upper_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_upper_map)
done
-lemma cast_lower_typ:
- "cast\<cdot>(lower_typ\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding lower_typ_def
+lemma cast_lower_defl:
+ "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding lower_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_lower_map)
done
-lemma cast_convex_typ:
- "cast\<cdot>(convex_typ\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding convex_typ_def
+lemma cast_convex_defl:
+ "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding convex_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_convex_map)
done
text {* REP of type constructor = type combinator *}
-lemma REP_one: "REP(one) = one_typ"
-by (simp only: one_typ_def)
-
-lemma REP_tr: "REP(tr) = tr_typ"
-by (simp only: tr_typ_def)
-
-lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cfun_typ)
+apply (simp add: cast_REP cast_cfun_defl)
apply (simp add: cfun_map_def)
apply (simp only: prj_cfun_def emb_cfun_def)
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
done
-lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_ssum_typ)
+apply (simp add: cast_REP cast_ssum_defl)
apply (simp add: prj_ssum_def)
apply (simp add: emb_ssum_def)
apply (simp add: ssum_map_map cfcomp1)
done
-lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_sprod_typ)
+apply (simp add: cast_REP cast_sprod_defl)
apply (simp add: prj_sprod_def)
apply (simp add: emb_sprod_def)
apply (simp add: sprod_map_map cfcomp1)
done
-lemma REP_cprod: "REP('a \<times> 'b) = cprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cprod_typ)
+apply (simp add: cast_REP cast_cprod_defl)
apply (simp add: prj_cprod_def)
apply (simp add: emb_cprod_def)
apply (simp add: cprod_map_map cfcomp1)
done
-lemma REP_up: "REP('a u) = u_typ\<cdot>REP('a)"
+lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_u_typ)
+apply (simp add: cast_REP cast_u_defl)
apply (simp add: prj_u_def)
apply (simp add: emb_u_def)
apply (simp add: u_map_map cfcomp1)
done
-lemma REP_upper: "REP('a upper_pd) = upper_typ\<cdot>REP('a)"
+lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_upper_typ)
+apply (simp add: cast_REP cast_upper_defl)
apply (simp add: prj_upper_pd_def)
apply (simp add: emb_upper_pd_def)
apply (simp add: upper_map_map cfcomp1)
done
-lemma REP_lower: "REP('a lower_pd) = lower_typ\<cdot>REP('a)"
+lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_lower_typ)
+apply (simp add: cast_REP cast_lower_defl)
apply (simp add: prj_lower_pd_def)
apply (simp add: emb_lower_pd_def)
apply (simp add: lower_map_map cfcomp1)
done
-lemma REP_convex: "REP('a convex_pd) = convex_typ\<cdot>REP('a)"
+lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_convex_typ)
+apply (simp add: cast_REP cast_convex_defl)
apply (simp add: prj_convex_pd_def)
apply (simp add: emb_convex_pd_def)
apply (simp add: convex_map_map cfcomp1)
done
lemmas REP_simps =
- REP_one
- REP_tr
REP_cfun
REP_ssum
REP_sprod
@@ -944,69 +955,111 @@
apply (simp add: emb_coerce coerce_prj REP)
done
+lemma isodefl_abs_rep:
+ fixes abs and rep and d
+ assumes REP: "REP('b) = REP('a)"
+ assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+ assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
+unfolding abs_def rep_def using REP by (rule isodefl_coerce)
+
lemma isodefl_cfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_typ\<cdot>t1\<cdot>t2)"
+ isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_cfun_typ cast_isodefl)
+apply (simp add: cast_cfun_defl cast_isodefl)
apply (simp add: emb_cfun_def prj_cfun_def)
apply (simp add: cfun_map_map cfcomp1)
done
lemma isodefl_ssum:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_typ\<cdot>t1\<cdot>t2)"
+ isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_ssum_typ cast_isodefl)
+apply (simp add: cast_ssum_defl cast_isodefl)
apply (simp add: emb_ssum_def prj_ssum_def)
apply (simp add: ssum_map_map isodefl_strict)
done
lemma isodefl_sprod:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
- isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_typ\<cdot>t1\<cdot>t2)"
+ isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
-apply (simp add: cast_sprod_typ cast_isodefl)
+apply (simp add: cast_sprod_defl cast_isodefl)
apply (simp add: emb_sprod_def prj_sprod_def)
apply (simp add: sprod_map_map isodefl_strict)
done
+lemma isodefl_cprod:
+ "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+ isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_cprod_defl cast_isodefl)
+apply (simp add: emb_cprod_def prj_cprod_def)
+apply (simp add: cprod_map_map cfcomp1)
+done
+
lemma isodefl_u:
- "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_u_typ cast_isodefl)
+apply (simp add: cast_u_defl cast_isodefl)
apply (simp add: emb_u_def prj_u_def)
apply (simp add: u_map_map)
done
-lemma isodefl_one: "isodefl (ID :: one \<rightarrow> one) one_typ"
-unfolding one_typ_def by (rule isodefl_ID_REP)
-
-lemma isodefl_tr: "isodefl (ID :: tr \<rightarrow> tr) tr_typ"
-unfolding tr_typ_def by (rule isodefl_ID_REP)
-
lemma isodefl_upper:
- "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_upper_typ cast_isodefl)
+apply (simp add: cast_upper_defl cast_isodefl)
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
apply (simp add: upper_map_map)
done
lemma isodefl_lower:
- "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_lower_typ cast_isodefl)
+apply (simp add: cast_lower_defl cast_isodefl)
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
apply (simp add: lower_map_map)
done
lemma isodefl_convex:
- "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_typ\<cdot>t)"
+ "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
apply (rule isodeflI)
-apply (simp add: cast_convex_typ cast_isodefl)
+apply (simp add: cast_convex_defl cast_isodefl)
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
apply (simp add: convex_map_map)
done
+subsection {* Constructing Domain Isomorphisms *}
+
+use "Tools/Domain/domain_isomorphism.ML"
+
+setup {*
+ fold Domain_Isomorphism.add_type_constructor
+ [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
+ @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}),
+
+ (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
+ @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}),
+
+ (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
+ @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}),
+
+ (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
+ @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}),
+
+ (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
+ @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}),
+
+ (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
+ @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}),
+
+ (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
+ @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}),
+
+ (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
+ @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})]
+*}
+
end
--- a/src/HOLCF/Sprod.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Sprod.thy Fri Nov 20 10:40:30 2009 +0100
@@ -245,6 +245,9 @@
"x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
by (simp add: sprod_map_def)
+lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
+
lemma sprod_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
--- a/src/HOLCF/Ssum.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Ssum.thy Fri Nov 20 10:40:30 2009 +0100
@@ -226,6 +226,9 @@
lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
unfolding ssum_map_def by simp
+lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
+unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
+
lemma ssum_map_map:
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Nov 20 10:40:30 2009 +0100
@@ -6,13 +6,16 @@
signature DOMAIN_AXIOMS =
sig
- val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
+ val copy_of_dtyp :
+ string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
val calc_axioms :
+ bool -> string Symtab.table ->
string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
string * (string * term) list * (string * term) list
val add_axioms :
+ bool ->
bstring -> Domain_Library.eq list -> theory -> theory
end;
@@ -34,119 +37,124 @@
(@{type_name "*"}, @{const_name "cprod_map"}),
(@{type_name "u"}, @{const_name "u_map"})];
-fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
-and copy r (DatatypeAux.DtRec i) = r i
- | copy r (DatatypeAux.DtTFree a) = ID
- | copy r (DatatypeAux.DtType (c, ds)) =
- case Symtab.lookup copy_tab c of
- SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
+fun copy_of_dtyp tab r dt =
+ if DatatypeAux.is_rec_type dt then copy tab r dt else ID
+and copy tab r (DatatypeAux.DtRec i) = r i
+ | copy tab r (DatatypeAux.DtTFree a) = ID
+ | copy tab r (DatatypeAux.DtType (c, ds)) =
+ case Symtab.lookup tab c of
+ SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
| NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
fun calc_axioms
- (comp_dname : string)
- (eqs : eq list)
- (n : int)
- (eqn as ((dname,_),cons) : eq)
+ (definitional : bool)
+ (map_tab : string Symtab.table)
+ (comp_dname : string)
+ (eqs : eq list)
+ (n : int)
+ (eqn as ((dname,_),cons) : eq)
: string * (string * term) list * (string * term) list =
- let
-
- (* ----- axioms and definitions concerning the isomorphism ------------------ *)
+ let
- val dc_abs = %%:(dname^"_abs");
- val dc_rep = %%:(dname^"_rep");
- val x_name'= "x";
- val x_name = idx_name eqs x_name' (n+1);
- val dnam = Long_Name.base_name dname;
+(* ----- axioms and definitions concerning the isomorphism ------------------ *)
- val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
- val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
+ val dc_abs = %%:(dname^"_abs");
+ val dc_rep = %%:(dname^"_rep");
+ val x_name'= "x";
+ val x_name = idx_name eqs x_name' (n+1);
+ val dnam = Long_Name.base_name dname;
+
+ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
+ val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
- val when_def = ("when_def",%%:(dname^"_when") ==
- List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
- Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
-
- val copy_def =
- let fun r i = proj (Bound 0) eqs i;
- in ("copy_def", %%:(dname^"_copy") ==
- /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
-
- (* -- definitions concerning the constructors, discriminators and selectors - *)
+ val when_def = ("when_def",%%:(dname^"_when") ==
+ List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
- fun con_def m n (_,args) = let
- fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
- fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
- fun inj y 1 _ = y
- | inj y _ 0 = mk_sinl y
- | inj y i j = mk_sinr (inj y (i-1) (j-1));
- in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
-
- val con_defs = mapn (fn n => fn (con,args) =>
- (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+ val copy_def =
+ let fun r i = proj (Bound 0) eqs i;
+ in
+ ("copy_def", %%:(dname^"_copy") == /\ "f"
+ (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
+ end;
+
+(* -- definitions concerning the constructors, discriminators and selectors - *)
+
+ fun con_def m n (_,args) = let
+ fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
+ fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
+ fun inj y 1 _ = y
+ | inj y _ 0 = mk_sinl y
+ | inj y i j = mk_sinr (inj y (i-1) (j-1));
+ in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
- val dis_defs = let
- fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => (List.foldr /\#
+ val con_defs = mapn (fn n => fn (con,args) =>
+ (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+
+ val dis_defs = let
+ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => (List.foldr /\#
(if con'=con then TT else FF) args)) cons))
- in map ddef cons end;
-
- val mat_defs =
- let
- fun mdef (con,_) =
- let
- val k = Bound 0
- val x = Bound 1
- fun one_con (con', args') =
- if con'=con then k else List.foldr /\# mk_fail args'
- val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
- val rhs = /\ "x" (/\ "k" (w ` x))
- in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
- in map mdef cons end;
+ in map ddef cons end;
- val pat_defs =
+ val mat_defs =
+ let
+ fun mdef (con,_) =
+ let
+ val k = Bound 0
+ val x = Bound 1
+ fun one_con (con', args') =
+ if con'=con then k else List.foldr /\# mk_fail args'
+ val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
+ val rhs = /\ "x" (/\ "k" (w ` x))
+ in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
+ in map mdef cons end;
+
+ val pat_defs =
+ let
+ fun pdef (con,args) =
let
- fun pdef (con,args) =
- let
- val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
- val xs = map (bound_arg args) args;
- val r = Bound (length args);
- val rhs = case args of [] => mk_return HOLogic.unit
- | _ => mk_ctuple_pat ps ` mk_ctuple xs;
- fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
- in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
- list_ccomb(%%:(dname^"_when"), map one_con cons))
- end
- in map pdef cons end;
+ val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+ val xs = map (bound_arg args) args;
+ val r = Bound (length args);
+ val rhs = case args of [] => mk_return HOLogic.unit
+ | _ => mk_ctuple_pat ps ` mk_ctuple xs;
+ fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
+ in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) ==
+ list_ccomb(%%:(dname^"_when"), map one_con cons))
+ end
+ in map pdef cons end;
- val sel_defs = let
- fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
- list_ccomb(%%:(dname^"_when"),map
- (fn (con',args) => if con'<>con then UU else
- List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
- in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+ val sel_defs = let
+ fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
+ list_ccomb(%%:(dname^"_when"),map
+ (fn (con',args) => if con'<>con then UU else
+ List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
+ in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
- (* ----- axiom and definitions concerning induction ------------------------- *)
+(* ----- axiom and definitions concerning induction ------------------------- *)
- val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
- `%x_name === %:x_name));
- val take_def =
- ("take_def",
- %%:(dname^"_take") ==
- mk_lam("n",proj
- (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
- val finite_def =
- ("finite_def",
- %%:(dname^"_finite") ==
- mk_lam(x_name,
- mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+ val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
+ `%x_name === %:x_name));
+ val take_def =
+ ("take_def",
+ %%:(dname^"_take") ==
+ mk_lam("n",proj
+ (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
+ val finite_def =
+ ("finite_def",
+ %%:(dname^"_finite") ==
+ mk_lam(x_name,
+ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
- in (dnam,
- [abs_iso_ax, rep_iso_ax, reach_ax],
- [when_def, copy_def] @
- con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
- [take_def, finite_def])
- end; (* let (calc_axioms) *)
+ in (dnam,
+ (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+ (if definitional then [when_def] else [when_def, copy_def]) @
+ con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
+ [take_def, finite_def])
+ end; (* let (calc_axioms) *)
(* legacy type inference *)
@@ -173,16 +181,17 @@
val ms = map qualify con_names ~~ map qualify mat_names;
in Fixrec.add_matchers ms thy end;
-fun add_axioms comp_dnam (eqs : eq list) thy' =
- let
- val comp_dname = Sign.full_bname thy' comp_dnam;
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
- fun copy_app dname = %%:(dname^"_copy")`Bound 0;
- val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
- /\ "f"(mk_ctuple (map copy_app dnames)));
+fun add_axioms definitional comp_dnam (eqs : eq list) thy' =
+ let
+ val comp_dname = Sign.full_bname thy' comp_dnam;
+ val dnames = map (fst o fst) eqs;
+ val x_name = idx_name dnames "x";
+ fun copy_app dname = %%:(dname^"_copy")`Bound 0;
+ val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
+ /\ "f"(mk_ctuple (map copy_app dnames)));
- fun one_con (con,args) = let
+ fun one_con (con,args) =
+ let
val nonrec_args = filter_out is_rec args;
val rec_args = filter is_rec args;
val recs_cnt = length rec_args;
@@ -199,37 +208,46 @@
fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $
Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
val capps =
- List.foldr mk_conj
- (mk_conj(
- Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
- (mapn rel_app 1 rec_args);
- in List.foldr mk_ex
- (Library.foldr mk_conj
- (map (defined o Bound) nonlazy_idxs,capps)) allvns
+ List.foldr
+ mk_conj
+ (mk_conj(
+ Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
+ Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
+ (mapn rel_app 1 rec_args);
+ in
+ List.foldr
+ mk_ex
+ (Library.foldr mk_conj
+ (map (defined o Bound) nonlazy_idxs,capps)) allvns
end;
- fun one_comp n (_,cons) =
- mk_all(x_name(n+1),
- mk_all(x_name(n+1)^"'",
- mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
- foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
- ::map one_con cons))));
- val bisim_def =
- ("bisim_def",
- %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
-
- fun add_one (dnam, axs, dfs) =
- Sign.add_path dnam
+ fun one_comp n (_,cons) =
+ mk_all (x_name(n+1),
+ mk_all (x_name(n+1)^"'",
+ mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
+ foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+ ::map one_con cons))));
+ val bisim_def =
+ ("bisim_def", %%:(comp_dname^"_bisim") ==
+ mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
+
+ fun add_one (dnam, axs, dfs) =
+ Sign.add_path dnam
#> add_defs_infer dfs
#> add_axioms_infer axs
#> Sign.parent_path;
- val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy';
+ val map_tab = Domain_Isomorphism.get_map_tab thy';
+
+ val thy = thy'
+ |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
- in thy |> Sign.add_path comp_dnam
- |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
- |> Sign.parent_path
- |> fold add_matchers eqs
- end; (* let (add_axioms) *)
+ val use_copy_def = length eqs>1 andalso not definitional;
+ in
+ thy
+ |> Sign.add_path comp_dnam
+ |> add_defs_infer (bisim_def::(if use_copy_def then [copy_def] else []))
+ |> Sign.parent_path
+ |> fold add_matchers eqs
+ end; (* let (add_axioms) *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Nov 20 10:40:30 2009 +0100
@@ -6,14 +6,29 @@
signature DOMAIN_EXTENDER =
sig
- val add_domain_cmd: string ->
- ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list
- -> theory -> theory
- val add_domain: string ->
- ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * typ) list * mixfix) list) list
- -> theory -> theory
+ val add_domain_cmd:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
+ -> theory -> theory
+
+ val add_domain:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
+
+ val add_new_domain_cmd:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
+ -> theory -> theory
+
+ val add_new_domain:
+ string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
+ -> theory -> theory
end;
structure Domain_Extender :> DOMAIN_EXTENDER =
@@ -23,132 +38,231 @@
(* ----- general testing and preprocessing of constructor list -------------- *)
fun check_and_sort_domain
- (dtnvs : (string * typ list) list)
- (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
- (sg : theory)
+ (definitional : bool)
+ (dtnvs : (string * typ list) list)
+ (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
+ (thy : theory)
: ((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list =
- let
- val defaultS = Sign.defaultS sg;
- val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
- [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons =
- (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of
- [] => false | dups => error ("Duplicate constructors: "
- ^ commas_quote dups));
- val test_dupl_sels =
- (case duplicates (op =) (map Binding.name_of (map_filter second
- (maps second (flat cons'')))) of
- [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
- val test_dupl_tvars =
- exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
- [] => false | dups => error("Duplicate type arguments: "
- ^commas_quote dups)) (map snd dtnvs);
- (* test for free type variables, illegal sort constraints on rhs,
- non-pcpo-types and invalid use of recursive type;
- replace sorts in type variables on rhs *)
- fun analyse_equation ((dname,typevars),cons') =
- let
- val tvars = map dest_TFree typevars;
- val distinct_typevars = map TFree tvars;
- fun rm_sorts (TFree(s,_)) = TFree(s,[])
- | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
- | rm_sorts (TVar(s,_)) = TVar(s,[])
- and remove_sorts l = map rm_sorts l;
- val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
- fun analyse indirect (TFree(v,s)) =
- (case AList.lookup (op =) tvars v of
- NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
- | SOME sort => if eq_set (op =) (s, defaultS) orelse
- eq_set (op =) (s, sort)
- then TFree(v,sort)
- else error ("Inconsistent sort constraint" ^
- " for type variable " ^ quote v))
- | analyse indirect (t as Type(s,typl)) =
- (case AList.lookup (op =) dtnvs s of
- NONE => if s mem indirect_ok
- then Type(s,map (analyse false) typl)
- else Type(s,map (analyse true) typl)
- | SOME typevars => if indirect
- then error ("Indirect recursion of type " ^
- quote (string_of_typ sg t))
- else if dname <> s orelse
- (** BUG OR FEATURE?:
- mutual recursion may use different arguments **)
- remove_sorts typevars = remove_sorts typl
- then Type(s,map (analyse true) typl)
- else error ("Direct recursion of type " ^
- quote (string_of_typ sg t) ^
- " with different arguments"))
- | analyse indirect (TVar _) = Imposs "extender:analyse";
- fun check_pcpo lazy T =
- let val ok = if lazy then cpo_type else pcpo_type
- in if ok sg T then T else error
- ("Constructor argument type is not of sort pcpo: " ^
- string_of_typ sg T)
- end;
- fun analyse_arg (lazy, sel, T) =
- (lazy, sel, check_pcpo lazy (analyse false T));
- fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
- in ((dname,distinct_typevars), map analyse_con cons') end;
- in ListPair.map analyse_equation (dtnvs,cons'')
- end; (* let *)
+ let
+ val defaultS = Sign.defaultS thy;
+
+ val test_dupl_typs =
+ case duplicates (op =) (map fst dtnvs) of
+ [] => false | dups => error ("Duplicate types: " ^ commas_quote dups);
+
+ val all_cons = map (Binding.name_of o first) (flat cons'');
+ val test_dupl_cons =
+ case duplicates (op =) all_cons of
+ [] => false | dups => error ("Duplicate constructors: "
+ ^ commas_quote dups);
+ val all_sels =
+ (map Binding.name_of o map_filter second o maps second) (flat cons'');
+ val test_dupl_sels =
+ case duplicates (op =) all_sels of
+ [] => false | dups => error("Duplicate selectors: "^commas_quote dups);
+
+ fun test_dupl_tvars s =
+ case duplicates (op =) (map(fst o dest_TFree)s) of
+ [] => false | dups => error("Duplicate type arguments: "
+ ^commas_quote dups);
+ val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs);
+
+ (* test for free type variables, illegal sort constraints on rhs,
+ non-pcpo-types and invalid use of recursive type;
+ replace sorts in type variables on rhs *)
+ fun analyse_equation ((dname,typevars),cons') =
+ let
+ val tvars = map dest_TFree typevars;
+ val distinct_typevars = map TFree tvars;
+ fun rm_sorts (TFree(s,_)) = TFree(s,[])
+ | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+ | rm_sorts (TVar(s,_)) = TVar(s,[])
+ and remove_sorts l = map rm_sorts l;
+ val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+ fun analyse indirect (TFree(v,s)) =
+ (case AList.lookup (op =) tvars v of
+ NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
+ | SOME sort => if eq_set (op =) (s, defaultS) orelse
+ eq_set (op =) (s, sort)
+ then TFree(v,sort)
+ else error ("Inconsistent sort constraint" ^
+ " for type variable " ^ quote v))
+ | analyse indirect (t as Type(s,typl)) =
+ (case AList.lookup (op =) dtnvs s of
+ NONE =>
+ if definitional orelse s mem indirect_ok
+ then Type(s,map (analyse false) typl)
+ else Type(s,map (analyse true) typl)
+ | SOME typevars =>
+ if indirect
+ then error ("Indirect recursion of type " ^
+ quote (string_of_typ thy t))
+ else if dname <> s orelse
+ (** BUG OR FEATURE?:
+ mutual recursion may use different arguments **)
+ remove_sorts typevars = remove_sorts typl
+ then Type(s,map (analyse true) typl)
+ else error ("Direct recursion of type " ^
+ quote (string_of_typ thy t) ^
+ " with different arguments"))
+ | analyse indirect (TVar _) = Imposs "extender:analyse";
+ fun check_pcpo lazy T =
+ let val ok = if lazy then cpo_type else pcpo_type
+ in if ok thy T then T
+ else error ("Constructor argument type is not of sort pcpo: " ^
+ string_of_typ thy T)
+ end;
+ fun analyse_arg (lazy, sel, T) =
+ (lazy, sel, check_pcpo lazy (analyse false T));
+ fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
+ in ((dname,distinct_typevars), map analyse_con cons') end;
+ in ListPair.map analyse_equation (dtnvs,cons'')
+ end; (* let *)
(* ----- calls for building new thy and thms -------------------------------- *)
fun gen_add_domain
- (prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
- (eqs''' : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * 'a) list * mixfix) list) list)
- (thy''' : theory) =
- let
- fun readS (SOME s) = Syntax.read_sort_global thy''' s
- | readS NONE = Sign.defaultS thy''';
- fun readTFree (a, s) = TFree (a, readS s);
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy''' s
+ | readS NONE = Sign.defaultS thy''';
+ fun readTFree (a, s) = TFree (a, readS s);
+
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) =
+ (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
+ val thy'' =
+ thy'''
+ |> Sign.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+ val cons'' =
+ map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+ val dtnvs' =
+ map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
+ check_and_sort_domain false dtnvs' cons'' thy'';
+ val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
+ val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+ fun typid (Type (id,_)) =
+ let val c = hd (Symbol.explode (Long_Name.base_name id))
+ in if Symbol.is_letter c then c else "t" end
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
+ ListPair.map (fn ((lazy,sel,tp),vn) =>
+ mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+ Option.map Binding.name_of sel,vn))
+ (args,(mk_var_names(map (typid o third) args)))
+ ) : cons;
+ val eqs : eq list =
+ map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+ val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs;
+ val ((rewss, take_rews), theorems_thy) =
+ thy
+ |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ in
+ theorems_thy
+ |> Sign.add_path (Long_Name.base_name comp_dnam)
+ |> PureThy.add_thmss
+ [((Binding.name "rews", flat rewss @ take_rews), [])]
+ |> snd
+ |> Sign.parent_path
+ end;
- val dtnvs = map (fn (vs,dname:binding,mx,_) =>
- (dname, map readTFree vs, mx)) eqs''';
- val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
- fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
- fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
- val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
- |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
- val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
- val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
- val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
- check_and_sort_domain dtnvs' cons'' thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
- val dts = map (Type o fst) eqs';
- val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
- fun typid (Type (id,_)) =
- let val c = hd (Symbol.explode (Long_Name.base_name id))
- in if Symbol.is_letter c then c else "t" end
- | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
- | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun one_con (con,args,mx) =
- ((Syntax.const_name mx (Binding.name_of con)),
- ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
- DatatypeAux.dtyp_of_typ new_dts tp),
- Option.map Binding.name_of sel,vn))
- (args,(mk_var_names(map (typid o third) args)))
- ) : cons;
- val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
- val ((rewss, take_rews), theorems_thy) =
- thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
- ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
- in
- theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
- |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])]))
- |> Sign.parent_path
- end;
+fun gen_add_new_domain
+ (prep_typ : theory -> 'a -> typ)
+ (comp_dnam : string)
+ (eqs''' : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (thy''' : theory) =
+ let
+ fun readS (SOME s) = Syntax.read_sort_global thy''' s
+ | readS NONE = Sign.defaultS thy''';
+ fun readTFree (a, s) = TFree (a, readS s);
+
+ val dtnvs = map (fn (vs,dname:binding,mx,_) =>
+ (dname, map readTFree vs, mx)) eqs''';
+ val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+ fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
+ fun thy_arity (dname,tvars,mx) =
+ (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep});
+
+ (* this theory is used just for parsing and error checking *)
+ val tmp_thy = thy'''
+ |> Theory.copy
+ |> Sign.add_types (map thy_type dtnvs)
+ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+
+ val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
+ map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
+ val dtnvs' : (string * typ list) list =
+ map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+ val eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list =
+ check_and_sort_domain true dtnvs' cons'' tmp_thy;
+
+ fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
+ fun mk_con_typ (bind, args, mx) =
+ if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
+ fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
+
+ val thy'' = thy''' |>
+ Domain_Isomorphism.domain_isomorphism
+ (map (fn ((vs, dname, mx, _), eq) =>
+ (map fst vs, dname, mx, mk_eq_typ eq))
+ (eqs''' ~~ eqs'))
+
+ val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
+ val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+ fun typid (Type (id,_)) =
+ let val c = hd (Symbol.explode (Long_Name.base_name id))
+ in if Symbol.is_letter c then c else "t" end
+ | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
+ | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+ fun one_con (con,args,mx) =
+ ((Syntax.const_name mx (Binding.name_of con)),
+ ListPair.map (fn ((lazy,sel,tp),vn) =>
+ mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+ Option.map Binding.name_of sel,vn))
+ (args,(mk_var_names(map (typid o third) args)))
+ ) : cons;
+ val eqs : eq list =
+ map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+ val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs;
+ val ((rewss, take_rews), theorems_thy) =
+ thy
+ |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ in
+ theorems_thy
+ |> Sign.add_path (Long_Name.base_name comp_dnam)
+ |> PureThy.add_thmss
+ [((Binding.name "rews", flat rewss @ take_rews), [])]
+ |> snd
+ |> Sign.parent_path
+ end;
val add_domain = gen_add_domain Sign.certify_typ;
val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
+val add_new_domain = gen_add_new_domain Sign.certify_typ;
+val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global;
+
(** outer syntax **)
@@ -157,47 +271,57 @@
val _ = OuterKeyword.keyword "lazy";
val dest_decl : (bool * binding option * string) parser =
- P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
- || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
- >> (fn t => (true,NONE,t))
- || P.typ >> (fn t => (false,NONE,t));
+ P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
+ (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ >> (fn t => (true,NONE,t))
+ || P.typ >> (fn t => (false,NONE,t));
val cons_decl =
- P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+ P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
val type_var' : (string * string option) parser =
- (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
+ (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
val type_args' : (string * string option) list parser =
- type_var' >> single ||
- P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
- Scan.succeed [];
+ type_var' >> single
+ || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")")
+ || Scan.succeed [];
val domain_decl =
- (type_args' -- P.binding -- P.opt_infix) --
- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+ (type_args' -- P.binding -- P.opt_infix) --
+ (P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
- P.and_list1 domain_decl;
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+ P.and_list1 domain_decl;
-fun mk_domain (opt_name : string option,
- doms : ((((string * string option) list * binding) * mixfix) *
- ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
- let
- val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
- val specs : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list =
- map (fn (((vs, t), mx), cons) =>
- (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
- val comp_dnam =
- case opt_name of NONE => space_implode "_" names | SOME s => s;
- in add_domain_cmd comp_dnam specs end;
+fun mk_domain
+ (definitional : bool)
+ (opt_name : string option,
+ doms : ((((string * string option) list * binding) * mixfix) *
+ ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
+ let
+ val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
+ val specs : ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list =
+ map (fn (((vs, t), mx), cons) =>
+ (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
+ val comp_dnam =
+ case opt_name of NONE => space_implode "_" names | SOME s => s;
+ in
+ if definitional
+ then add_new_domain_cmd comp_dnam specs
+ else add_domain_cmd comp_dnam specs
+ end;
val _ =
- OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
- (domains_decl >> (Toplevel.theory o mk_domain));
+ OuterSyntax.command "domain" "define recursive domains (HOLCF)"
+ K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
+
+val _ =
+ OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
+ K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 20 10:40:30 2009 +0100
@@ -0,0 +1,710 @@
+(* Title: HOLCF/Tools/domain/domain_isomorphism.ML
+ Author: Brian Huffman
+
+Defines new types satisfying the given domain equations.
+*)
+
+signature DOMAIN_ISOMORPHISM =
+sig
+ val domain_isomorphism:
+ (string list * binding * mixfix * typ) list -> theory -> theory
+ val domain_isomorphism_cmd:
+ (string list * binding * mixfix * string) list -> theory -> theory
+ val add_type_constructor:
+ (string * term * string * thm * thm * thm) -> theory -> theory
+ val get_map_tab:
+ theory -> string Symtab.table
+end;
+
+structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
+struct
+
+val beta_ss =
+ HOL_basic_ss
+ addsimps simp_thms
+ addsimps [@{thm beta_cfun}]
+ addsimprocs [@{simproc cont_proc}];
+
+val beta_tac = simp_tac beta_ss;
+
+(******************************************************************************)
+(******************************** theory data *********************************)
+(******************************************************************************)
+
+structure DeflData = Theory_Data
+(
+ type T = term Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ fun merge data = Symtab.merge (K true) data;
+);
+
+structure MapData = Theory_Data
+(
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ fun merge data = Symtab.merge (K true) data;
+);
+
+structure RepData = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
+
+structure IsodeflData = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
+
+structure MapIdData = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ val merge = Thm.merge_thms;
+);
+
+fun add_type_constructor
+ (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) =
+ DeflData.map (Symtab.insert (K true) (tname, defl_const))
+ #> MapData.map (Symtab.insert (K true) (tname, map_name))
+ #> RepData.map (Thm.add_thm REP_thm)
+ #> IsodeflData.map (Thm.add_thm isodefl_thm)
+ #> MapIdData.map (Thm.add_thm map_ID_thm);
+
+val get_map_tab = MapData.get;
+
+
+(******************************************************************************)
+(******************************* building types *******************************)
+(******************************************************************************)
+
+(* ->> is taken from holcf_logic.ML *)
+fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+
+infixr 6 ->>; val (op ->>) = cfunT;
+
+fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+ | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
+
+fun tupleT [] = HOLogic.unitT
+ | tupleT [T] = T
+ | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
+
+val deflT = @{typ "udom alg_defl"};
+
+fun mapT (T as Type (_, Ts)) =
+ Library.foldr cfunT (map (fn T => T ->> T) Ts, T ->> T);
+
+(******************************************************************************)
+(******************************* building terms *******************************)
+(******************************************************************************)
+
+(* builds the expression (v1,v2,..,vn) *)
+fun mk_tuple [] = HOLogic.unit
+| mk_tuple (t::[]) = t
+| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
+
+(* builds the expression (%(v1,v2,..,vn). rhs) *)
+fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
+ | lambda_tuple (v::[]) rhs = Term.lambda v rhs
+ | lambda_tuple (v::vs) rhs =
+ HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
+
+(* continuous application and abstraction *)
+
+fun capply_const (S, T) =
+ Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+
+fun cabs_const (S, T) =
+ Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+
+fun mk_cabs t =
+ let val T = Term.fastype_of t
+ in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+
+(* builds the expression (LAM v. rhs) *)
+fun big_lambda v rhs =
+ cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
+
+(* builds the expression (LAM v1 v2 .. vn. rhs) *)
+fun big_lambdas [] rhs = rhs
+ | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
+
+fun mk_capply (t, u) =
+ let val (S, T) =
+ case Term.fastype_of t of
+ Type(@{type_name "->"}, [S, T]) => (S, T)
+ | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
+ in capply_const (S, T) $ t $ u end;
+
+(* miscellaneous term constructions *)
+
+val mk_trp = HOLogic.mk_Trueprop;
+
+val mk_fst = HOLogic.mk_fst;
+val mk_snd = HOLogic.mk_snd;
+
+fun mk_cont t =
+ let val T = Term.fastype_of t
+ in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
+
+fun mk_fix t =
+ let val (T, _) = dest_cfunT (Term.fastype_of t)
+ in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end;
+
+fun ID_const T = Const (@{const_name ID}, cfunT (T, T));
+
+fun cfcomp_const (T, U, V) =
+ Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V));
+
+fun mk_cfcomp (f, g) =
+ let
+ val (U, V) = dest_cfunT (Term.fastype_of f);
+ val (T, U') = dest_cfunT (Term.fastype_of g);
+ in
+ if U = U'
+ then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
+ else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
+ end;
+
+fun mk_Rep_of T =
+ Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
+
+fun coerce_const T = Const (@{const_name coerce}, T);
+
+fun isodefl_const T =
+ Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
+
+(* splits a cterm into the right and lefthand sides of equality *)
+fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
+
+fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
+
+(******************************************************************************)
+(*************** fixed-point definitions and unfolding theorems ***************)
+(******************************************************************************)
+
+fun add_fixdefs
+ (spec : (binding * term) list)
+ (thy : theory) : (thm list * thm list) * theory =
+ let
+ val binds = map fst spec;
+ val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
+ val functional = lambda_tuple lhss (mk_tuple rhss);
+ val fixpoint = mk_fix (mk_cabs functional);
+
+ (* project components of fixpoint *)
+ fun mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+ val projs = mk_projs lhss fixpoint;
+
+ (* convert parameters to lambda abstractions *)
+ fun mk_eqn (lhs, rhs) =
+ case lhs of
+ Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
+ mk_eqn (f, big_lambda x rhs)
+ | Const _ => Logic.mk_equals (lhs, rhs)
+ | _ => raise TERM ("lhs not of correct form", [lhs, rhs]);
+ val eqns = map mk_eqn projs;
+
+ (* register constant definitions *)
+ val (fixdef_thms, thy) =
+ (PureThy.add_defs false o map Thm.no_attributes)
+ (map (Binding.suffix_name "_def") binds ~~ eqns) thy;
+
+ (* prove applied version of definitions *)
+ fun prove_proj (lhs, rhs) =
+ let
+ val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1;
+ val goal = Logic.mk_equals (lhs, rhs);
+ in Goal.prove_global thy [] [] goal (K tac) end;
+ val proj_thms = map prove_proj projs;
+
+ (* mk_tuple lhss == fixpoint *)
+ fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
+ val tuple_fixdef_thm = foldr1 pair_equalI proj_thms;
+
+ val cont_thm =
+ Goal.prove_global thy [] [] (mk_trp (mk_cont functional))
+ (K (beta_tac 1));
+ val tuple_unfold_thm =
+ (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
+ |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv};
+
+ fun mk_unfold_thms [] thm = []
+ | mk_unfold_thms (n::[]) thm = [(n, thm)]
+ | mk_unfold_thms (n::ns) thm = let
+ val thmL = thm RS @{thm Pair_eqD1};
+ val thmR = thm RS @{thm Pair_eqD2};
+ in (n, thmL) :: mk_unfold_thms ns thmR end;
+ val unfold_binds = map (Binding.suffix_name "_unfold") binds;
+
+ (* register unfold theorems *)
+ val (unfold_thms, thy) =
+ (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+ (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
+ in
+ ((proj_thms, unfold_thms), thy)
+ end;
+
+
+(******************************************************************************)
+(****************** deflation combinators and map functions *******************)
+(******************************************************************************)
+
+fun defl_of_typ
+ (tab : term Symtab.table)
+ (T : typ) : term =
+ let
+ fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+ | is_closed_typ _ = false;
+ fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
+ | defl_of (TVar _) = error ("defl_of_typ: TVar")
+ | defl_of (T as Type (c, Ts)) =
+ case Symtab.lookup tab c of
+ SOME t => Library.foldl mk_capply (t, map defl_of Ts)
+ | NONE => if is_closed_typ T
+ then mk_Rep_of T
+ else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
+ in defl_of T end;
+
+fun map_of_typ
+ (tab : string Symtab.table)
+ (T : typ) : term =
+ let
+ fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+ | is_closed_typ _ = false;
+ fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T)
+ | map_of (T as TVar _) = error ("map_of_typ: TVar")
+ | map_of (T as Type (c, Ts)) =
+ case Symtab.lookup tab c of
+ SOME t => Library.foldl mk_capply (Const (t, mapT T), map map_of Ts)
+ | NONE => if is_closed_typ T
+ then ID_const T
+ else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
+ in map_of T end;
+
+
+(******************************************************************************)
+(* prepare datatype specifications *)
+
+fun read_typ thy str sorts =
+ let
+ val ctxt = ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) sorts;
+ val T = Syntax.read_typ ctxt str;
+ in (T, Term.add_tfreesT T sorts) end;
+
+fun cert_typ sign raw_T sorts =
+ let
+ val T = Type.no_tvars (Sign.certify_typ sign raw_T)
+ handle TYPE (msg, _, _) => error msg;
+ val sorts' = Term.add_tfreesT T sorts;
+ val _ =
+ case duplicates (op =) (map fst sorts') of
+ [] => ()
+ | dups => error ("Inconsistent sort constraints for " ^ commas dups)
+ in (T, sorts') end;
+
+fun gen_domain_isomorphism
+ (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
+ (doms_raw: (string list * binding * mixfix * 'a) list)
+ (thy: theory)
+ : theory =
+ let
+ val _ = Theory.requires thy "Representable" "domain isomorphisms";
+
+ (* this theory is used just for parsing *)
+ val tmp_thy = thy |>
+ Theory.copy |>
+ Sign.add_types (map (fn (tvs, tname, mx, _) =>
+ (tname, length tvs, mx)) doms_raw);
+
+ fun prep_dom thy (vs, t, mx, typ_raw) sorts =
+ let val (typ, sorts') = prep_typ thy typ_raw sorts
+ in ((vs, t, mx, typ), sorts') end;
+
+ val (doms : (string list * binding * mixfix * typ) list,
+ sorts : (string * sort) list) =
+ fold_map (prep_dom tmp_thy) doms_raw [];
+
+ (* domain equations *)
+ fun mk_dom_eqn (vs, tbind, mx, rhs) =
+ let fun arg v = TFree (v, the (AList.lookup (op =) sorts v));
+ in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end;
+ val dom_eqns = map mk_dom_eqn doms;
+
+ (* check for valid type parameters *)
+ val (tyvars, _, _, _)::_ = doms;
+ val new_doms = map (fn (tvs, tname, mx, _) =>
+ let val full_tname = Sign.full_name tmp_thy tname
+ in
+ (case duplicates (op =) tvs of
+ [] =>
+ if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
+ else error ("Mutually recursive domains must have same type parameters")
+ | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
+ " : " ^ commas dups))
+ end) doms;
+ val dom_binds = map (fn (_, tbind, _, _) => tbind) doms;
+
+ (* declare deflation combinator constants *)
+ fun declare_defl_const (vs, tbind, mx, rhs) thy =
+ let
+ val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT);
+ val defl_bind = Binding.suffix_name "_defl" tbind;
+ in
+ Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
+ end;
+ val (defl_consts, thy) = fold_map declare_defl_const doms thy;
+
+ (* defining equations for type combinators *)
+ val defl_tab1 = DeflData.get thy;
+ val defl_tab2 =
+ Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
+ val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
+ val thy = DeflData.put defl_tab' thy;
+ fun mk_defl_spec (lhsT, rhsT) =
+ mk_eqs (defl_of_typ defl_tab' lhsT,
+ defl_of_typ defl_tab' rhsT);
+ val defl_specs = map mk_defl_spec dom_eqns;
+
+ (* register recursive definition of deflation combinators *)
+ val defl_binds = map (Binding.suffix_name "_defl") dom_binds;
+ val ((defl_apply_thms, defl_unfold_thms), thy) =
+ add_fixdefs (defl_binds ~~ defl_specs) thy;
+
+ (* define types using deflation combinators *)
+ fun make_repdef ((vs, tbind, mx, _), defl_const) thy =
+ let
+ fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
+ val reps = map (mk_Rep_of o tfree) vs;
+ val defl = Library.foldl mk_capply (defl_const, reps);
+ val ((_, _, _, {REP, ...}), thy) =
+ Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
+ in
+ (REP, thy)
+ end;
+ val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
+ val thy = RepData.map (fold Thm.add_thm REP_thms) thy;
+
+ (* prove REP equations *)
+ fun mk_REP_eq_thm (lhsT, rhsT) =
+ let
+ val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
+ val REP_simps = RepData.get thy;
+ val tac =
+ simp_tac (HOL_basic_ss addsimps REP_simps) 1
+ THEN resolve_tac defl_unfold_thms 1;
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+ val REP_eq_thms = map mk_REP_eq_thm dom_eqns;
+
+ (* register REP equations *)
+ val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds;
+ val (_, thy) = thy |>
+ (PureThy.add_thms o map Thm.no_attributes)
+ (REP_eq_binds ~~ REP_eq_thms);
+
+ (* define rep/abs functions *)
+ fun mk_rep_abs (tbind, (lhsT, rhsT)) thy =
+ let
+ val rep_type = cfunT (lhsT, rhsT);
+ val abs_type = cfunT (rhsT, lhsT);
+ val rep_bind = Binding.suffix_name "_rep" tbind;
+ val abs_bind = Binding.suffix_name "_abs" tbind;
+ val (rep_const, thy) = thy |>
+ Sign.declare_const ((rep_bind, rep_type), NoSyn);
+ val (abs_const, thy) = thy |>
+ Sign.declare_const ((abs_bind, abs_type), NoSyn);
+ val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type);
+ val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type);
+ val ([rep_def, abs_def], thy) = thy |>
+ (PureThy.add_defs false o map Thm.no_attributes)
+ [(Binding.suffix_name "_rep_def" tbind, rep_eqn),
+ (Binding.suffix_name "_abs_def" tbind, abs_eqn)];
+ in
+ (((rep_const, abs_const), (rep_def, abs_def)), thy)
+ end;
+ val ((rep_abs_consts, rep_abs_defs), thy) = thy
+ |> fold_map mk_rep_abs (dom_binds ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ (* prove isomorphism and isodefl rules *)
+ fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
+ let
+ fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]);
+ val rep_iso_thm = make @{thm domain_rep_iso};
+ val abs_iso_thm = make @{thm domain_abs_iso};
+ val isodefl_thm = make @{thm isodefl_abs_rep};
+ val rep_iso_bind = Binding.name "rep_iso";
+ val abs_iso_bind = Binding.name "abs_iso";
+ val isodefl_bind = Binding.name "isodefl_abs_rep";
+ val (_, thy) = thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> (PureThy.add_thms o map Thm.no_attributes)
+ [(rep_iso_bind, rep_iso_thm),
+ (abs_iso_bind, abs_iso_thm),
+ (isodefl_bind, isodefl_thm)]
+ ||> Sign.parent_path;
+ in
+ (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
+ end;
+ val ((iso_thms, isodefl_abs_rep_thms), thy) = thy
+ |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
+ |>> ListPair.unzip;
+
+ (* declare map functions *)
+ fun declare_map_const (tbind, (lhsT, rhsT)) thy =
+ let
+ val map_type = mapT lhsT;
+ val map_bind = Binding.suffix_name "_map" tbind;
+ in
+ Sign.declare_const ((map_bind, map_type), NoSyn) thy
+ end;
+ val (map_consts, thy) = thy |>
+ fold_map declare_map_const (dom_binds ~~ dom_eqns);
+
+ (* defining equations for map functions *)
+ val map_tab1 = MapData.get thy;
+ val map_tab2 =
+ Symtab.make (map (fst o dest_Type o fst) dom_eqns
+ ~~ map (fst o dest_Const) map_consts);
+ val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2);
+ val thy = MapData.put map_tab' thy;
+ fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) =
+ let
+ val lhs = map_of_typ map_tab' lhsT;
+ val body = map_of_typ map_tab' rhsT;
+ val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+ in mk_eqs (lhs, rhs) end;
+ val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns);
+
+ (* register recursive definition of map functions *)
+ val map_binds = map (Binding.suffix_name "_map") dom_binds;
+ val ((map_apply_thms, map_unfold_thms), thy) =
+ add_fixdefs (map_binds ~~ map_specs) thy;
+
+ (* prove isodefl rules for map functions *)
+ val isodefl_thm =
+ let
+ fun unprime a = Library.unprefix "'" a;
+ fun mk_d (TFree (a, _)) = Free ("d" ^ unprime a, deflT);
+ fun mk_f (T as TFree (a, _)) = Free ("f" ^ unprime a, T ->> T);
+ fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
+ fun mk_goal ((map_const, defl_const), (T as Type (c, Ts), rhsT)) =
+ let
+ val map_term = Library.foldl mk_capply (map_const, map mk_f Ts);
+ val defl_term = Library.foldl mk_capply (defl_const, map mk_d Ts);
+ in isodefl_const T $ map_term $ defl_term end;
+ val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
+ val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns);
+ val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
+ val start_thms =
+ @{thm split_def} :: defl_apply_thms @ map_apply_thms;
+ val adm_rules =
+ @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
+ val bottom_rules =
+ @{thms fst_strict snd_strict isodefl_bottom simp_thms};
+ val isodefl_rules =
+ @{thms conjI isodefl_ID_REP}
+ @ isodefl_abs_rep_thms
+ @ IsodeflData.get thy;
+ fun tacf {prems, ...} = EVERY
+ [simp_tac (HOL_basic_ss addsimps start_thms) 1,
+ (* FIXME: how reliable is unification here? *)
+ (* Maybe I should instantiate the rule. *)
+ rtac @{thm parallel_fix_ind} 1,
+ REPEAT (resolve_tac adm_rules 1),
+ simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
+ simp_tac beta_ss 1,
+ simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
+ REPEAT (etac @{thm conjE} 1),
+ REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)];
+ in
+ Goal.prove_global thy [] assms goal tacf
+ end;
+ val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
+ fun conjuncts [] thm = []
+ | conjuncts (n::[]) thm = [(n, thm)]
+ | conjuncts (n::ns) thm = let
+ val thmL = thm RS @{thm conjunct1};
+ val thmR = thm RS @{thm conjunct2};
+ in (n, thmL):: conjuncts ns thmR end;
+ val (isodefl_thms, thy) = thy |>
+ (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+ (conjuncts isodefl_binds isodefl_thm);
+ val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
+
+ (* prove map_ID theorems *)
+ fun prove_map_ID_thm
+ (((map_const, (lhsT, _)), REP_thm), isodefl_thm) =
+ let
+ val Ts = snd (dest_Type lhsT);
+ val lhs = Library.foldl mk_capply (map_const, map ID_const Ts);
+ val goal = mk_eqs (lhs, ID_const lhsT);
+ val tac = EVERY
+ [rtac @{thm isodefl_REP_imp_ID} 1,
+ stac REP_thm 1,
+ rtac isodefl_thm 1,
+ REPEAT (rtac @{thm isodefl_ID_REP} 1)];
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+ val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds;
+ val map_ID_thms =
+ map prove_map_ID_thm
+ (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
+ val (_, thy) = thy |>
+ (PureThy.add_thms o map Thm.no_attributes)
+ (map_ID_binds ~~ map_ID_thms);
+ val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
+
+ (* define copy combinators *)
+ val new_dts =
+ map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
+ val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns);
+ val copy_arg = Free ("f", copy_arg_type);
+ val copy_args =
+ let fun mk_copy_args [] t = []
+ | mk_copy_args (_::[]) t = [t]
+ | mk_copy_args (_::xs) t =
+ mk_fst t :: mk_copy_args xs (mk_snd t);
+ in mk_copy_args doms copy_arg end;
+ fun copy_of_dtyp (T, dt) =
+ if DatatypeAux.is_rec_type dt
+ then copy_of_dtyp' (T, dt)
+ else ID_const T
+ and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i
+ | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T
+ | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) =
+ case Symtab.lookup map_tab' c of
+ SOME f =>
+ Library.foldl mk_capply
+ (Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds))
+ | NONE =>
+ (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T);
+ fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy =
+ let
+ val copy_type = copy_arg_type ->> (lhsT ->> lhsT);
+ val copy_bind = Binding.suffix_name "_copy" tbind;
+ val (copy_const, thy) = thy |>
+ Sign.declare_const ((copy_bind, copy_type), NoSyn);
+ val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT;
+ val body = copy_of_dtyp (rhsT, dtyp);
+ val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+ val rhs = big_lambda copy_arg comp;
+ val eqn = Logic.mk_equals (copy_const, rhs);
+ val ([copy_def], thy) =
+ thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> (PureThy.add_defs false o map Thm.no_attributes)
+ [(Binding.name "copy_def", eqn)]
+ ||> Sign.parent_path;
+ in ((copy_const, copy_def), thy) end;
+ val ((copy_consts, copy_defs), thy) = thy
+ |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
+ |>> ListPair.unzip;
+
+ (* define combined copy combinator *)
+ val ((c_const, c_def_thms), thy) =
+ if length doms = 1
+ then ((hd copy_consts, []), thy)
+ else
+ let
+ val c_type = copy_arg_type ->> copy_arg_type;
+ val c_name = space_implode "_" (map Binding.name_of dom_binds);
+ val c_bind = Binding.name (c_name ^ "_copy");
+ val c_body =
+ mk_tuple (map (mk_capply o rpair copy_arg) copy_consts);
+ val c_rhs = big_lambda copy_arg c_body;
+ val (c_const, thy) =
+ Sign.declare_const ((c_bind, c_type), NoSyn) thy;
+ val c_eqn = Logic.mk_equals (c_const, c_rhs);
+ val (c_def_thms, thy) =
+ thy
+ |> Sign.add_path c_name
+ |> (PureThy.add_defs false o map Thm.no_attributes)
+ [(Binding.name "copy_def", c_eqn)]
+ ||> Sign.parent_path;
+ in ((c_const, c_def_thms), thy) end;
+
+ (* fixed-point lemma for combined copy combinator *)
+ val fix_copy_lemma =
+ let
+ fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) =
+ Library.foldl mk_capply (map_const, map ID_const Ts);
+ val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
+ val goal = mk_eqs (mk_fix c_const, rhs);
+ val rules =
+ [@{thm pair_collapse}, @{thm split_def}]
+ @ map_apply_thms
+ @ c_def_thms @ copy_defs
+ @ MapIdData.get thy;
+ val tac = simp_tac (beta_ss addsimps rules) 1;
+ in
+ Goal.prove_global thy [] [] goal (K tac)
+ end;
+
+ (* prove reach lemmas *)
+ val reach_thm_projs =
+ let fun mk_projs (x::[]) t = [(x, t)]
+ | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+ in mk_projs dom_binds (mk_fix c_const) end;
+ fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy =
+ let
+ val x = Free ("x", lhsT);
+ val goal = mk_eqs (mk_capply (t, x), x);
+ val rules =
+ fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1};
+ val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+ val reach_thm = Goal.prove_global thy [] [] goal (K tac);
+ in
+ thy
+ |> Sign.add_path (Binding.name_of bind)
+ |> yield_singleton (PureThy.add_thms o map Thm.no_attributes)
+ (Binding.name "reach", reach_thm)
+ ||> Sign.parent_path
+ end;
+ val (reach_thms, thy) = thy |>
+ fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
+
+ in
+ thy
+ end;
+
+val domain_isomorphism = gen_domain_isomorphism cert_typ;
+val domain_isomorphism_cmd = gen_domain_isomorphism read_typ;
+
+(******************************************************************************)
+(******************************** outer syntax ********************************)
+(******************************************************************************)
+
+local
+
+structure P = OuterParse and K = OuterKeyword
+
+val parse_domain_iso : (string list * binding * mixfix * string) parser =
+ (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ))
+ >> (fn (((vs, t), mx), rhs) => (vs, t, mx, rhs));
+
+val parse_domain_isos = P.and_list1 parse_domain_iso;
+
+in
+
+val _ =
+ OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
+ (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
+
+end;
+
+end;
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Fri Nov 20 10:40:30 2009 +0100
@@ -7,12 +7,14 @@
signature DOMAIN_SYNTAX =
sig
val calc_syntax:
+ bool ->
typ ->
(string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list ->
(binding * typ * mixfix) list * ast Syntax.trrule list
val add_syntax:
+ bool ->
string ->
((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list ->
@@ -27,155 +29,177 @@
infixr 5 -->; infixr 6 ->>;
fun calc_syntax
- (dtypeprod : typ)
- ((dname : string, typevars : typ list),
- (cons': (binding * (bool * binding option * typ) list * mixfix) list))
+ (definitional : bool)
+ (dtypeprod : typ)
+ ((dname : string, typevars : typ list),
+ (cons': (binding * (bool * binding option * typ) list * mixfix) list))
: (binding * typ * mixfix) list * ast Syntax.trrule list =
- let
- (* ----- constants concerning the isomorphism ------------------------------- *)
+ let
+(* ----- constants concerning the isomorphism ------------------------------- *)
+ local
+ fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+ fun prod (_,args,_) = case args of [] => oneT
+ | _ => foldr1 mk_sprodT (map opt_lazy args);
+ fun freetvar s = let val tvar = mk_TFree s in
+ if tvar mem typevars then freetvar ("t"^s) else tvar end;
+ fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
+ in
+ val dtype = Type(dname,typevars);
+ val dtype2 = foldr1 mk_ssumT (map prod cons');
+ val dnam = Long_Name.base_name dname;
+ fun dbind s = Binding.name (dnam ^ s);
+ val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
+ end;
- local
- fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
- fun prod (_,args,_) = case args of [] => oneT
- | _ => foldr1 mk_sprodT (map opt_lazy args);
- fun freetvar s = let val tvar = mk_TFree s in
- if tvar mem typevars then freetvar ("t"^s) else tvar end;
- fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
- in
- val dtype = Type(dname,typevars);
- val dtype2 = foldr1 mk_ssumT (map prod cons');
- val dnam = Long_Name.base_name dname;
- fun dbind s = Binding.name (dnam ^ s);
- val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn);
- val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
- val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
- end;
+(* ----- constants concerning constructors, discriminators, and selectors --- *)
+
+ local
+ val escape = let
+ fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
+ else c::esc cs
+ | esc [] = []
+ in implode o esc o Symbol.explode end;
- (* ----- constants concerning constructors, discriminators, and selectors --- *)
+ fun dis_name_ con =
+ Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+ fun mat_name_ con =
+ Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+ fun pat_name_ con =
+ Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+ fun con (name,args,mx) =
+ (name, List.foldr (op ->>) dtype (map third args), mx);
+ fun dis (con,args,mx) =
+ (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
+ (* strictly speaking, these constants have one argument,
+ but the mixfix (without arguments) is introduced only
+ to generate parse rules for non-alphanumeric names*)
+ fun freetvar s n =
+ let val tvar = mk_TFree (s ^ string_of_int n)
+ in if tvar mem typevars then freetvar ("t"^s) n else tvar end;
- local
- val escape = let
- fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
- else c::esc cs
- | esc [] = []
- in implode o esc o Symbol.explode end;
- fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
- fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
- fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
- fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
- fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
- Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
- (* strictly speaking, these constants have one argument,
- but the mixfix (without arguments) is introduced only
- to generate parse rules for non-alphanumeric names*)
- fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in
- if tvar mem typevars then freetvar ("t"^s) n else tvar end;
- fun mk_matT (a,bs,c) = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
- fun mat (con,args,mx) = (mat_name_ con,
- mk_matT(dtype, map third args, freetvar "t" 1),
- Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
- fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
- fun sel (con,args,mx) = map_filter sel1 args;
- fun mk_patT (a,b) = a ->> mk_maybeT b;
- fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
- fun pat (con,args,mx) = (pat_name_ con,
- (mapn pat_arg_typ 1 args)
- --->
- mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
- Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+ fun mk_matT (a,bs,c) =
+ a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+ fun mat (con,args,mx) =
+ (mat_name_ con,
+ mk_matT(dtype, map third args, freetvar "t" 1),
+ Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
+ fun sel1 (_,sel,typ) =
+ Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+ fun sel (con,args,mx) = map_filter sel1 args;
+ fun mk_patT (a,b) = a ->> mk_maybeT b;
+ fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
+ fun pat (con,args,mx) =
+ (pat_name_ con,
+ (mapn pat_arg_typ 1 args)
+ --->
+ mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
+ Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+ in
+ val consts_con = map con cons';
+ val consts_dis = map dis cons';
+ val consts_mat = map mat cons';
+ val consts_pat = map pat cons';
+ val consts_sel = maps sel cons';
+ end;
+
+(* ----- constants concerning induction ------------------------------------- *)
+
+ val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
+
+(* ----- case translation --------------------------------------------------- *)
+ local open Syntax in
+ local
+ fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
+ fun expvar n = Variable ("e"^(string_of_int n));
+ fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+ (string_of_int m));
+ fun argvars n args = mapn (argvar n) 1 args;
+ fun app s (l,r) = mk_appl (Constant s) [l,r];
+ val cabs = app "_cabs";
+ val capp = app "Rep_CFun";
+ fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+ fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+ fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
+ fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+
+ fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
+ fun app_pat x = mk_appl (Constant "_pat") [x];
+ fun args_list [] = Constant "_noargs"
+ | args_list xs = foldr1 (app "_args") xs;
+ in
+ val case_trans =
+ ParsePrintRule
+ (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
+ capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
+
+ fun one_abscon_trans n (con,mx,args) =
+ ParsePrintRule
+ (cabs (con1 n (con,mx,args), expvar n),
+ Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
+ val abscon_trans = mapn one_abscon_trans 1 cons';
+
+ fun one_case_trans (con,args,mx) =
+ let
+ val cname = c_ast con mx;
+ val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
+ val ns = 1 upto length args;
+ val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
+ val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
+ val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
in
- val consts_con = map con cons';
- val consts_dis = map dis cons';
- val consts_mat = map mat cons';
- val consts_pat = map pat cons';
- val consts_sel = maps sel cons';
- end;
-
- (* ----- constants concerning induction ------------------------------------- *)
-
- val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
- val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
-
- (* ----- case translation --------------------------------------------------- *)
-
- local open Syntax in
- local
- fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
- (string_of_int m));
- fun argvars n args = mapn (argvar n) 1 args;
- fun app s (l,r) = mk_appl (Constant s) [l,r];
- val cabs = app "_cabs";
- val capp = app "Rep_CFun";
- fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
- fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
- fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
- fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+ [ParseRule (app_pat (Library.foldl capp (cname, xs)),
+ mk_appl pname (map app_pat xs)),
+ ParseRule (app_var (Library.foldl capp (cname, xs)),
+ app_var (args_list xs)),
+ PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
+ app "_match" (mk_appl pname ps, args_list vs))]
+ end;
+ val Case_trans = maps one_case_trans cons';
+ end;
+ end;
+ val optional_consts =
+ if definitional then [] else [const_rep, const_abs, const_copy];
- fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
- fun app_pat x = mk_appl (Constant "_pat") [x];
- fun args_list [] = Constant "_noargs"
- | args_list xs = foldr1 (app "_args") xs;
- in
- val case_trans =
- ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
- capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
-
- fun one_abscon_trans n (con,mx,args) =
- ParsePrintRule
- (cabs (con1 n (con,mx,args), expvar n),
- Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
- val abscon_trans = mapn one_abscon_trans 1 cons';
-
- fun one_case_trans (con,args,mx) =
- let
- val cname = c_ast con mx;
- val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
- val ns = 1 upto length args;
- val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
- val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
- val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
- in
- [ParseRule (app_pat (Library.foldl capp (cname, xs)),
- mk_appl pname (map app_pat xs)),
- ParseRule (app_var (Library.foldl capp (cname, xs)),
- app_var (args_list xs)),
- PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
- app "_match" (mk_appl pname ps, args_list vs))]
- end;
- val Case_trans = maps one_case_trans cons';
- end;
- end;
-
- in ([const_rep, const_abs, const_when, const_copy] @
- consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
- [const_take, const_finite],
- (case_trans::(abscon_trans @ Case_trans)))
- end; (* let *)
+ in (optional_consts @ [const_when] @
+ consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
+ [const_take, const_finite],
+ (case_trans::(abscon_trans @ Case_trans)))
+ end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
fun add_syntax
- (comp_dnam : string)
- (eqs' : ((string * typ list) *
- (binding * (bool * binding option * typ) list * mixfix) list) list)
- (thy'' : theory) =
- let
- val dtypes = map (Type o fst) eqs';
- val boolT = HOLogic.boolT;
- val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
- val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
- val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
- val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
- in thy'' |> ContConsts.add_consts_i (maps fst ctt @
- (if length eqs'>1 then [const_copy] else[])@
- [const_bisim])
- |> Sign.add_trrules_i (maps snd ctt)
- end; (* let *)
+ (definitional : bool)
+ (comp_dnam : string)
+ (eqs' : ((string * typ list) *
+ (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (thy'' : theory) =
+ let
+ val dtypes = map (Type o fst) eqs';
+ val boolT = HOLogic.boolT;
+ val funprod =
+ foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod =
+ foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val const_copy =
+ (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+ val const_bisim =
+ (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+ val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list =
+ map (calc_syntax definitional funprod) eqs';
+ in thy''
+ |> ContConsts.add_consts_i
+ (maps fst ctt @
+ (if length eqs'>1 andalso not definitional
+ then [const_copy] else []) @
+ [const_bisim])
+ |> Sign.add_trrules_i (maps snd ctt)
+ end; (* let *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Nov 20 10:40:30 2009 +0100
@@ -141,6 +141,8 @@
val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
val pg = pg' thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
+
(* ----- getting the axioms and definitions --------------------------------- *)
@@ -599,7 +601,8 @@
val lhs = dc_copy`%"f"`(con_app con args);
fun one_rhs arg =
if DatatypeAux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+ then Domain_Axioms.copy_of_dtyp map_tab
+ (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
else (%# arg);
val rhs = con_app2 con one_rhs args;
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
@@ -660,6 +663,7 @@
fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
val global_ctxt = ProofContext.init thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
@@ -727,7 +731,8 @@
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
if DatatypeAux.is_rec_type (dtyp_of arg)
- then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
+ then Domain_Axioms.copy_of_dtyp map_tab
+ mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
val rhs = con_app2 con one_rhs args;
@@ -993,7 +998,7 @@
handle THM _ =>
(warning "Induction proofs failed (THM raised)."; ([], TrueI))
| ERROR _ =>
- (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
+ (warning "Cannot prove induction rule"; ([], TrueI));
end; (* local *)
--- a/src/HOLCF/Tools/repdef.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Tools/repdef.ML Fri Nov 20 10:40:30 2009 +0100
@@ -172,7 +172,7 @@
((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
val _ =
- OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_goal
+ OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
(repdef_decl >>
(Toplevel.print oo (Toplevel.theory o mk_repdef)));
--- a/src/HOLCF/Up.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/Up.thy Fri Nov 20 10:40:30 2009 +0100
@@ -303,6 +303,9 @@
lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
unfolding u_map_def by simp
+lemma u_map_ID: "u_map\<cdot>ID = ID"
+unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
+
lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
by (induct p) simp_all
--- a/src/HOLCF/UpperPD.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/UpperPD.thy Fri Nov 20 10:40:30 2009 +0100
@@ -466,6 +466,9 @@
lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: upper_pd_induct, simp_all)
+lemma upper_map_ID: "upper_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def upper_map_ident)
+
lemma upper_map_map:
"upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
by (induct xs rule: upper_pd_induct, simp_all)
--- a/src/HOLCF/ex/Domain_Proofs.thy Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Fri Nov 20 10:40:30 2009 +0100
@@ -16,8 +16,8 @@
datatypes:
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
- and 'a bar = Bar (lazy 'a) (lazy "'a baz")
- and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd")
+ and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
+ and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
*)
@@ -28,47 +28,47 @@
text {* Start with the one-step non-recursive version *}
definition
- foo_bar_baz_typF ::
+ foo_bar_baz_deflF ::
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
where
- "foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3).
- ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))"
+ "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3).
+ ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+ , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>REP(tr))
+ , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>REP(tr)))))"
-lemma foo_bar_baz_typF_beta:
- "foo_bar_baz_typF\<cdot>a\<cdot>t =
- ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t))))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
- , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))"
-unfolding foo_bar_baz_typF_def
-by (simp add: csplit_def cfst_def csnd_def)
+lemma foo_bar_baz_deflF_beta:
+ "foo_bar_baz_deflF\<cdot>a\<cdot>t =
+ ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+ , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>REP(tr))
+ , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>REP(tr)))"
+unfolding foo_bar_baz_deflF_def
+by (simp add: split_def)
text {* Individual type combinators are projected from the fixed point. *}
-definition foo_typ :: "TypeRep \<rightarrow> TypeRep"
-where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))"
+definition foo_defl :: "TypeRep \<rightarrow> TypeRep"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
-definition bar_typ :: "TypeRep \<rightarrow> TypeRep"
-where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition bar_defl :: "TypeRep \<rightarrow> TypeRep"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
-definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
-where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition baz_defl :: "TypeRep \<rightarrow> TypeRep"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
text {* Unfold rules for each combinator. *}
-lemma foo_typ_unfold:
- "foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma foo_defl_unfold:
+ "foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>REP(tr))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>REP(tr))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
how the fixrec package works."
@@ -79,13 +79,13 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}"
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
-pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
-pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>REP('a)}"
by (simp_all add: adm_in_deflation)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
@@ -97,10 +97,10 @@
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))"
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
-where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<cdot>REP('a))"
+where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -120,10 +120,10 @@
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))"
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
-where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<cdot>REP('a))"
+where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -143,10 +143,10 @@
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))"
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
-where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<cdot>REP('a))"
+where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>REP('a))"
instance
apply (rule typedef_rep_class)
@@ -161,7 +161,7 @@
text {* Prove REP rules using lemma @{text typedef_REP}. *}
-lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)"
+lemma REP_foo: "REP('a foo) = foo_defl\<cdot>REP('a)"
apply (rule typedef_REP)
apply (rule type_definition_foo)
apply (rule below_foo_def)
@@ -169,7 +169,7 @@
apply (rule prj_foo_def)
done
-lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)"
+lemma REP_bar: "REP('a bar) = bar_defl\<cdot>REP('a)"
apply (rule typedef_REP)
apply (rule type_definition_bar)
apply (rule below_bar_def)
@@ -177,7 +177,7 @@
apply (rule prj_bar_def)
done
-lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)"
+lemma REP_baz: "REP('a baz) = baz_defl\<cdot>REP('a)"
apply (rule typedef_REP)
apply (rule type_definition_baz)
apply (rule below_baz_def)
@@ -189,15 +189,15 @@
lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule foo_typ_unfold)
+by (rule foo_defl_unfold)
-lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
+lemma REP_bar': "REP('a bar) = REP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule bar_typ_unfold)
+by (rule bar_defl_unfold)
-lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
+lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule baz_typ_unfold)
+by (rule baz_defl_unfold)
(********************************************************************)
@@ -206,41 +206,56 @@
text {* Define them all using @{text coerce}! *}
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-where "foo_rep = coerce"
+where "foo_rep \<equiv> coerce"
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
-where "foo_abs = coerce"
+where "foo_abs \<equiv> coerce"
+
+definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
+where "bar_rep \<equiv> coerce"
+
+definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
+where "bar_abs \<equiv> coerce"
-definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
-where "bar_rep = coerce"
+definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
+where "baz_rep \<equiv> coerce"
+
+definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
+where "baz_abs \<equiv> coerce"
+
+text {* Prove isomorphism rules. *}
-definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
-where "bar_abs = coerce"
+lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def])
-definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
-where "baz_rep = coerce"
+lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def])
-definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
-where "baz_abs = coerce"
+lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def])
+
+lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def])
text {* Prove isodefl rules using @{text isodefl_coerce}. *}
lemma isodefl_foo_abs:
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
-unfolding foo_abs_def foo_rep_def
-by (rule isodefl_coerce [OF REP_foo'])
+by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def])
lemma isodefl_bar_abs:
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
-unfolding bar_abs_def bar_rep_def
-by (rule isodefl_coerce [OF REP_bar'])
+by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def])
lemma isodefl_baz_abs:
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
-unfolding baz_abs_def baz_rep_def
-by (rule isodefl_coerce [OF REP_baz'])
-
-text {* TODO: prove iso predicate for rep and abs. *}
+by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def])
(********************************************************************)
@@ -253,20 +268,20 @@
definition
foo_bar_baz_mapF ::
- "('a \<rightarrow> 'b)
- \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)
- \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)"
+ "('a \<rightarrow> 'b) \<rightarrow>
+ ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
+ ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
where
- "foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3).
+ "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
(
foo_abs oo
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
oo foo_rep
,
- bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep
+ bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
,
- baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
- ))"
+ baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
+ )))"
lemma foo_bar_baz_mapF_beta:
"foo_bar_baz_mapF\<cdot>f\<cdot>d =
@@ -275,12 +290,12 @@
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
oo foo_rep
,
- bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep
+ bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
,
- baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
+ baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
)"
unfolding foo_bar_baz_mapF_def
-by (simp add: csplit_def cfst_def csnd_def)
+by (simp add: split_def)
text {* Individual map functions are projected from the fixed point. *}
@@ -290,7 +305,7 @@
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
-definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)"
+definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
text {* Prove isodefl rules for all map functions simultaneously. *}
@@ -298,17 +313,16 @@
lemma isodefl_foo_bar_baz:
assumes isodefl_d: "isodefl d t"
shows
- "isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and>
- isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and>
- isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)"
+ "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
+ isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
+ isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
apply (simp add: foo_map_def bar_map_def baz_map_def)
- apply (simp add: foo_typ_def bar_typ_def baz_typ_def)
- apply (rule parallel_fix_ind
- [where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
+ apply (simp add: foo_defl_def bar_defl_def baz_defl_def)
+ apply (rule parallel_fix_ind)
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
apply (simp only: foo_bar_baz_mapF_beta
- foo_bar_baz_typF_beta
+ foo_bar_baz_deflF_beta
fst_conv snd_conv)
apply (elim conjE)
apply (intro
@@ -316,7 +330,8 @@
isodefl_foo_abs
isodefl_bar_abs
isodefl_baz_abs
- isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex
+ isodefl_ssum isodefl_sprod isodefl_ID_REP
+ isodefl_u isodefl_convex isodefl_cfun
isodefl_d
)
apply assumption+
@@ -353,23 +368,63 @@
subsection {* Step 5: Define copy functions, prove reach lemmas *}
-definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID"
-definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))"
-definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))"
-definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))"
+text {* Define copy functions just like the old domain package does. *}
+
+definition
+ foo_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a foo \<rightarrow> 'a foo"
+where
+ "foo_copy = (\<Lambda> p. foo_abs oo
+ ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
+ oo foo_rep)"
+
+definition
+ bar_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a bar \<rightarrow> 'a bar"
+where
+ "bar_copy = (\<Lambda> p. bar_abs oo
+ u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
+
+definition
+ baz_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ 'a baz \<rightarrow> 'a baz"
+where
+ "baz_copy = (\<Lambda> p. baz_abs oo
+ u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
+
+definition
+ foo_bar_baz_copy ::
+ "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+ ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
+where
+ "foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))"
lemma fix_foo_bar_baz_copy:
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)"
-unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def
-by simp
+unfolding foo_map_def bar_map_def baz_map_def
+apply (subst beta_cfun, simp)+
+apply (subst pair_collapse)+
+apply (rule cfun_arg_cong)
+unfolding foo_bar_baz_mapF_def split_def
+unfolding foo_bar_baz_copy_def
+unfolding foo_copy_def bar_copy_def baz_copy_def
+apply (subst beta_cfun, simp)+
+apply (rule refl)
+done
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding foo_map_ID by (rule ID1)
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding bar_map_ID by (rule ID1)
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding baz_map_ID by (rule ID1)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/New_Domain.thy Fri Nov 20 10:40:30 2009 +0100
@@ -0,0 +1,92 @@
+(* Title: HOLCF/ex/New_Domain.thy
+ Author: Brian Huffman
+*)
+
+header {* Definitional domain package *}
+
+theory New_Domain
+imports HOLCF
+begin
+
+text {*
+ The definitional domain package only works with representable domains,
+ i.e. types in class @{text rep}.
+*}
+
+defaultsort rep
+
+text {*
+ Provided that @{text rep} is the default sort, the @{text new_domain}
+ package should work with any type definition supported by the old
+ domain package.
+*}
+
+new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+
+text {*
+ The difference is that the new domain package is completely
+ definitional, and does not generate any axioms. The following type
+ and constant definitions are not produced by the old domain package.
+*}
+
+thm type_definition_llist
+thm llist_abs_def llist_rep_def
+
+text {*
+ The new domain package also adds support for indirect recursion with
+ user-defined datatypes. This definition of a tree datatype uses
+ indirect recursion through the lazy list type constructor.
+*}
+
+new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+
+text {*
+ For indirect-recursive definitions, the domain package is not able to
+ generate a high-level induction rule. (It produces a warning
+ message instead.) The low-level reach lemma (now proved as a
+ theorem, no longer generated as an axiom) can be used to derive
+ other induction rules.
+*}
+
+thm ltree.reach
+
+text {*
+ The definition of the copy function uses map functions associated with
+ each type constructor involved in the definition. A map function
+ for the lazy list type has been generated by the new domain package.
+*}
+
+thm ltree.copy_def
+thm llist_map_def
+
+lemma ltree_induct:
+ fixes P :: "'a ltree \<Rightarrow> bool"
+ assumes adm: "adm P"
+ assumes bot: "P \<bottom>"
+ assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
+ assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
+ shows "P x"
+proof -
+ have "\<forall>x. P (fix\<cdot>ltree_copy\<cdot>x)"
+ proof (rule fix_ind)
+ show "adm (\<lambda>a. \<forall>x. P (a\<cdot>x))"
+ by (simp add: adm_subst [OF _ adm])
+ next
+ show "\<forall>x. P (\<bottom>\<cdot>x)"
+ by (simp add: bot)
+ next
+ fix f :: "'a ltree \<rightarrow> 'a ltree"
+ assume f: "\<forall>x. P (f\<cdot>x)"
+ show "\<forall>x. P (ltree_copy\<cdot>f\<cdot>x)"
+ apply (rule allI)
+ apply (case_tac x)
+ apply (simp add: bot)
+ apply (simp add: Leaf)
+ apply (simp add: Branch [OF f])
+ done
+ qed
+ thus ?thesis
+ by (simp add: ltree.reach)
+qed
+
+end
--- a/src/HOLCF/ex/ROOT.ML Thu Nov 19 19:42:54 2009 +0100
+++ b/src/HOLCF/ex/ROOT.ML Fri Nov 20 10:40:30 2009 +0100
@@ -4,4 +4,5 @@
*)
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
- "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs"];
+ "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
+ "New_Domain"];