--- a/Nominal/nominal_dt_quot.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_quot.ML Thu Jul 09 02:32:46 2015 +0100
@@ -58,7 +58,7 @@
fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
let
val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
- val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, false, NONE))) qtys_descr qty_args1
+ val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1
val qty_args3 = qty_args2 ~~ alpha_equivp_thms
in
fold_map Quotient_Type.add_quotient_type qty_args3 lthy
@@ -113,9 +113,9 @@
map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
|> Variable.exportT lthy3 lthy2
- fun tac _ =
- Class.intro_classes_tac [] THEN
- (ALLGOALS (resolve_tac lifted_perm_laws))
+ fun tac ctxt =
+ Class.intro_classes_tac ctxt [] THEN
+ (ALLGOALS (resolve_tac ctxt lifted_perm_laws))
in
lthy2
|> Class.prove_instantiation_exit tac
@@ -126,7 +126,7 @@
(* defines the size functions and proves size-class *)
fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
let
- val tac = K (Class.intro_classes_tac [])
+ fun tac ctxt = Class.intro_classes_tac ctxt []
in
lthy
|> Local_Theory.exit_global
@@ -157,7 +157,7 @@
let
fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
- val vars = Term.add_vars (prop_of thm) []
+ val vars = Term.add_vars (Thm.prop_of thm) []
val vars' = map (Var o unraw_var_str) vars
in
Thm.certify_instantiate ([], (vars ~~ vars')) thm
@@ -229,14 +229,14 @@
val tac =
EVERY' [ rtac @{thm supports_finite},
- resolve_tac qsupports_thms,
+ resolve_tac ctxt' qsupports_thms,
asm_simp_tac (put_simpset HOL_ss ctxt'
addsimps @{thms finite_supp supp_Pair finite_Un}) ]
in
Goal.prove ctxt' [] [] goals
(K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
|> singleton (Proof_Context.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
|> map zero_var_indexes
end
@@ -250,9 +250,9 @@
|> Local_Theory.exit_global
|> Class.instantiation (qfull_ty_names, tvs, @{sort fs})
- fun tac _ =
- Class.intro_classes_tac [] THEN
- (ALLGOALS (resolve_tac qfsupp_thms))
+ fun tac ctxt =
+ Class.intro_classes_tac ctxt [] THEN
+ (ALLGOALS (resolve_tac ctxt qfsupp_thms))
in
lthy1
|> Class.prove_instantiation_exit tac
@@ -303,7 +303,7 @@
val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
-val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_conv permute_prod_def
prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps
@@ -436,7 +436,7 @@
| Const (@{const_name "Abs_res"}, _) => true
| _ => false
in
- thm |> prop_of
+ thm |> Thm.prop_of
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq
|> fst
@@ -538,8 +538,8 @@
val tac1 =
if rec_flag
- then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
- else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
+ then resolve_tac ctxt @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+ else resolve_tac ctxt @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
val tac2 =
EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss),
@@ -559,10 +559,10 @@
let
fun aux_tac prem bclauses =
case (get_all_binders bclauses) of
- [] => EVERY' [rtac prem, atac]
+ [] => EVERY' [rtac prem, assume_tac ctxt]
| binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
let
- val parms = map (term_of o snd) params
+ val parms = map (Thm.term_of o snd) params
val fthm = fresh_thm ctxt c parms binders bn_finite_thms
val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
@@ -572,7 +572,7 @@
REPEAT o (etac @{thm conjE})]) [fthm] ctxt
val abs_eq_thms = flat
- (map (abs_eq_thm ctxt' fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses)
+ (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses)
val ((_, eqs), ctxt'') = Obtain.result
(fn ctxt'' => EVERY1
@@ -592,17 +592,17 @@
val tac1 = SOLVED' (EVERY'
[ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
- conj_tac (DETERM o resolve_tac fprops') ])
+ conj_tac (DETERM o resolve_tac ctxt'' fprops') ])
(* for equalities between constructors *)
val tac2 = SOLVED' (EVERY'
[ rtac (@{thm ssubst} OF prems),
rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
- conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ])
+ conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
(* proves goal "P" *)
- val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
+ val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
(K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
|> singleton (Proof_Context.export ctxt'' ctxt)
in
@@ -622,7 +622,7 @@
val c = Free (c, TFree (a, @{sort fs}))
val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
- |> map prop_of
+ |> map Thm.prop_of
|> map Logic.strip_horn
|> split_list
@@ -707,7 +707,7 @@
val c = Free (c_name, c_ty)
val (prems, concl) = induct'
- |> prop_of
+ |> Thm.prop_of
|> Logic.strip_horn
val concls = concl
@@ -721,13 +721,12 @@
|> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
fun pat_tac ctxt thm =
- Subgoal.FOCUS (fn {params, context, ...} =>
+ Subgoal.FOCUS (fn {params, context = ctxt', ...} =>
let
- val thy = Proof_Context.theory_of context
- val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params
- val vs = Term.add_vars (prop_of thm) []
+ val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params
+ val vs = Term.add_vars (Thm.prop_of thm) []
val vs_tys = map (Type.legacy_freeze_type o snd) vs
- val vs_ctrms = map (cterm_of thy o Var) vs
+ val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs
val assigns = map (lookup ty_parms) vs_tys
val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
@@ -739,7 +738,7 @@
fun size_simp_tac ctxt =
simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms))
in
- Goal.prove_multi lthy'' [] prems' concls
+ Goal.prove_common lthy'' NONE [] prems' concls
(fn {prems, context = ctxt} =>
Induction_Schema.induction_schema_tac ctxt prems
THEN RANGE (map (pat_tac ctxt) exhausts) 1