# HG changeset patch # User Christian Urban # Date 1389482243 0 # Node ID 35bb5b013f0e8585cd1f231544c978755259fe67 # Parent 780b7a2c50b653ff6507cf9d208e8149be283976 updated with current AFP version diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/Nominal2.thy --- 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 diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_dt_quot.ML --- 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 diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_function.ML --- 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 = diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_function_core.ML --- 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 diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_mutual.ML --- 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 diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_termination.ML --- 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