--- a/src/HOL/BNF/BNF.thy Tue May 07 15:03:01 2013 +0200
+++ b/src/HOL/BNF/BNF.thy Tue May 07 15:03:15 2013 +0200
@@ -13,8 +13,8 @@
imports More_BNFs
begin
-hide_const (open) Gr collect fsts snds setl setr
- convol thePull pick_middle fstO sndO csquare inver
+hide_const (open) Gr Grp collect fsts snds setl setr
+ convol thePull pick_middle pick_middlep fstO sndO fstOp sndOp csquare inver
image2 relImage relInvImage prefCl PrefCl Succ Shift shift
end
--- a/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 15:03:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 15:03:15 2013 +0200
@@ -662,7 +662,6 @@
val CB' = mk_bnf_T Bs' CA;
val CC' = mk_bnf_T Cs CA;
val CRs' = mk_bnf_T RTs CA;
- val CA'CB' = HOLogic.mk_prodT (CA', CB');
val bnf_map_AsAs = mk_bnf_map As' As';
val bnf_map_AsBs = mk_bnf_map As' Bs';
@@ -674,15 +673,14 @@
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
val pre_names_lthy = lthy;
- val (((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
+ val ((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
- ||>> yield_singleton (mk_Frees "p") CA'CB'
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "x") CA'
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "y") CB'
+ ||>> yield_singleton (mk_Frees "x") CA'
+ ||>> yield_singleton (mk_Frees "y") CB'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
||>> mk_Frees "z" As'
||>> mk_Frees "A" (map HOLogic.mk_setT As')
@@ -1022,7 +1020,7 @@
Goal.prove_sorry lthy [] []
(mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
HOLogic.eq_const CA'))
- (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms))
+ (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
|> Thm.close_derivation
end;
@@ -1083,16 +1081,13 @@
val in_rel = Lazy.lazy mk_in_rel;
- val predicate2_cong = @{thm predicate2_cong};
- val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
-
fun mk_rel_flip () =
let
val rel_conversep_thm = Lazy.force rel_conversep;
val cts = map (SOME o certify lthy) Rs;
val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
in
- unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS predicate2_cong)
+ unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_cong})
|> singleton (Proof_Context.export names_lthy pre_names_lthy)
end;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue May 07 15:03:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue May 07 15:03:15 2013 +0200
@@ -18,7 +18,7 @@
val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_rel_eq_tac: int -> thm -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_in_rel_tac: thm list -> {prems: 'b, context: Proof.context} -> tactic
@@ -104,7 +104,7 @@
@{thms fst_convol snd_convol} [map_id', refl])] 1
end;
-fun mk_rel_eq_tac n rel_Grp rel_cong map_id {context = ctxt, prems = _} =
+fun mk_rel_eq_tac n rel_Grp rel_cong map_id =
(EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN'
rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
(if n = 0 then rtac refl
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 07 15:03:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 07 15:03:15 2013 +0200
@@ -59,8 +59,6 @@
let
val timer = time (Timer.startRealTimer ());
- val note_all = Config.get lthy bnf_note_all;
-
val live = live_of_bnf (hd bnfs);
val n = length bnfs; (*active*)
val ks = 1 upto n;
@@ -228,7 +226,6 @@
val set_map'ss = map set_map'_of_bnf bnfs;
val rel_congs = map rel_cong_of_bnf bnfs;
val rel_converseps = map rel_conversep_of_bnf bnfs;
- val rel_defs = map rel_def_of_bnf bnfs;
val rel_Grps = map rel_Grp_of_bnf bnfs;
val rel_eqs = map rel_eq_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;
@@ -2315,7 +2312,6 @@
val p2Ts = map2 (curry op -->) passiveXs passiveBs;
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 mk_pred2T passiveAs passiveBs;
val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts';
val B1Ts = map HOLogic.mk_setT passiveAs;
@@ -2324,8 +2320,8 @@
val XTs = mk_Ts passiveXs;
val YTs = mk_Ts passiveYs;
- val ((((((((((((((((((((fs, fs'), fs_copy), gs), us),
- (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), JRs), Jphis),
+ val (((((((((((((((((((fs, fs'), fs_copy), gs), us),
+ (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), Jphis),
B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)),
names_lthy) = names_lthy
|> mk_Frees' "f" fTs
@@ -2335,7 +2331,6 @@
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
- ||>> mk_Frees "r" JRTs
||>> mk_Frees "P" JphiTs
||>> mk_Frees "B1" B1Ts
||>> mk_Frees "B2" B2Ts
@@ -2912,7 +2907,6 @@
val in_rels = map in_rel_of_bnf bnfs;
val in_Jrels = map in_rel_of_bnf Jbnfs;
- val Jrel_defs = map rel_def_of_bnf Jbnfs;
val folded_dtor_map_thms = map fold_maps dtor_map_thms;
val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 07 15:03:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 07 15:03:15 2013 +0200
@@ -30,8 +30,6 @@
let
val timer = time (Timer.startRealTimer ());
- val note_all = Config.get lthy bnf_note_all;
-
val live = live_of_bnf (hd bnfs);
val n = length bnfs; (*active*)
val ks = 1 upto n;
@@ -1380,11 +1378,10 @@
val AXTs = map HOLogic.mk_setT passiveXs;
val XTs = mk_Ts passiveXs;
val YTs = mk_Ts passiveYs;
- val IRTs = map2 (curry mk_relT) passiveAs passiveBs;
val IphiTs = map2 mk_pred2T passiveAs passiveBs;
- val (((((((((((((((fs, fs'), fs_copy), us),
- B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),
+ val ((((((((((((((fs, fs'), fs_copy), us),
+ B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), Iphis),
names_lthy) = names_lthy
|> mk_Frees' "f" fTs
||>> mk_Frees "f" fTs
@@ -1398,7 +1395,6 @@
||>> mk_Frees "p1" p1Ts
||>> mk_Frees "p2" p2Ts
||>> mk_Frees' "y" passiveAs
- ||>> mk_Frees "S" IRTs
||>> mk_Frees "R" IphiTs;
val map_FTFT's = map2 (fn Ds =>
@@ -1753,8 +1749,6 @@
val in_rels = map in_rel_of_bnf bnfs;
val in_Irels = map in_rel_of_bnf Ibnfs;
- val rel_defs = map rel_def_of_bnf bnfs;
- val Irel_defs = map rel_def_of_bnf Ibnfs;
val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
--- a/src/HOL/BNF/Tools/bnf_util.ML Tue May 07 15:03:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Tue May 07 15:03:15 2013 +0200
@@ -375,7 +375,8 @@
fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
-fun retype_free T (Free (s, _)) = Free (s, T);
+fun retype_free T (Free (s, _)) = Free (s, T)
+ | retype_free _ t = raise TERM ("retype_free", [t]);
(** Types **)