--- a/src/HOL/Codatatype/BNF_Def.thy Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy Wed Sep 12 15:01:25 2012 +0200
@@ -51,7 +51,7 @@
moreover have "f1 (fst a') = f2 (snd a')"
using a' unfolding csquare_def thePull_def by auto
ultimately show "\<exists> ja'. ?phi a' ja'"
- using assms unfolding wppull_def by auto
+ using assms unfolding wppull_def by blast
qed
lemma wpull_wppull:
@@ -64,7 +64,7 @@
then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
using wp unfolding wpull_def by blast
show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
- apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
+ apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
qed
lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
@@ -87,8 +87,7 @@
definition "pick_middle P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
lemma pick_middle:
-assumes "(a,c) \<in> P O Q"
-shows "(a, pick_middle P Q a c) \<in> P \<and> (pick_middle P Q a c, c) \<in> Q"
+"(a,c) \<in> P O Q \<Longrightarrow> (a, pick_middle P Q a c) \<in> P \<and> (pick_middle P Q a c, c) \<in> Q"
unfolding pick_middle_def apply(rule someI_ex)
using assms unfolding relcomp_def by auto
@@ -96,7 +95,8 @@
definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)"
lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
-by (metis assms fstO_def pick_middle surjective_pairing)
+unfolding fstO_def
+by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
unfolding comp_def fstO_def by simp
@@ -105,11 +105,12 @@
unfolding comp_def sndO_def by simp
lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
-by (metis assms sndO_def pick_middle surjective_pairing)
+unfolding sndO_def
+by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2])
lemma csquare_fstO_sndO:
"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
-unfolding csquare_def fstO_def sndO_def using pick_middle by auto
+unfolding csquare_def fstO_def sndO_def using pick_middle by simp
lemma wppull_fstO_sndO:
shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
--- a/src/HOL/Codatatype/BNF_FP.thy Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Wed Sep 12 15:01:25 2012 +0200
@@ -80,16 +80,24 @@
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
by blast
+lemma obj_sumE_f':
+"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P"
+by (cases x) blast+
+
lemma obj_sumE_f:
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
-by (metis sum.exhaust)
+by (rule allI) (rule obj_sumE_f')
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (cases s) auto
+lemma obj_sum_step':
+"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f (Inr x) \<longrightarrow> P"
+by (cases x) blast+
+
lemma obj_sum_step:
- "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
-by (metis obj_sumE)
+"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
+by (rule allI) (rule obj_sum_step')
lemma sum_case_if:
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
--- a/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 15:01:25 2012 +0200
@@ -278,12 +278,10 @@
(* pick according to the weak pullback *)
definition pickWP_pred where
-"pickWP_pred A p1 p2 b1 b2 a \<equiv>
- a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
+"pickWP_pred A p1 p2 b1 b2 a \<equiv> a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
definition pickWP where
-"pickWP A p1 p2 b1 b2 \<equiv>
- SOME a. pickWP_pred A p1 p2 b1 b2 a"
+"pickWP A p1 p2 b1 b2 \<equiv> SOME a. pickWP_pred A p1 p2 b1 b2 a"
lemma pickWP_pred:
assumes "wpull A B1 B2 f1 f2 p1 p2" and
@@ -323,9 +321,6 @@
lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
by auto
-lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
-by simp
-
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
by simp
--- a/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 15:01:25 2012 +0200
@@ -61,7 +61,8 @@
then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
using bchoice[of B ?phi] by blast
hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
- have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f)
+ have gf: "inver g f A" unfolding inver_def
+ by (metis (no_types) gg imageI[of _ A f] the_inv_into_f_f[OF inj_f])
moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
moreover have "A \<le> g ` B"
proof safe
@@ -123,13 +124,16 @@
unfolding bij_betw_def inver_def by auto
lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
-by (metis bij_betw_iff_ex bij_betw_imageE)
+by (drule bij_betw_imageE, unfold bij_betw_iff_ex) blast
lemma bij_betwI':
"\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
\<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
\<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
-unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI)
+unfolding bij_betw_def inj_on_def
+apply (rule conjI)
+ apply blast
+by (erule thin_rl) blast
lemma surj_fun_eq:
assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
@@ -192,7 +196,15 @@
then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
- show ?case by (metis Card_order_trans insert(5) insertE y(2) z)
+ show ?case
+ apply (intro bexI ballI)
+ apply (erule insertE)
+ apply hypsubst
+ apply (rule z(2))
+ using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3)
+ apply blast
+ apply (rule z(1))
+ done
qed
lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Wed Sep 12 15:01:25 2012 +0200
@@ -482,7 +482,6 @@
val bd_CnotzeroN = "bd_Cnotzero";
val collect_set_naturalN = "collect_set_natural";
val in_bdN = "in_bd";
-val in_congN = "in_cong";
val in_monoN = "in_mono";
val in_relN = "in_rel";
val map_idN = "map_id";
@@ -490,9 +489,7 @@
val map_compN = "map_comp";
val map_comp'N = "map_comp'";
val map_congN = "map_cong";
-val map_wppullN = "map_wppull";
val map_wpullN = "map_wpull";
-val rel_congN = "rel_cong";
val rel_IdN = "rel_Id";
val rel_GrN = "rel_Gr";
val rel_converseN = "rel_converse";
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 15:01:25 2012 +0200
@@ -59,12 +59,8 @@
fun resort_tfree S (TFree (s, _)) = TFree (s, S);
-fun retype_free T (Free (s, _)) = Free (s, T);
-
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
-fun mk_predT T = T --> HOLogic.boolT;
-
fun mk_id T = Const (@{const_name id}, T --> T);
fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
@@ -704,10 +700,11 @@
val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
-val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
+val parse_binding_colon = Parse.binding --| @{keyword ":"};
+val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder;
val parse_ctr_arg =
- @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
+ @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
(Parse.typ >> pair no_binder);
val parse_defaults =
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 12 15:01:25 2012 +0200
@@ -78,9 +78,15 @@
val mk_set_minimalN: int -> string
val mk_set_inductN: int -> string
+ val mk_bundle_name: binding list -> string
+
val split_conj_thm: thm -> thm list
val split_conj_prems: int -> thm -> thm
+ val retype_free: typ -> term -> term
+
+ val mk_predT: typ -> typ;
+
val mk_sumTN: typ list -> typ
val mk_sumTN_balanced: typ list -> typ
@@ -207,6 +213,12 @@
val set_inclN = "set_incl"
val set_set_inclN = "set_set_incl"
+val mk_bundle_name = space_implode "_" o map Binding.name_of;
+
+fun mk_predT T = T --> HOLogic.boolT;
+
+fun retype_free T (Free (s, _)) = Free (s, T);
+
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
fun dest_sumTN 1 T = [T]
@@ -319,7 +331,7 @@
fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
let
- val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
+ val name = mk_bundle_name bs;
fun qualify i bind =
let val namei = if i > 0 then name ^ string_of_int i else name;
in
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 15:01:25 2012 +0200
@@ -64,7 +64,7 @@
val ks = 1 upto n;
val m = live - n (*passive, if 0 don't generate a new bnf*);
val ls = 1 upto m;
- val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
+ val b = Binding.name (mk_bundle_name bs);
(* TODO: check if m, n etc are sane *)
@@ -1675,7 +1675,7 @@
map (fn i => map (fn i' =>
split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
- (2, @{thm sum_case_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
+ (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
(mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks
end;
@@ -1873,7 +1873,7 @@
||>> mk_Frees "f" coiter_fTs
||>> mk_Frees "g" coiter_fTs
||>> mk_Frees "s" corec_sTs
- ||>> mk_Frees "phi" (map (fn T => T --> T --> HOLogic.boolT) Ts);
+ ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts);
fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
val unf_name = Binding.name_of o unf_bind;
@@ -2291,7 +2291,7 @@
val pTs = map2 (curry op -->) passiveXs passiveCs;
val uTs = map2 (curry op -->) Ts Ts';
val JRTs = map2 (curry mk_relT) passiveAs passiveBs;
- val JphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
+ val JphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts';
val B1Ts = map HOLogic.mk_setT passiveAs;
val B2Ts = map HOLogic.mk_setT passiveBs;
@@ -2309,7 +2309,7 @@
||>> mk_Frees "u" uTs
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
- ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> U --> HOLogic.boolT) Ts) passiveAs)
+ ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
||>> mk_Frees "R" JRTs
||>> mk_Frees "phi" JphiTs
||>> mk_Frees "B1" B1Ts
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Wed Sep 12 15:01:25 2012 +0200
@@ -143,6 +143,7 @@
val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
val subst_id = @{thm subst[of _ _ "%x. x"]};
+val sum_case_weak_cong = @{thm sum_case_weak_cong};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
fun mk_coalg_set_tac coalg_def =
@@ -701,7 +702,7 @@
CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
rtac (@{thm append_Cons} RS arg_cong RS trans),
- rtac (rv_Cons RS trans), etac (@{thm sum_case_cong} RS arg_cong RS trans),
+ rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
ks])
rv_Conss)
@@ -873,7 +874,7 @@
rtac exI, rtac conjI,
(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
- etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
+ etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
rtac trans_fun_cong_image_id_id_apply,
@@ -897,7 +898,7 @@
rtac exI, rtac conjI,
(if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
- etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
+ etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
rtac trans_fun_cong_image_id_id_apply,
@@ -946,13 +947,13 @@
((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
rtac (@{thm if_P} RS
- (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans),
+ (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
rtac Lev_0, rtac @{thm singletonI},
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
- else (rtac (@{thm sum_case_cong} RS trans) THEN'
+ else (rtac (sum_case_weak_cong RS trans) THEN'
rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
@@ -990,7 +991,7 @@
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
- else rtac @{thm sum_case_cong} THEN' rtac (mk_sum_casesN n i' RS trans),
+ else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl,
rtac refl])
ks to_sbd_injs from_to_sbds)];
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 14:46:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 15:01:25 2012 +0200
@@ -33,7 +33,7 @@
val n = length bnfs; (*active*)
val ks = 1 upto n;
val m = live - n; (*passive, if 0 don't generate a new bnf*)
- val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
+ val b = Binding.name (mk_bundle_name bs);
(* TODO: check if m, n etc are sane *)
@@ -792,7 +792,7 @@
||>> mk_Frees' "x" init_FTs
||>> mk_Frees "f" init_fTs
||>> mk_Frees "f" init_fTs
- ||>> mk_Frees "phi" (replicate n (initT --> HOLogic.boolT));
+ ||>> mk_Frees "phi" (replicate n (mk_predT initT));
val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
(HOLogic.mk_conj (HOLogic.mk_eq (iidx,
@@ -977,20 +977,21 @@
val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
- val (((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
- (iter_f, iter_f')), fs), phis), phi2s), rec_ss), names_lthy) = names_lthy
- |> mk_Frees "z" Ts
- ||>> mk_Frees' "z1" Ts
+ val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
+ (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
+ |> mk_Frees' "z1" Ts
||>> mk_Frees' "z2" Ts'
||>> mk_Frees' "x" FTs
||>> mk_Frees "y" FTs'
||>> mk_Freess' "z" setFTss
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
||>> mk_Frees "f" fTs
- ||>> mk_Frees "phi" (map (fn T => T --> HOLogic.boolT) Ts)
- ||>> mk_Frees "phi" (map2 (fn T => fn U => T --> U --> HOLogic.boolT) Ts Ts')
||>> mk_Frees "s" rec_sTs;
+ val Izs = map2 retype_free Ts zs;
+ val phis = map2 retype_free (map mk_predT Ts) init_phis;
+ val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis;
+
fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1));
val fld_name = Binding.name_of o fld_bind;
val fld_def_bind = rpair [] o Thm.def_binding o fld_bind;
@@ -1353,7 +1354,7 @@
val XTs = mk_Ts passiveXs;
val YTs = mk_Ts passiveYs;
val IRTs = map2 (curry mk_relT) passiveAs passiveBs;
- val IphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs;
+ val IphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
val (((((((((((((((fs, fs'), fs_copy), us),
B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),