nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:d67a6a48f1c7
+:89158f401b07
 |> HOLogic.mk_Trueprop
 end
 fun supports_tac ctxt perm_simps =
 let
-val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
+val simpset1 =
-val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
+put_simpset HOL_basic_ss ctxt addsimps @{thms supports_def fresh_def[symmetric]}
-in
+val simpset2 =
-EVERY' [ simp_tac ss1,
+put_simpset HOL_ss ctxt addsimps @{thms swap_fresh_fresh fresh_Pair}
+in
+EVERY' [ simp_tac simpset1,
 eqvt_tac ctxt (eqvt_strict_config addpres perm_simps),
-simp_tac ss2 ]
+simp_tac simpset2 ]
 end
 fun prove_supports_single ctxt perm_simps qtrm =
 let
 val goal = mk_supports_goal ctxt qtrm
 |> HOLogic.mk_Trueprop
 val tac =
 EVERY' [ rtac @{thm supports_finite},
 resolve_tac qsupports_thms,
-asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
+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
 end
 fun mk_fvs_goals fv = gen_mk_goals fv mk_supp
 fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn)
-fun add_ss thms =
+fun add_simpset ctxt thms = put_simpset HOL_basic_ss ctxt addsimps thms
-HOL_basic_ss addsimps thms
 fun symmetric thms =
 map (fn thm => thm RS @{thm sym}) thms
 val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
 fun mk_supp_abs_tac ctxt [] = []
 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs
-fun mk_bn_supp_abs_tac trm =
+fun mk_bn_supp_abs_tac ctxt trm =
 trm
 |> fastype_of
 |> body_type
 |> (fn ty => case ty of
-@{typ "atom set"}  => simp_tac (add_ss supp_Abs_set)
+@{typ "atom set"}  => simp_tac (add_simpset ctxt supp_Abs_set)
-| @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
+| @{typ "atom list"} => simp_tac (add_simpset ctxt supp_Abs_lst)
 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
 |> fst o HOLogic.dest_eq
 |> dest_comb
 val supp_abs_tac =
 case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
 SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
-| NONE => mk_bn_supp_abs_tac fv_fun
+| NONE => mk_bn_supp_abs_tac ctxt fv_fun
 val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts)
 in
-EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
+EVERY' [ TRY o asm_full_simp_tac (add_simpset ctxt (@{thm supp_Pair[symmetric]}::fv_simps)),
 TRY o supp_abs_tac,
-TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
+TRY o simp_tac (add_simpset ctxt @{thms supp_def supp_rel_def}),
 TRY o eqvt_tac ctxt eqvt_rconfig,
-TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
+TRY o simp_tac (add_simpset ctxt (@{thms Abs_eq_iff} @ eq_iffs)),
-TRY o asm_full_simp_tac (add_ss thms3),
+TRY o asm_full_simp_tac (add_simpset ctxt thms3),
-TRY o simp_tac (add_ss thms2),
+TRY o simp_tac (add_simpset ctxt thms2),
-TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i
+TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i
 end)
 in
 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
 |> map atomize
-|> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
+|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]}))
 end
 fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
 let
 in
 (arg_ty, fn x => finite $ (to_set (qbn $ x)))
 end
 val props = map mk_goal qbns
-val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @
+val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @
 @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
 in
 induct_prove qtys props qinduct (K ss_tac) ctxt
 end
 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
 end
 val props = map2 mk_goal qperm_bns alpha_bns
 val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
-val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
+val ss_tac = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss)
 in
 induct_prove qtys props qinduct (K ss_tac) ctxt'
 |> Proof_Context.export ctxt' ctxt
-|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
+|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def}))
 end
 fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
 let
 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
 end
 val props = map2 mk_goal qbns qperm_bns
 val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
 val ss_tac =
-EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
+EVERY' [asm_full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
 TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts),
-TRY o asm_full_simp_tac HOL_basic_ss]
+TRY o asm_full_simp_tac (put_simpset HOL_basic_ss ctxt')]
 in
 induct_prove qtys props qinduct (K ss_tac) ctxt'
 |> Proof_Context.export ctxt' ctxt
-|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
+|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def}))
 end
 (*** proves strong exhauts theorems ***)
 val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}
 @ @{thms finite.intros finite_Un finite_set finite_fset}
 in
 Goal.prove ctxt [] [] goal
 (K (HEADGOAL (rtac @{thm at_set_avoiding1}
-THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
+THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss)))))
 end
 (* derives an abs_eq theorem of the form
 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}
-val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss]
+val tac2 =
+EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss),
+TRY o simp_tac (put_simpset HOL_ss ctxt)]
 in
 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
 |> (if rec_flag
 then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)
 else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ]
 val parms = map (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}
 val (([(_, fperm)], fprops), ctxt') = Obtain.result
-(K (EVERY1 [etac exE,
+(fn ctxt' => EVERY1 [etac exE,
-full_simp_tac (HOL_basic_ss addsimps ss),
+full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
-REPEAT o (etac @{thm conjE})])) [fthm] ctxt
+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)
 val ((_, eqs), ctxt'') = Obtain.result
-(K (EVERY1
+(fn ctxt'' => EVERY1
 [ REPEAT o (etac @{thm exE}),
 REPEAT o (etac @{thm conjE}),
 REPEAT o (dtac setify),
-full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt'
+full_simp_tac (put_simpset HOL_basic_ss ctxt''
+addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt'
 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
 (* for freshness conditions *)
 val tac1 = SOLVED' (EVERY'
-[ simp_tac (HOL_basic_ss addsimps peqs),
+[ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
 conj_tac (DETERM o resolve_tac fprops') ])
 (* for equalities between constructors *)
 val tac2 = SOLVED' (EVERY'
 val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
 in
 rtac thm' 1
 end) ctxt
-THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss
+THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)
+(* FIXME proper goal context *)
 val size_simp_tac =
-simp_tac (size_simpset addsimps (@{thms comp_def snd_conv} @ size_thms))
+simp_tac (put_simpset size_ss lthy'' 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

changeset 3218	89158f401b07
parent 3210	024d07886de8
child 3226	780b7a2c50b6