--- a/src/HOL/Library/bnf_decl.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML Fri Jan 31 10:02:36 2014 +0100
@@ -72,7 +72,7 @@
user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
lthy;
- fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
+ fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
@@ -81,7 +81,8 @@
||> `Local_Theory.restore;
fun mk_wit_thms set_maps =
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
+ (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
--- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Fri Jan 31 10:02:36 2014 +0100
@@ -198,7 +198,7 @@
val single_set_bd_thmss =
map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
in
- map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} =>
+ map2 (fn set_alt => fn single_set_bds => fn ctxt =>
mk_comp_set_bd_tac ctxt set_alt single_set_bds)
set_alt_thms single_set_bd_thmss
end;
@@ -251,7 +251,7 @@
|> minimize_wits
|> map (fn (frees, t) => fold absfree frees t);
- fun wit_tac {context = ctxt, prems = _} =
+ fun wit_tac ctxt =
mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
(maps wit_thms_of_bnf inners);
@@ -301,10 +301,10 @@
(Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp0_tac {context = ctxt, prems = _} =
+ fun map_comp0_tac ctxt =
unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
@{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
- fun map_cong0_tac {context = ctxt, prems = _} =
+ fun map_cong0_tac ctxt =
mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
@@ -322,7 +322,7 @@
Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
end;
- fun le_rel_OO_tac {context = ctxt, prems = _} =
+ fun le_rel_OO_tac ctxt =
EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN
unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1;
@@ -393,10 +393,10 @@
val bd = mk_bd_of_bnf Ds As bnf;
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
- fun map_comp0_tac {context = ctxt, prems = _} =
+ fun map_comp0_tac ctxt =
unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
@{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
- fun map_cong0_tac {context = ctxt, prems = _} =
+ fun map_cong0_tac ctxt =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
val set_map0_tacs =
if Config.get lthy quick_and_dirty then
@@ -478,7 +478,7 @@
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1;
- fun map_cong0_tac {context = ctxt, prems = _} =
+ fun map_cong0_tac ctxt =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf));
fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
@@ -628,7 +628,7 @@
val set_bds =
map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
- fun mk_tac thm {context = ctxt, prems = _} =
+ fun mk_tac thm ctxt =
(rtac (unfold_all ctxt thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
@@ -640,7 +640,7 @@
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac {context = ctxt, prems = _} =
+ fun wit_tac ctxt =
mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
val (bnf', lthy') =
--- a/src/HOL/Tools/BNF/bnf_def.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jan 31 10:02:36 2014 +0100
@@ -106,7 +106,7 @@
binding -> binding -> binding list ->
(((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
string * term list *
- ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) *
+ ((Proof.context -> thm list -> tactic) option * term list list) *
((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
local_theory * thm list
@@ -123,8 +123,8 @@
(typ list -> typ list -> typ list -> term))) * local_theory
val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
- ({prems: thm list, context: Proof.context} -> tactic) list ->
- ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
+ (Proof.context -> tactic) list ->
+ (Proof.context -> tactic) -> typ list option -> binding ->
binding -> binding list ->
(((((binding * typ) * term) * term list) * term) * term list) * term option ->
local_theory -> bnf * local_theory
@@ -1021,7 +1021,7 @@
map wit_goal (0 upto live - 1)
end;
- val triv_wit_tac = mk_trivial_wit_tac bnf_wit_defs;
+ fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs;
val wit_goalss =
(if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
@@ -1132,7 +1132,7 @@
(HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
in
Goal.prove_sorry lthy [] [] in_bd_goal
- (mk_in_bd_tac live surj_imp_ordLeq_inst
+ (fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt live surj_imp_ordLeq_inst
(Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
(map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
bd_Card_order bd_Cinfinite bd_Cnotzero)
@@ -1151,8 +1151,9 @@
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id)
- (Lazy.force map_comp) (map Lazy.force set_map))
+ (fn {context = ctxt, prems = _} => mk_rel_Grp_tac ctxt rel_OO_Grps (#map_id0 axioms)
+ (#map_cong0 axioms) (Lazy.force map_id) (Lazy.force map_comp)
+ (map Lazy.force set_map))
|> Thm.close_derivation
end;
@@ -1203,8 +1204,9 @@
val rhs = mk_conversep (Term.list_comb (rel, Rs));
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
val le_thm = Goal.prove_sorry lthy [] [] le_goal
- (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
- (Lazy.force map_comp) (map Lazy.force set_map))
+ (fn {context = ctxt, prems = _} => mk_rel_conversep_le_tac ctxt rel_OO_Grps
+ (Lazy.force rel_eq) (#map_cong0 axioms) (Lazy.force map_comp)
+ (map Lazy.force set_map))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
@@ -1218,8 +1220,8 @@
fun mk_rel_OO () =
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
- (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
- (Lazy.force map_comp) (map Lazy.force set_map))
+ (fn {context = ctxt, prems = _} => mk_rel_OO_le_tac ctxt rel_OO_Grps (Lazy.force rel_eq)
+ (#map_cong0 axioms) (Lazy.force map_comp) (map Lazy.force set_map))
|> Thm.close_derivation
|> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
@@ -1254,7 +1256,8 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
- (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map))
+ (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
+ (map Lazy.force set_map))
|> Thm.close_derivation
end;
@@ -1271,8 +1274,9 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
- (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
- (map Lazy.force set_map) (#map_cong0 axioms) (Lazy.force map_comp))
+ (fn {context = ctxt, prems = _} => mk_map_transfer_tac ctxt (Lazy.force rel_mono)
+ (Lazy.force in_rel) (map Lazy.force set_map) (#map_cong0 axioms)
+ (Lazy.force map_comp))
|> Thm.close_derivation
end;
@@ -1308,22 +1312,22 @@
fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
(fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
let
- fun mk_wits_tac set_maps =
- K (TRYALL Goal.conjunction_tac) THEN'
+ fun mk_wits_tac ctxt set_maps =
+ TRYALL Goal.conjunction_tac THEN
(case triv_tac_opt of
- SOME tac => tac set_maps
- | NONE => fn {context = ctxt, prems} =>
- unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems});
+ SOME tac => tac ctxt set_maps
+ | NONE => unfold_thms_tac ctxt one_step_defs THEN wit_tac ctxt);
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
fun mk_wit_thms set_maps =
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
+ (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
in
map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
- goals (map (fn tac => fn {context = ctxt, prems} =>
- unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs)
+ goals (map (fn tac => fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
|> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
@@ -1332,7 +1336,7 @@
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
fun mk_triv_wit_thms tac set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
- (K (TRYALL Goal.conjunction_tac) THEN' tac set_maps)
+ (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Jan 31 10:02:36 2014 +0100
@@ -15,25 +15,20 @@
val mk_in_mono_tac: int -> tactic
val mk_set_map: thm -> thm
- val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
+ val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
- val mk_rel_OO_le_tac: thm list -> thm -> thm -> thm -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
+ val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_conversep_tac: thm -> thm -> tactic
- val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
+ val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_mono_tac: thm list -> thm -> tactic
- val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
- val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm ->
- {prems: thm list, context: Proof.context} -> tactic
+ val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
- val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm ->
- thm -> {prems: thm list, context: Proof.context} -> tactic
+ val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
+ thm -> thm -> thm -> thm -> tactic
- val mk_trivial_wit_tac: thm list -> thm list -> {prems: thm list, context: Proof.context} ->
- tactic
+ val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -67,8 +62,7 @@
rtac set_map0) set_map0s) THEN'
rtac @{thm image_empty}) 1;
-fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps
- {context = ctxt, prems = _} =
+fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
let
val n = length set_maps;
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
@@ -120,8 +114,7 @@
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
end;
-fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
- {context = ctxt, prems = _} =
+fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
let
val n = length set_maps;
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
@@ -146,8 +139,7 @@
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
-fun mk_rel_OO_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
- {context = ctxt, prems = _} =
+fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
let
val n = length set_maps;
fun in_tac nthO_in = rtac CollectI THEN'
@@ -183,7 +175,7 @@
in_tac @{thm sndOp_in}] 1
end;
-fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
+fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
if null set_maps then atac 1
else
unfold_tac ctxt [in_rel] THEN
@@ -194,8 +186,7 @@
(etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
set_maps] 1;
-fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp
- {context = ctxt, prems = _} =
+fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
let
val n = length set_maps;
val in_tac = if n = 0 then rtac UNIV_I else
@@ -216,8 +207,8 @@
REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
end;
-fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
- bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
+fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
+ bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero =
if live = 0 then
rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
@@ -278,7 +269,7 @@
map_comp RS sym, map_id])] 1
end;
-fun mk_trivial_wit_tac wit_defs set_maps {context = ctxt, prems = _} =
+fun mk_trivial_wit_tac ctxt wit_defs set_maps =
unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Jan 31 10:02:36 2014 +0100
@@ -696,7 +696,8 @@
map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
+ (fn {context = ctxt, prems = _} => mk_hset_rec_minimal_tac ctxt m cts hset_rec_0s
+ hset_rec_Sucs))
|> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss'
end;
@@ -711,7 +712,8 @@
in
map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
Goal.prove_sorry lthy [] [] goal
- (mk_hset_minimal_tac n hset_defs hset_rec_minimal)
+ (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n hset_defs
+ hset_rec_minimal)
|> Thm.close_derivation)
goals hset_defss' hset_rec_minimal_thms
end;
@@ -830,7 +832,8 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([coalg_prem, mor_prem], concl)))
- (mk_bis_Gr_tac bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms)
+ (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
+ morE_thms coalg_in_thms)
|> Thm.close_derivation
end;
@@ -852,7 +855,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
(Logic.mk_implies (prem, concl)))
- (mk_bis_Union_tac bis_def in_mono'_thms)
+ (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
|> Thm.close_derivation
end;
@@ -1193,7 +1196,8 @@
val coalgT_thm =
Goal.prove_sorry lthy [] []
(fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
- (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
+ (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
+ (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
|> Thm.close_derivation;
val timer = time (timer "Tree coalgebra");
@@ -1557,7 +1561,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
- (mk_mor_beh_tac m mor_def mor_cong_thm
+ (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
beh_defs carT_defs strT_defs isNode_defs
to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
@@ -1709,14 +1713,15 @@
val mor_Rep =
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
- (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
- map_comp_id_thms map_cong0L_thms)
+ (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m (mor_def :: dtor_defs) Reps
+ Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
|> Thm.close_derivation;
val mor_Abs =
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
- (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses)
+ (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
+ Abs_inverses)
|> Thm.close_derivation;
in
(mor_Rep, mor_Abs)
@@ -1863,7 +1868,8 @@
in
map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
Goal.prove_sorry lthy [] [] goal
- (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
+ (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
+ map_cong0L unfold_o_dtor_thms)
|> Thm.close_derivation)
goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
end;
@@ -1948,7 +1954,8 @@
in
map3 (fn goal => fn unfold => fn map_cong0 =>
Goal.prove_sorry lthy [] [] goal
- (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
+ (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
+ corec_Inl_sum_thms)
|> Thm.close_derivation)
goals dtor_unfold_thms map_cong0s
end;
@@ -1963,7 +1970,8 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
- (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm)
+ (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
+ corec_Inl_sum_thms unfold_unique_mor_thm)
|> Thm.close_derivation
end;
@@ -2278,7 +2286,8 @@
in
map2 (fn goal => fn induct =>
Goal.prove_sorry lthy [] [] goal
- (mk_coind_wit_tac induct dtor_unfold_thms (flat set_mapss) wit_thms)
+ (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
+ (flat set_mapss) wit_thms)
|> Thm.close_derivation)
goals dtor_hset_induct_thms
|> map split_conj_thm
@@ -2362,7 +2371,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
- mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt)
+ mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
|> Thm.close_derivation
end;
@@ -2444,7 +2453,8 @@
map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss))
+ (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
+ dtor_Jmap_thms set_mapss))
|> Thm.close_derivation)
goals ctss hset_rec_0ss' hset_rec_Sucss';
in
@@ -2586,7 +2596,7 @@
val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
val zip_setss = mk_Jsetss passiveABs |> transpose;
- val Jrel_coinduct_tac =
+ fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
let
fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
let
@@ -2611,13 +2621,13 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map6 (mk_helper_coind_concl false)
activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
- val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
- map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms;
fun mk_helper_coind_thms vars concl =
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
(Logic.list_implies (helper_prems, concl)))
- helper_coind_tac
+ (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m
+ dtor_map_coinduct_thm ks map_comps map_cong0s map_arg_cong_thms set_mapss
+ dtor_unfold_thms dtor_Jmap_thms)
|> Thm.close_derivation
|> split_conj_thm;
val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl;
@@ -2641,13 +2651,14 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips)
(Logic.list_implies (helper_prems, concl)))
- (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct)
+ (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
+ dtor_unfold_thms set_mapss j set_induct)
|> Thm.close_derivation
|> split_conj_thm)
mk_helper_ind_concls ls dtor_Jset_induct_thms
|> transpose;
in
- mk_rel_coinduct_tac in_rels in_Jrels
+ mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels
helper_ind_thmss helper_coind1_thms helper_coind2_thms
end;
@@ -2674,9 +2685,9 @@
val map_id0_tacs =
map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
- val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
- val set_nat_tacss =
- map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
+ val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) map_cong0_thms;
+ val set_map0_tacss =
+ map2 (map2 (fn def => fn col => fn ctxt =>
unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col))
hset_defss (transpose col_natural_thmss);
@@ -2687,7 +2698,7 @@
val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites;
val set_bd_tacss =
- map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
+ map3 (fn Cinf => map2 (fn def => fn col => fn ctxt =>
unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col))
Jbd_Cinfinites hset_defss (transpose col_bd_thmss);
@@ -2695,11 +2706,11 @@
val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
- val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
- fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN
- mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt;
+ fun wit_tac thms ctxt = unfold_thms_tac ctxt (flat Jwit_defss) THEN
+ mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
val (Jbnfs, lthy) =
fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts =>
@@ -2750,8 +2761,8 @@
(if m = 0 then map HOLogic.eq_const Ts
else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
(mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
- (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
- dtor_unfold_thms)
+ (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
+ (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
lthy;
val timer = time (timer "relator coinduction");
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Jan 31 10:02:36 2014 +0100
@@ -9,41 +9,35 @@
signature BNF_GFP_TACTICS =
sig
- val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
- thm list list -> tactic
- val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list list ->
+ tactic
+ val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
- val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
thm list list -> tactic
- val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
tactic
val mk_coalg_set_tac: thm -> tactic
- val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
thm list list -> tactic
- val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
+ thm list list -> tactic
val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
- val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
- val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
- tactic
+ val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
+ val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
- val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
- val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_hset_minimal_tac: Proof.context -> int -> thm list -> thm -> tactic
+ val mk_hset_rec_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
+ tactic
val mk_incl_lsbis_tac: int -> int -> thm -> tactic
val mk_length_Lev'_tac: thm -> tactic
val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
@@ -52,17 +46,17 @@
thm list list -> thm list list -> thm list list list -> tactic
val mk_map_id0_tac: thm list -> thm -> thm -> tactic
val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
- val mk_dtor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
- val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
- val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
- thm list -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
+ val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list list ->
+ thm list -> thm list -> tactic
val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
val mk_mor_UNIV_tac: thm list -> thm -> tactic
- val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
- thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
- thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
- thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
+ thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
+ thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
+ thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
+ thm list -> thm list -> tactic
val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
val mk_mor_elim_tac: thm -> tactic
val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
@@ -75,12 +69,12 @@
val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm list -> thm list -> thm -> thm list -> tactic
- val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
- thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
- val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
+ thm list -> thm list -> tactic
+ val mk_rel_coinduct_coind_tac: Proof.context -> int -> thm -> int list -> thm list -> thm list ->
+ thm list -> thm list list -> thm list -> thm list -> tactic
+ val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list ->
+ int -> thm -> tactic
val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
@@ -96,9 +90,8 @@
val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
thm list -> thm list -> thm list list -> thm list list -> tactic
val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
- val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
+ val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
val mk_le_rel_OO_tac: thm -> thm list -> thm list -> tactic
end;
@@ -191,7 +184,7 @@
mk_UnIN n i] @
[etac @{thm UN_I}, atac]) 1;
-fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
+fun mk_hset_rec_minimal_tac ctxt m cts rec_0s rec_Sucs =
EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn thm => EVERY'
@@ -206,7 +199,7 @@
rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
rec_Sucs] 1;
-fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
+fun mk_hset_minimal_tac ctxt n hset_defs hset_rec_minimal =
(CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
@@ -319,8 +312,7 @@
REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
-fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
- {context = ctxt, prems = _} =
+fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
@@ -329,7 +321,7 @@
etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
(coalg_ins ~~ morEs)] 1;
-fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
+fun mk_bis_Union_tac ctxt bis_def in_monos =
let
val n = length in_monos;
val ks = 1 upto n;
@@ -377,7 +369,7 @@
rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
etac @{thm relcompI}, atac] 1;
-fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} =
+fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
let
val n = length strT_defs;
val ks = 1 upto n;
@@ -661,10 +653,10 @@
((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
end;
-fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
+fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
- map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
+ map_comp_ids map_cong0s map_arg_congs =
let
val n = length beh_defs;
val ks = 1 upto n;
@@ -865,8 +857,7 @@
rtac congruent_str_final, atac, rtac o_apply])
(equiv_LSBISs ~~ congruent_str_finals)] 1;
-fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
- {context = ctxt, prems = _} =
+fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
unfold_thms_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
@@ -878,7 +869,7 @@
Abs_inverses (drop m coalg_final_sets))])
(Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
-fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
+fun mk_mor_Abs_tac ctxt defs Abs_inverses =
unfold_thms_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
@@ -926,21 +917,20 @@
rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
-fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
- {context = ctxt, prems = _} =
+fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
EVERY' (map (fn thm =>
rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
rtac sym, rtac id_apply] 1;
-fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
+fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
-fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
+fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
unfold_thms_tac ctxt
(corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
etac unfold_unique_mor 1;
@@ -1052,13 +1042,12 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt =
+fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps =
rtac unfold_unique 1 THEN
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
ALLGOALS (etac sym);
-fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
- {context = ctxt, prems = _} =
+fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss =
let
val n = length dtor_maps;
in
@@ -1114,7 +1103,7 @@
end)
rel_Jrels rel_OOs) 1;
-fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits ctxt =
+fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
REPEAT_DETERM (atac 1 ORELSE
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
@@ -1128,7 +1117,7 @@
EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
+fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
@@ -1200,8 +1189,8 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
- dtor_unfolds dtor_maps {context = ctxt, prems = _} =
+fun mk_rel_coinduct_coind_tac ctxt m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
+ dtor_unfolds dtor_maps =
let val n = length ks;
in
EVERY' [DETERM o rtac coinduct,
@@ -1234,7 +1223,7 @@
val split_id_unfolds = @{thms prod.cases image_id id_apply};
-fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} =
+fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
let val n = length ks;
in
rtac set_induct 1 THEN
@@ -1258,8 +1247,7 @@
unfolds set_map0ss ks) 1
end;
-fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
- {context = ctxt, prems = CIHs} =
+fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
let val n = length in_rels;
in
Method.insert_tac CIHs 1 THEN
@@ -1284,7 +1272,7 @@
(in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
end;
-fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
+fun mk_unfold_transfer_tac ctxt m rel_coinduct map_transfers unfolds =
let
val n = length map_transfers;
in
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Jan 31 10:02:36 2014 +0100
@@ -877,7 +877,7 @@
val alg_select_thm = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_Ball II
(Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
- (mk_alg_select_tac Abs_IIT_inverse_thm)
+ (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
|> Thm.close_derivation;
val mor_select_thm =
@@ -904,8 +904,9 @@
(list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
val ex_mor = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
- (mk_init_ex_mor_tac Abs_IIT_inverse_thm ex_copy_alg_thm alg_min_alg_thm
- card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm)
+ (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
+ ex_copy_alg_thm alg_min_alg_thm card_of_min_alg_thms mor_comp_thm mor_select_thm
+ mor_incl_min_alg_thm)
|> Thm.close_derivation;
val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
@@ -1062,7 +1063,8 @@
val mor_Rep =
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
- (mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps)
+ (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
+ inver_Reps)
|> Thm.close_derivation;
val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
@@ -1292,7 +1294,8 @@
val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
in
map2 (fn goal => fn foldx =>
- Goal.prove_sorry lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
|> Thm.close_derivation)
goals ctor_fold_thms
end;
@@ -1306,7 +1309,8 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique)))
- (mk_rec_unique_mor_tac rec_defs fst_rec_pair_thms fold_unique_mor_thm)
+ (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
+ fold_unique_mor_thm)
|> Thm.close_derivation
end;
@@ -1389,7 +1393,8 @@
in
(singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (mk_ctor_induct2_tac cTs cts ctor_induct_thm weak_ctor_induct_thms))
+ (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
+ weak_ctor_induct_thms))
|> Thm.close_derivation,
rev (Term.add_tfrees goal []))
end;
@@ -1551,7 +1556,7 @@
val unique = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
- mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps ctxt)
+ mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
|> Thm.close_derivation;
in
`split_conj_thm unique
@@ -1626,11 +1631,12 @@
(map4 (mk_set_map0 f) fs_Imaps Izs sets sets')))
fs Isetss_by_range Isetss_by_range';
- fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_Imap_thms;
+ fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
val thms =
map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i))
+ (Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
|> Thm.close_derivation)
goals csetss ctor_Iset_thmss inducts ls;
in
@@ -1653,13 +1659,13 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
- fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss;
+ fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sum_Cinfinite set_bd_sumss;
val thms =
map4 (fn goal => fn ctor_sets => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
- mk_tac induct ctor_sets i ctxt))
+ mk_tac ctxt induct ctor_sets i))
|> Thm.close_derivation)
goals ctor_Iset_thmss inducts ls;
in
@@ -1689,7 +1695,8 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (mk_mcong_tac (rtac induct) set_Iset_thmsss map_cong0s ctor_Imap_thms))
+ (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
+ map_cong0s ctor_Imap_thms))
|> Thm.close_derivation;
in
split_conj_thm thm
@@ -1746,8 +1753,8 @@
in
singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (mk_le_rel_OO_tac m induct ctor_nchotomy_thms ctor_Irel_thms rel_mono_strongs
- rel_OOs))
+ (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
+ ctor_Irel_thms rel_mono_strongs rel_OOs))
|> Thm.close_derivation
end;
@@ -1756,11 +1763,11 @@
val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_Imap_unique_thms;
val map_comp0_tacs =
map2 (K oo mk_map_comp0_tac map_comps ctor_Imap_thms) ctor_Imap_unique_thms ks;
- val map_cong0_tacs = map (mk_map_cong0_tac m) Imap_cong0_thms;
+ val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms;
val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss);
- val bd_co_tacs = replicate n (fn {context = ctxt, prems = _} =>
+ val bd_co_tacs = replicate n (fn ctxt =>
unfold_thms_tac ctxt Ibd_defs THEN mk_bd_card_order_tac bd_card_orders);
- val bd_cinf_tacs = replicate n (fn {context = ctxt, prems = _} =>
+ val bd_cinf_tacs = replicate n (fn ctxt =>
unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1);
val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss);
val le_rel_OO_tacs = map (fn i =>
@@ -1771,7 +1778,7 @@
val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
- fun wit_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Iwit_defss) THEN
+ fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
val (Ibnfs, lthy) =
@@ -1816,13 +1823,15 @@
else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
val Irel_induct_thm =
mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
- (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strongs) lthy;
+ (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
+ ctor_Irel_thms rel_mono_strongs) lthy;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
val ctor_fold_transfer_thms =
mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
(mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
- (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms)
+ (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
+ (map map_transfer_of_bnf bnfs) ctor_fold_thms)
lthy;
val timer = time (timer "relator induction");
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Jan 31 10:02:36 2014 +0100
@@ -11,7 +11,7 @@
val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
thm list -> tactic
val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
- val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_alg_select_tac: Proof.context -> thm -> tactic
val mk_alg_set_tac: thm -> tactic
val mk_bd_card_order_tac: thm list -> tactic
val mk_bd_limit_tac: int -> thm -> tactic
@@ -20,39 +20,37 @@
val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
thm list -> thm list -> thm list -> tactic
- val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
+ thm list -> tactic
val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
- val mk_init_ex_mor_tac: thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
+ tactic
val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
thm list -> tactic
val mk_iso_alt_tac: thm list -> thm -> tactic
val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
- val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
+ val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
val mk_least_min_alg_tac: thm -> thm -> tactic
- val mk_le_rel_OO_tac: int -> thm -> thm list -> thm list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
+ thm list -> tactic
val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id0_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
- val mk_ctor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
- val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list ->
+ thm list -> tactic
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
thm -> thm -> thm -> thm -> thm -> tactic
val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
val mk_min_algs_tac: thm -> thm list -> tactic
val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
- val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
+ val mk_mor_Rep_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> thm list -> tactic
val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
val mk_mor_convol_tac: 'a list -> thm -> tactic
@@ -63,15 +61,14 @@
val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
- val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
- val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
- tactic
- val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
- Proof.context -> tactic
- val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
- thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list ->
+ thm list -> tactic
+ val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic
+ val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
+ val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list ->
+ int -> tactic
+ val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list ->
+ cterm list -> thm list -> int -> tactic
val mk_set_map0_tac: thm -> tactic
val mk_set_tac: thm -> tactic
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
@@ -385,7 +382,7 @@
EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac,
REPEAT_DETERM o etac conjE, atac] 1;
-fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
+fun mk_alg_select_tac ctxt Abs_inverse =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
@@ -410,8 +407,8 @@
stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
end;
-fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
- mor_comp mor_select mor_incl_min_alg {context = ctxt, prems = _} =
+fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
+ mor_comp mor_select mor_incl_min_alg =
let
val n = length card_of_min_algs;
val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso},
@@ -486,7 +483,7 @@
CONJ_WRAP' mk_induct_tac least_min_algs 1
end;
-fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
+fun mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss inver_Reps =
(K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
EVERY' (map rtac inver_Abss) THEN'
@@ -522,13 +519,13 @@
ctor_o_folds),
rtac sym, rtac id_apply] 1;
-fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}=
+fun mk_rec_tac ctxt rec_defs foldx fst_recs =
unfold_thms_tac ctxt
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
rtac @{thm snd_convol'}] 1;
-fun mk_rec_unique_mor_tac rec_defs fst_recs fold_unique_mor {context = ctxt, prems = _} =
+fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor =
unfold_thms_tac ctxt
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
etac fold_unique_mor 1;
@@ -558,7 +555,7 @@
DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1
end;
-fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} =
+fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts =
let
val n = length weak_ctor_inducts;
val ks = 1 upto n;
@@ -583,7 +580,7 @@
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt =
+fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
rtac fold_unique 1 THEN
unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
ALLGOALS atac;
@@ -603,8 +600,7 @@
EVERY' (map mk_UN set_maps)] 1
end;
-fun mk_set_nat_tac m induct_tac set_mapss
- ctor_maps csets ctor_sets i {context = ctxt, prems = _} =
+fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i =
let
val n = length ctor_maps;
@@ -623,7 +619,7 @@
(induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
end;
-fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i ctxt =
+fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
let
val n = length ctor_sets;
@@ -639,7 +635,7 @@
(induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
end;
-fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} =
+fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
let
fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
@@ -657,8 +653,7 @@
(induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
end;
-fun mk_le_rel_OO_tac m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs
- {context = ctxt, prems = _} =
+fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs =
EVERY' (rtac induct ::
map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO =>
EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
@@ -779,7 +774,7 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
+fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
let val n = length ks;
in
unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
@@ -794,7 +789,7 @@
IHs ctor_rels rel_mono_strongs)] 1
end;
-fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} =
+fun mk_fold_transfer_tac ctxt m rel_induct map_transfers folds =
let
val n = length map_transfers;
in
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Fri Jan 31 10:02:36 2014 +0100
@@ -21,11 +21,10 @@
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
- val mk_ctor_or_dtor_rel_tac:
- thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_ctor_or_dtor_rel_tac: Proof.context -> thm -> thm list -> thm list -> thm -> tactic
val mk_map_comp_id_tac: thm -> tactic
- val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic
val mk_map_cong0L_tac: int -> thm -> thm -> tactic
end;
@@ -85,7 +84,7 @@
gen_tac
end;
-fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
+fun mk_ctor_or_dtor_rel_tac ctxt srel_def IJrel_defs IJsrel_defs dtor_srel =
unfold_thms_tac ctxt IJrel_defs THEN
rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
@{thms Collect_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
@@ -97,7 +96,7 @@
fun mk_map_comp_id_tac map_comp0 =
(rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;
-fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
+fun mk_map_cong0_tac ctxt m map_cong0 =
EVERY' [rtac mp, rtac map_cong0,
CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;