--- a/Nominal/Nominal2.thy Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/Nominal2.thy Sat Jan 11 23:17:23 2014 +0000
@@ -48,8 +48,6 @@
section{* Interface for nominal_datatype *}
-ML {* print_depth 50 *}
-
ML {*
fun get_cnstrs dts =
map snd dts
--- a/Nominal/nominal_dt_quot.ML Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_dt_quot.ML Sat Jan 11 23:17:23 2014 +0000
@@ -230,7 +230,7 @@
val tac =
EVERY' [ rtac @{thm supports_finite},
resolve_tac qsupports_thms,
- asm_simp_tac (put_simpset HOL_ss ctxt
+ asm_simp_tac (put_simpset HOL_ss ctxt'
addsimps @{thms finite_supp supp_Pair finite_Un}) ]
in
Goal.prove ctxt' [] [] goals
@@ -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 (term_of fperm) parms bn_eqvt permute_bns) bclauses)
val ((_, eqs), ctxt'') = Obtain.result
(fn ctxt'' => EVERY1
@@ -585,8 +585,8 @@
val (abs_eqs, peqs) = split_filter is_abs_eq eqs
val fprops' =
- map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops
- @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops
+ map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops
+ @ map (eqvt_rule ctxt'' (eqvt_strict_config addpres bn_eqvt)) fprops
(* for freshness conditions *)
val tac1 = SOLVED' (EVERY'
@@ -736,16 +736,15 @@
end) ctxt
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)
- (* FIXME proper goal context *)
- val size_simp_tac =
- simp_tac (put_simpset size_ss lthy'' addsimps (@{thms comp_def snd_conv} @ size_thms))
+ 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
- (fn {prems, context} =>
- Induction_Schema.induction_schema_tac context prems
- THEN RANGE (map (pat_tac context) exhausts) 1
- THEN prove_termination_ind context 1
- THEN ALLGOALS size_simp_tac)
+ (fn {prems, context = ctxt} =>
+ Induction_Schema.induction_schema_tac ctxt prems
+ THEN RANGE (map (pat_tac ctxt) exhausts) 1
+ THEN prove_termination_ind ctxt 1
+ THEN ALLGOALS (size_simp_tac ctxt))
|> Proof_Context.export lthy'' lthy
end
--- a/Nominal/nominal_function.ML Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_function.ML Sat Jan 11 23:17:23 2014 +0000
@@ -216,7 +216,7 @@
in
lthy'
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
- |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
+ |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
end
val nominal_function =
--- a/Nominal/nominal_function_core.ML Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_function_core.ML Sat Jan 11 23:17:23 2014 +0000
@@ -485,7 +485,8 @@
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
val ih_intro_case =
- full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ih_intro
+ full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+ ih_intro
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_intro_case)
@@ -519,7 +520,8 @@
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
- |> simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp RS sym])
+ |> simplify
+ (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym])
|> Thm.implies_intr (cprop_of case_hyp)
|> fold_rev (Thm.implies_intr o cprop_of) ags
|> fold_rev Thm.forall_intr cqs
@@ -734,7 +736,7 @@
|> Thm.forall_intr (cterm_of thy z)
|> (fn it => it COMP valthm)
|> Thm.implies_intr lhs_acc
- |> asm_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [f_iff])
+ |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff])
|> fold_rev (Thm.implies_intr o cprop_of) ags
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
@@ -889,7 +891,8 @@
qglr=(oqs, _, _, _), ...} = clause
val ih_case =
- full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ihyp
+ full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+ ihyp
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
@@ -979,7 +982,7 @@
|> Thm.forall_intr (cterm_of thy R')
|> Thm.forall_elim (cterm_of thy (inrel_R))
|> curry op RS wf_in_rel
- |> full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [in_rel_def])
+ |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def])
|> Thm.forall_intr (cterm_of thy Rrel)
end
--- a/Nominal/nominal_mutual.ML Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_mutual.ML Sat Jan 11 23:17:23 2014 +0000
@@ -171,7 +171,7 @@
val rhs = inst pre_rhs
val cqs = map (cterm_of thy) qs
- val ags = map (Thm.assume o cterm_of thy) gs
+ val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt
val import = fold Thm.forall_elim cqs
#> fold Thm.elim_implies ags
@@ -179,7 +179,7 @@
val export = fold_rev (Thm.implies_intr o cprop_of) ags
#> fold_rev forall_intr_rename (oqnames ~~ cqs)
in
- F ctxt (f, qs, gs, args, rhs) import export
+ F ctxt' (f, qs, gs, args, rhs) import export
end
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
@@ -188,17 +188,19 @@
val (MutualPart {f=SOME f, ...}) = get_part fname parts
val psimp = import sum_psimp_eq
- val (simp, restore_cond) =
+ val ((simp, restore_cond), ctxt') =
case cprems_of psimp of
- [] => (psimp, I)
- | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
+ [] => ((psimp, I), ctxt)
+ | [cond] =>
+ let val (asm, ctxt') = Thm.assume_hyps cond ctxt
+ in ((Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end
| _ => raise General.Fail "Too many conditions"
in
- Goal.prove ctxt [] []
+ Goal.prove ctxt' [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
- (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
- THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
- THEN (simp_tac ctxt) 1)
+ (fn _ => (Local_Defs.unfold_tac ctxt' all_orig_fdefs)
+ THEN EqSubst.eqsubst_tac ctxt' [0] [simp] 1
+ THEN (simp_tac ctxt') 1)
|> restore_cond
|> export
end
@@ -212,19 +214,21 @@
val (MutualPart {f=SOME f, ...}) = get_part fname parts
val psimp = import sum_psimp_eq
- val (cond, simp, restore_cond) =
+ val ((cond, simp, restore_cond), ctxt') =
case cprems_of psimp of
- [] => ([], psimp, I)
- | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
+ [] => (([], psimp, I), ctxt)
+ | [cond] =>
+ let val (asm, ctxt') = Thm.assume_hyps cond ctxt
+ in (([asm], Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end
| _ => raise General.Fail "Too many conditions"
- val ([p], ctxt') = ctxt
+ val ([p], ctxt'') = ctxt'
|> fold Variable.declare_term args
|> Variable.variant_fixes ["p"]
val p = Free (p, @{typ perm})
val simpset =
- put_simpset HOL_basic_ss ctxt' addsimps
+ put_simpset HOL_basic_ss ctxt'' addsimps
@{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @
@{thms Projr.simps Projl.simps} @
[(cond MRS eqvt_thm) RS @{thm sym}] @
@@ -232,10 +236,10 @@
val goal_lhs = mk_perm p (list_comb (f, args))
val goal_rhs = list_comb (f, map (mk_perm p) args)
in
- Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
- (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+ Goal.prove ctxt'' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
+ (fn _ => Local_Defs.unfold_tac ctxt'' all_orig_fdefs
THEN (asm_full_simp_tac simpset 1))
- |> singleton (Proof_Context.export ctxt' ctxt)
+ |> singleton (Proof_Context.export ctxt'' ctxt)
|> restore_cond
|> export
end
--- a/Nominal/nominal_termination.ML Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_termination.ML Sat Jan 11 23:17:23 2014 +0000
@@ -92,7 +92,7 @@
[((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
|> Proof_Context.note_thmss ""
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
- [([Goal.norm_result termination], [])])] |> snd
+ [([Goal.norm_result lthy termination], [])])] |> snd
|> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
end