--- a/NEWS Wed Jan 01 15:55:11 2014 +0100
+++ b/NEWS Wed Jan 01 21:23:32 2014 +0100
@@ -33,10 +33,10 @@
*** HOL ***
-* "declare [[code abort: …]]" replaces "code_abort …".
-INCOMPATIBILITY.
-
-* "declare [[code drop: …]]" drops all code equations associated
+* "declare [[code abort: ...]]" replaces "code_abort ...".
+INCOMPATIBILITY.
+
+* "declare [[code drop: ...]]" drops all code equations associated
with the given constants.
* Abolished slightly odd global lattice interpretation for min/max.
@@ -121,7 +121,7 @@
* When devising rule sets for number calculation, consider the
following canonical cases: 0, 1, numeral _, - 1, - numeral _.
* HOLogic.dest_number also recognizes numerals in non-canonical forms
- like "numeral One", "- numeral One", "- 0" and even "- … - _".
+ like "numeral One", "- numeral One", "- 0" and even "- ... - _".
* Syntax for negative numerals is mere input syntax.
INCOMPATBILITY.
@@ -155,7 +155,7 @@
Consider simplification with algebra_simps or field_simps.
b) Lifting rules from addition to subtraction:
-Try with "using <rule for addition> of [… "- _" …]" by simp".
+Try with "using <rule for addition> of [... "- _" ...]" by simp".
c) Simplification with "diff_def": just drop "diff_def".
Consider simplification with algebra_simps or field_simps;
--- a/etc/components Wed Jan 01 15:55:11 2014 +0100
+++ b/etc/components Wed Jan 01 21:23:32 2014 +0100
@@ -8,5 +8,4 @@
src/HOL/Tools
src/HOL/Tools/ATP
src/HOL/Tools/Sledgehammer/MaSh
-src/HOL/Tools/SMT
src/HOL/TPTP
--- a/etc/isar-keywords.el Wed Jan 01 15:55:11 2014 +0100
+++ b/etc/isar-keywords.el Wed Jan 01 21:23:32 2014 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-FP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -33,6 +33,7 @@
"axiomatization"
"back"
"bnf"
+ "bnf_decl"
"boogie_file"
"bundle"
"by"
@@ -46,7 +47,6 @@
"classes"
"classrel"
"codatatype"
- "code_abort"
"code_class"
"code_const"
"code_datatype"
@@ -486,6 +486,7 @@
"atom_decl"
"attribute_setup"
"axiomatization"
+ "bnf_decl"
"boogie_file"
"bundle"
"case_of_simps"
@@ -493,7 +494,6 @@
"classes"
"classrel"
"codatatype"
- "code_abort"
"code_class"
"code_const"
"code_datatype"
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Jan 01 21:23:32 2014 +0100
@@ -227,12 +227,12 @@
in Library.foldr mk_ex (vs, conj) end
val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
(* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
- fun tacs {context = ctxt, prems} = [
+ fun tacs ctxt = [
rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
rtac thm3 1]
in
- val nchotomy = prove thy con_betas goal tacs
+ val nchotomy = prove thy con_betas goal (tacs o #context)
val exhaust =
(nchotomy RS @{thm exh_casedist0})
|> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
@@ -272,8 +272,8 @@
val bottom = mk_bottom (fastype_of v')
val vs' = map (fn v => if v = v' then bottom else v) vs
val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
- val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
in map one_strict nonlazy end
fun con_defin (con, args) =
@@ -286,8 +286,8 @@
val goal = mk_trp (iff_disj (lhs, rhss))
val rule1 = iso_locale RS @{thm iso.abs_bottom_iff}
val rules = rule1 :: @{thms con_bottom_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
in
val con_stricts = maps con_strict spec'
val con_defins = map con_defin spec'
@@ -317,16 +317,16 @@
val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}
val rules2 = @{thms up_defined spair_defined ONE_defined}
val rules = rules1 @ rules2
- val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
- in map (fn c => pgterm mk_below c (K tacs)) cons' end
+ fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
+ in map (fn c => pgterm mk_below c (tacs o #context)) cons' end
val injects =
let
val abs_eq = iso_locale RS @{thm iso.abs_eq}
val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}
val rules2 = @{thms up_defined spair_defined ONE_defined}
val rules = rules1 @ rules2
- val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
- in map (fn c => pgterm mk_eq c (K tacs)) cons' end
+ fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
+ in map (fn c => pgterm mk_eq c (tacs o #context)) cons' end
end
(* prove distinctness of constructors *)
@@ -350,8 +350,8 @@
val goal = mk_trp (iff_disj (lhs, rhss))
val rule1 = iso_locale RS @{thm iso.abs_below}
val rules = rule1 :: @{thms con_below_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
fun dist_eq (con1, args1) (con2, args2) =
let
val (vs1, zs1) = get_vars args1
@@ -362,8 +362,8 @@
val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2))
val rule1 = iso_locale RS @{thm iso.abs_eq}
val rules = rule1 :: @{thms con_eq_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
in
val dist_les = map_dist dist_le spec'
val dist_eqs = map_dist dist_eq spec'
@@ -518,8 +518,8 @@
val rules2 = @{thms con_bottom_iff_rules}
val rules3 = @{thms cfcomp2 one_case2}
val rules = abs_inverse :: rules1 @ rules2 @ rules3
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1]
- in prove thy defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]
+ in prove thy defs goal (tacs o #context) end
in
val case_apps = map2 one_case spec fs
end
@@ -586,12 +586,12 @@
val sel_stricts : thm list =
let
val rules = rep_strict :: @{thms sel_strict_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
+ fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
fun sel_strict sel =
let
val goal = mk_trp (mk_strict sel)
in
- prove thy sel_defs goal (K tacs)
+ prove thy sel_defs goal (tacs o #context)
end
in
map sel_strict sel_consts
@@ -602,7 +602,7 @@
let
val defs = con_betas @ sel_defs
val rules = abs_inv :: @{thms sel_app_rules}
- val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
+ fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
let
val Ts : typ list = map #3 args
@@ -617,13 +617,13 @@
val concl = mk_trp (mk_eq (sel ` con_app, nth vs n))
val goal = Logic.list_implies (assms, concl)
in
- prove thy defs goal (K tacs)
+ prove thy defs goal (tacs o #context)
end
fun one_diff (_, sel, T) =
let
val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
in
- prove thy defs goal (K tacs)
+ prove thy defs goal (tacs o #context)
end
fun one_con (j, (_, args')) : thm list =
let
@@ -647,7 +647,7 @@
val sel_defins : thm list =
let
val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
+ fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
fun sel_defin sel =
let
val (T, U) = dest_cfunT (fastype_of sel)
@@ -656,7 +656,7 @@
val rhs = mk_eq (x, mk_bottom T)
val goal = mk_trp (mk_eq (lhs, rhs))
in
- prove thy sel_defs goal (K tacs)
+ prove thy sel_defs goal (tacs o #context)
end
fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
| one_arg _ = NONE
@@ -724,8 +724,8 @@
val assms = map (mk_trp o mk_defined) nonlazy
val concl = mk_trp (mk_eq (lhs, rhs))
val goal = Logic.list_implies (assms, concl)
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
- in prove thy dis_defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+ in prove thy dis_defs goal (tacs o #context) end
fun one_dis (i, dis) =
map_index (dis_app (i, dis)) spec
in
@@ -738,13 +738,13 @@
let
val x = Free ("x", lhsT)
val simps = dis_apps @ @{thms dist_eq_tr}
- val tacs =
+ fun tacs ctxt =
[rtac @{thm iffI} 1,
- asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps dis_stricts) 2,
+ asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps dis_stricts) 2,
rtac exhaust 1, atac 1,
- ALLGOALS (asm_full_simp_tac (Simplifier.global_context thy simple_ss addsimps simps))]
+ ALLGOALS (asm_full_simp_tac (put_simpset simple_ss ctxt addsimps simps))]
val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x))
- in prove thy [] goal (K tacs) end
+ in prove thy [] goal (tacs o #context) end
in
val dis_defins = map dis_defin dis_consts
end
@@ -813,8 +813,8 @@
val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat))
val k = Free ("k", U)
val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V))
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
- in prove thy match_defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+ in prove thy match_defs goal (tacs o #context) end
in
val match_stricts = map match_strict match_consts
end
@@ -832,8 +832,8 @@
val assms = map (mk_trp o mk_defined) nonlazy
val concl = mk_trp (mk_eq (lhs, rhs))
val goal = Logic.list_implies (assms, concl)
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
- in prove thy match_defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+ in prove thy match_defs goal (tacs o #context) end
fun one_match (i, mat) =
map_index (match_app (i, mat)) spec
in
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Jan 01 21:23:32 2014 +0100
@@ -71,9 +71,9 @@
val rules =
[abs_inverse] @ con_betas @ @{thms take_con_rules}
@ take_Suc_thms @ deflation_thms @ deflation_take_thms
- val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1
+ fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
in
- Goal.prove_global thy [] [] goal (K tac)
+ Goal.prove_global thy [] [] goal (tac o #context)
end
val take_apps = map prove_take_app con_specs
in
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Jan 01 21:23:32 2014 +0100
@@ -158,7 +158,7 @@
fun prove_proj (lhs, rhs) =
let
fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
- (simp_tac (Simplifier.global_context thy beta_ss)) 1
+ (simp_tac (put_simpset beta_ss ctxt)) 1
val goal = Logic.mk_equals (lhs, rhs)
in Goal.prove_global thy [] [] goal (tac o #context) end
val proj_thms = map prove_proj projs
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Jan 01 21:23:32 2014 +0100
@@ -273,8 +273,8 @@
let
val goal = mk_trp (mk_chain take_const)
val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}
- val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1
- val thm = Goal.prove_global thy [] [] goal (K tac)
+ fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
+ val thm = Goal.prove_global thy [] [] goal (tac o #context)
in
add_qualified_simp_thm "chain_take" (dbind, thm) thy
end
@@ -287,8 +287,8 @@
val lhs = take_const $ @{term "0::nat"}
val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}
- val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1
- val take_0_thm = Goal.prove_global thy [] [] goal (K tac)
+ fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
+ val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context)
in
add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
end
@@ -307,8 +307,8 @@
val goal = mk_eqs (lhs, rhs)
val simps = @{thms iterate_Suc fst_conv snd_conv}
val rules = take_defs @ simps
- val tac = simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1
- val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac)
+ fun tac ctxt = simp_tac (put_simpset beta_ss ctxt addsimps rules) 1
+ val take_Suc_thm = Goal.prove_global thy [] [] goal (tac o #context)
in
add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
end
@@ -330,11 +330,11 @@
@ deflation_abs_rep_thms
@ get_deflation_thms thy
in
- Goal.prove_global thy [] [] goal (fn _ =>
+ Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} =>
EVERY
[rtac @{thm nat.induct} 1,
- simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps bottom_rules) 1,
- asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps take_Suc_thms) 1,
+ simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
+ asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1,
REPEAT (etac @{thm conjE} 1
ORELSE resolve_tac deflation_rules 1
ORELSE atac 1)])
@@ -455,11 +455,11 @@
val rules1 =
take_Suc_thms @ decisive_abs_rep_thms
@ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}
- val tac = EVERY [
+ fun tac ctxt = EVERY [
rtac @{thm nat.induct} 1,
- simp_tac (Simplifier.global_context thy HOL_ss addsimps rules0) 1,
- asm_simp_tac (Simplifier.global_context thy HOL_ss addsimps rules1) 1]
- in Goal.prove_global thy [] [] goal (K tac) end
+ simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1,
+ asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1]
+ in Goal.prove_global thy [] [] goal (tac o #context) end
fun conjuncts 1 thm = [thm]
| conjuncts n thm = let
val thmL = thm RS @{thm conjunct1}
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Jan 01 21:23:32 2014 +0100
@@ -558,8 +558,8 @@
val defs = @{thm branch_def} :: pat_defs;
val goal = mk_trp (mk_strict fun1);
val rules = @{thms match_bind_simps} @ case_rews;
- val tacs = [simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1];
- in prove thy defs goal (K tacs) end;
+ fun tacs ctxt = [simp_tac (put_simpset beta_ss ctxt addsimps rules) 1];
+ in prove thy defs goal (tacs o #context) end;
fun pat_apps (i, (pat, (con, args))) =
let
val (fun1, fun2, taken) = pat_lhs (pat, args);
@@ -573,8 +573,8 @@
val goal = Logic.list_implies (assms, concl);
val defs = @{thm branch_def} :: pat_defs;
val rules = @{thms match_bind_simps} @ case_rews;
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1];
- in prove thy defs goal (K tacs) end;
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1];
+ in prove thy defs goal (tacs o #context) end;
in map_index pat_app spec end;
in
val pat_stricts = map pat_strict (pat_consts ~~ spec);
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Jan 01 21:23:32 2014 +0100
@@ -1523,7 +1523,7 @@
(augment_sort thy1 pt_cp_sort
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
(fn {context = ctxt, ...} => rtac rec_induct 1 THEN REPEAT
- (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
+ (simp_tac (put_simpset HOL_basic_ss ctxt
addsimps flat perm_simps'
addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
(resolve_tac rec_intrs THEN_ALL_NEW
@@ -1925,9 +1925,9 @@
in
Goal.prove context'' [] []
(HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
- (fn _ => EVERY
+ (fn {context = ctxt, ...} => EVERY
[cut_facts_tac [th'] 1,
- full_simp_tac (Simplifier.global_context thy11 HOL_ss (* FIXME context'' (!?) *)
+ full_simp_tac (put_simpset HOL_ss ctxt
addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
addsimprocs [NominalPermeq.perm_simproc_app]) 1,
full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jan 01 21:23:32 2014 +0100
@@ -271,7 +271,7 @@
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
- val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss
+ val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
@@ -452,13 +452,14 @@
concl))
in map mk_prem prems end) cases_prems;
- val cases_eqvt_simpset = Simplifier.global_context thy HOL_ss
+ val cases_eqvt_simpset = put_simpset HOL_ss (Proof_Context.init_global thy)
addsimps eqvt_thms @ swap_simps @ perm_pi_simp
addsimprocs [NominalPermeq.perm_simproc_app,
NominalPermeq.perm_simproc_fun];
val simp_fresh_atm = map
- (Simplifier.simplify (Simplifier.global_context thy HOL_basic_ss addsimps fresh_atm));
+ (Simplifier.simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
+ addsimps fresh_atm));
fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
prems') =
@@ -608,7 +609,7 @@
atoms)
end;
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
- val eqvt_simpset = Simplifier.global_context thy HOL_basic_ss addsimps
+ val eqvt_simpset = put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps
(NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
[mk_perm_bool_simproc names,
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 01 21:23:32 2014 +0100
@@ -290,7 +290,7 @@
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn a => Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
- val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss
+ val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Jan 01 21:23:32 2014 +0100
@@ -66,12 +66,11 @@
val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
- val simp_ctxt =
- Simplifier.global_context thy HOL_basic_ss
- addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
-
fun prove goal =
- Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
+ Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
+ ALLGOALS (simp_tac
+ (put_simpset HOL_basic_ss ctxt
+ addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))))
|> Simpdata.mk_eq;
in
(map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Jan 01 21:23:32 2014 +0100
@@ -195,8 +195,8 @@
EVERY [
rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
ALLGOALS (EVERY'
- [asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps case_rewrites),
- resolve_tac prems, asm_simp_tac (Simplifier.global_context thy HOL_basic_ss)])])
+ [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
+ resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
|> Drule.export_without_context;
val exh_name = Thm.derivation_name exhaust;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Jan 01 21:23:32 2014 +0100
@@ -185,12 +185,12 @@
#> Conv.fconv_rule (nnf_conv ctxt)
#> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}])
-fun rewrite_intros thy =
- Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [@{thm all_not_ex}])
+fun rewrite_intros ctxt =
+ Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}])
#> Simplifier.full_simplify
- (Simplifier.global_context thy HOL_basic_ss
+ (put_simpset HOL_basic_ss ctxt
addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
- #> split_conjuncts_in_assms (Proof_Context.init_global thy)
+ #> split_conjuncts_in_assms ctxt
fun print_specs options thy msg ths =
if show_intermediate_results options then
@@ -208,7 +208,7 @@
if forall is_pred_equation specs then
map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
else if forall (is_intro constname) specs then
- map (rewrite_intros thy) specs
+ map (rewrite_intros ctxt) specs
else
error ("unexpected specification for constant " ^ quote constname ^ ":\n"
^ commas (map (quote o Display.string_of_thm_global thy) specs))
--- a/src/HOL/Tools/SMT/etc/settings Wed Jan 01 15:55:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_SMT="$COMPONENT"
-
-ISABELLE_SMT_REMOTE="$ISABELLE_SMT/lib/scripts/remote_smt"
-ISABELLE_SMT_REMOTE_URL="http://smt.in.tum.de/smt"
-
--- a/src/HOL/Tools/TFL/rules.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Wed Jan 01 21:23:32 2014 +0100
@@ -648,7 +648,7 @@
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
let val globals = func::G
- val ctxt0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
+ val ctxt0 = empty_simpset (Proof_Context.init_global (Thm.theory_of_thm th))
val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val cut_lemma' = cut_lemma RS eq_reflection
--- a/src/HOL/Tools/TFL/tfl.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Jan 01 21:23:32 2014 +0100
@@ -432,7 +432,7 @@
not simplified. Otherwise large examples (Red-Black trees) are too
slow.*)
val case_simpset =
- Simplifier.global_context theory HOL_basic_ss
+ put_simpset HOL_basic_ss (Proof_Context.init_global theory)
addsimps case_rewrites
|> fold (Simplifier.add_cong o #weak_case_cong o snd)
(Symtab.dest (Datatype.get_all theory))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/etc/settings Wed Jan 01 21:23:32 2014 +0100
@@ -0,0 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_SMT_REMOTE="$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/remote_smt"
+ISABELLE_SMT_REMOTE_URL="http://smt.in.tum.de/smt"
+
--- a/src/HOL/Tools/inductive_set.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML Wed Jan 01 21:23:32 2014 +0100
@@ -406,8 +406,10 @@
(**** preprocessor for code generator ****)
-fun codegen_preproc thy =
+(* FIXME unused!? *)
+fun codegen_preproc thy = (* FIXME proper context!? *)
let
+ val ctxt = Proof_Context.init_global thy;
val {to_pred_simps, set_arities, pred_arities, ...} =
Data.get (Context.Theory thy);
fun preproc thm =
@@ -417,7 +419,7 @@
forall is_none xs) arities) (prop_of thm)
then
thm |>
- Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimprocs
+ Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
[to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
eta_contract_thm (is_pred pred_arities)
else thm
--- a/src/HOL/Tools/record.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/HOL/Tools/record.ML Wed Jan 01 21:23:32 2014 +0100
@@ -1556,6 +1556,7 @@
typ_thy
|> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
|> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]);
+ val defs_ctxt = Proof_Context.init_global defs_thy;
(* prepare propositions *)
@@ -1583,7 +1584,7 @@
in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
- simplify (Simplifier.global_context defs_thy HOL_ss)
+ simplify (put_simpset HOL_ss defs_ctxt)
(Goal.prove_sorry_global defs_thy [] [] inject_prop
(fn {context = ctxt, ...} =>
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
@@ -1605,7 +1606,7 @@
val cterm_ext = cterm_of defs_thy ext;
val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
val tactic1 =
- simp_tac (Simplifier.global_context defs_thy HOL_basic_ss addsimps [ext_def]) 1 THEN
+ simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
val [halfway] = Seq.list_of (tactic1 start);
@@ -1838,6 +1839,7 @@
thy
|> Sign.qualified_path false binding
|> extension_definition extension_name fields alphas_ext zeta moreT more vars;
+ val ext_ctxt = Proof_Context.init_global ext_thy;
val _ = timing_msg ctxt "record preparing definitions";
val Type extension_scheme = extT;
@@ -1935,7 +1937,7 @@
val init_thm = named_cterm_instantiate insts updacc_eq_triv;
val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
val tactic =
- simp_tac (Simplifier.global_context ext_thy HOL_basic_ss addsimps ext_defs) 1 THEN
+ simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
val updaccs = Seq.list_of (tactic init_thm);
in
@@ -2010,6 +2012,7 @@
map (rpair [Code.add_default_eqn_attribute]
o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
[make_spec, fields_spec, extend_spec, truncate_spec]);
+ val defs_ctxt = Proof_Context.init_global defs_thy;
(* prepare propositions *)
val _ = timing_msg ctxt "record preparing propositions";
@@ -2078,7 +2081,7 @@
val record_ss = get_simpset defs_thy;
val sel_upd_ctxt =
- Simplifier.global_context defs_thy record_ss
+ put_simpset record_ss defs_ctxt
addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
val (sel_convs, upd_convs) =
@@ -2092,7 +2095,7 @@
val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
let
val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
- val fold_ctxt = Simplifier.global_context defs_thy HOL_basic_ss addsimps symdefs;
+ val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt addsimps symdefs;
val ua_congs = map (Drule.export_without_context o simplify fold_ctxt) upd_acc_cong_assists;
in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end);
--- a/src/Provers/blast.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/Provers/blast.ML Wed Jan 01 21:23:32 2014 +0100
@@ -1258,7 +1258,6 @@
end
in
prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
- |> Seq.maps Thm.flexflex_rule
end
handle PROVE => Seq.empty
| TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
--- a/src/Pure/raw_simplifier.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Wed Jan 01 21:23:32 2014 +0100
@@ -40,7 +40,6 @@
val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc
val simpset_of: Proof.context -> simpset
val put_simpset: simpset -> Proof.context -> Proof.context
- val global_context: theory -> simpset -> Proof.context
val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory
val empty_simpset: Proof.context -> Proof.context
@@ -388,8 +387,6 @@
val Simpset ({bounds, depth, ...}, _) = context_ss;
in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end);
-fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss;
-
val empty_simpset = put_simpset empty_ss;
fun map_theory_simpset f thy =
--- a/src/Tools/Code/code_preproc.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML Wed Jan 01 21:23:32 2014 +0100
@@ -143,7 +143,8 @@
val resubst = curry (Term.betapplys o swap) all_vars;
in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
-fun lift_ss_conv f ss ct = f (Simplifier.global_context (theory_of_cterm ct) ss) ct;
+fun lift_ss_conv f ss ct = (* FIXME proper context!? *)
+ f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss) ct;
fun preprocess_conv thy =
let
--- a/src/Tools/Code/code_simp.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/Tools/Code/code_simp.ML Wed Jan 01 21:23:32 2014 +0100
@@ -62,8 +62,8 @@
fun simpset_program thy some_ss program =
simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss);
-fun lift_ss_conv f ss ct =
- f (Simplifier.global_context (theory_of_cterm ct) ss |> set_trace) ct;
+fun lift_ss_conv f ss ct = (* FIXME proper context!? *)
+ f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss |> set_trace) ct;
fun rewrite_modulo thy some_ss program =
lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);
--- a/src/ZF/Tools/inductive_package.ML Wed Jan 01 15:55:11 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML Wed Jan 01 21:23:32 2014 +0100
@@ -327,7 +327,7 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
val min_ss =
- (Simplifier.global_context thy empty_ss
+ (empty_simpset (Proof_Context.init_global thy)
|> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
setSolver (mk_solver "minimal"
(fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)