nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:b2e1a7b83e05
+:67370521c09c
 end
 (* produces the introduction rule for an alpha rule *)
 fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
 let
-val arg_names = Datatype_Prop.make_tnames arg_tys
+val arg_names = Old_Datatype_Prop.make_tnames arg_tys
 val arg_names' = Name.variant_list arg_names arg_names
 val args = map Free (arg_names ~~ arg_tys)
 val args' = map Free (arg_names' ~~ arg_tys)
 val alpha = fst (lookup alpha_map ty)
 val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
 | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
 end
 fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
 let
-val arg_names = Datatype_Prop.make_tnames arg_tys
+val arg_names = Old_Datatype_Prop.make_tnames arg_tys
 val arg_names' = Name.variant_list arg_names arg_names
 val args = map Free (arg_names ~~ arg_tys)
 val args' = map Free (arg_names' ~~ arg_tys)
 val alpha_bn = lookup alpha_bn_map bn_trm
 val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
 fun tac ctxt =
 HEADGOAL
 (DETERM o (rtac induct_thm)
 THEN_ALL_NEW
-(REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
+(REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt])))
 in
 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
 |> singleton (Proof_Context.export ctxt' ctxt)
-|> Datatype_Aux.split_conj_thm
+|> Old_Datatype_Aux.split_conj_thm
-|> map Datatype_Aux.split_conj_thm
+|> map Old_Datatype_Aux.split_conj_thm
 |> flat
-|> filter_out (is_true o concl_of)
+|> filter_out (is_true o Thm.concl_of)
 |> map zero_var_indexes
 end
 (* proof by rule induction over the alpha-definitions *)
 (DETERM o (rtac alpha_induct_thm)
 THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
 in
 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
 |> singleton (Proof_Context.export ctxt' ctxt)
-|> Datatype_Aux.split_conj_thm
+|> Old_Datatype_Aux.split_conj_thm
 |> map (fn th => th RS mp)
-|> map Datatype_Aux.split_conj_thm
+|> map Old_Datatype_Aux.split_conj_thm
 |> flat
-|> filter_out (is_true o concl_of)
+|> filter_out (is_true o Thm.concl_of)
 |> map zero_var_indexes
 end
 |> HOLogic.mk_not
 |> HOLogic.mk_Trueprop
 end
 fun distinct_tac ctxt cases_thms distinct_thms =
-rtac notI THEN' eresolve_tac cases_thms
+rtac notI THEN' eresolve_tac ctxt cases_thms
 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms)
 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
 let
 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result
 in
 Goal.prove ctxt [] [] goal
 (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1))
 end
 in
-map (mk_alpha_distinct o prop_of) raw_distinct_thms
+map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms
 end
 (** produces the alpha_eq_iff simplification rules **)
 (* in case a theorem is of the form (Rel Const Const), it will be
 rewritten to ((Rel Const = Const) = True)
 *)
 fun mk_simp_rule thm =
-case (prop_of thm) of
+case Thm.prop_of thm of
 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}
 | _ => thm
 fun alpha_eq_iff_tac ctxt dist_inj intros elims =
 SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE'
 (rtac @{thm iffI} THEN'
-RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
+RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)])
 fun mk_alpha_eq_iff_goal thm =
 let
-val prop = prop_of thm;
+val prop = Thm.prop_of thm;
 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
 fun list_conj l = foldr1 HOLogic.mk_conj l;
 in
 if hyps = [] then HOLogic.mk_Trueprop concl
 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
 fun cases_tac intros ctxt =
 let
-val prod_simps = @{thms split_conv prod_alpha_def rel_prod_def}
+val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv}
-val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
+val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt
 val bound_tac =
 EVERY' [ rtac exi_zero,
-resolve_tac @{thms alpha_refl},
+resolve_tac ctxt @{thms alpha_refl},
 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]
 in
-resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
+resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
 end
 fun raw_prove_refl ctxt alpha_result raw_dt_induct =
 let
 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} =
 fun trans_prem_tac pred_names ctxt =
 SUBPROOF (fn {prems, context, ...} =>
 let
 val prems' = map (transform_prem1 context pred_names) prems
 in
-resolve_tac prems' 1
+resolve_tac ctxt prems' 1
 end) ctxt
-val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_def alphas}
+val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas}
 in
 EVERY'
 [ etac exi_neg,
-resolve_tac @{thms alpha_sym_eqvt},
+resolve_tac ctxt @{thms alpha_sym_eqvt},
 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps),
 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
 trans_prem_tac pred_names ctxt]
 end
 val alpha_names = alpha_names @ alpha_bn_names
 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
 fun tac ctxt =
-resolve_tac alpha_intros THEN_ALL_NEW
+resolve_tac ctxt alpha_intros THEN_ALL_NEW
-FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
+FIRST' [assume_tac ctxt,
+rtac @{thm sym} THEN' assume_tac ctxt,
+prem_bound_tac alpha_names alpha_eqvt ctxt]
 in
 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt
 end
 (** transitivity proof for alphas **)
 (* applies cases rules and resolves them with the last premise *)
 fun ecases_tac cases =
-Subgoal.FOCUS (fn {prems, ...} =>
+Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
-HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
+HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems)))
 fun aatac pred_names =
-SUBPROOF (fn {prems, context, ...} =>
+SUBPROOF (fn {context = ctxt, prems, ...} =>
-HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
+HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems)))
 (* instantiates exI with the permutation p + q *)
 val perm_inst_tac =
 Subgoal.FOCUS (fn {params, ...} =>
 let
-val (p, q) = pairself snd (last2 params)
+val (p, q) = apply2 snd (last2 params)
 val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q]
 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
 in
 HEADGOAL (rtac exi_inst)
 end)
 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
 let
-val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_def}
+val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv}
 in
-resolve_tac intros
+resolve_tac ctxt intros
 THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN'
 TRY o EVERY'   (* if binders are present *)
 [ etac @{thm exE},
 etac @{thm exE},
 perm_inst_tac ctxt,
-resolve_tac @{thms alpha_trans_eqvt},
+resolve_tac ctxt @{thms alpha_trans_eqvt},
-atac,
+assume_tac ctxt,
 aatac pred_names ctxt,
 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
 end
 val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans
 fun prep_goal t =
 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
 in
-Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
+Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN'
-RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
+RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans']))))
 |> chop (length alpha_trms)
 end
 (* proves that alpha_raw implies alpha_bn *)
 fun raw_prove_bn_imp_tac alpha_result ctxt =
 SUBPROOF (fn {prems, context, ...} =>
 let
 val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
-val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
 val prems'' = map (transform_prem1 context alpha_names) prems'
 in
 HEADGOAL
 (REPEAT_ALL_NEW
 (FIRST' [ rtac @{thm TrueI},
 rtac @{thm conjI},
-resolve_tac prems',
+resolve_tac ctxt prems',
-resolve_tac prems'',
+resolve_tac ctxt prems'',
-resolve_tac alpha_intros ]))
+resolve_tac ctxt alpha_intros ]))
 end) ctxt
 fun raw_prove_bn_imp ctxt alpha_result =
 let
 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
 val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
 val simpset =
-put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_def
+put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv
 permute_prod_def prod.case prod.rec})
 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset
 in
 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
 (* respectfulness for constructors *)
 fun raw_constr_rsp_tac ctxt alpha_intros simps =
 let
 val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def}
-val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_def
+val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv
 prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps
 in
 asm_full_simp_tac pre_simpset
-THEN' REPEAT o (resolve_tac @{thms allI impI})
+THEN' REPEAT o (resolve_tac ctxt @{thms allI impI})
-THEN' resolve_tac alpha_intros
+THEN' resolve_tac ctxt alpha_intros
 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset)
 end
 fun raw_constrs_rsp ctxt alpha_result constrs simps =
 let
 |> (fn t => t $ trm $ trm)
 |> Syntax.check_term ctxt
 |> HOLogic.mk_Trueprop
 in
 map (fn constrs =>
-Goal.prove_multi ctxt [] [] (map prep_goal constrs)
+Goal.prove_common ctxt NONE [] [] (map prep_goal constrs)
 (K (HEADGOAL
 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs
 end
 fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps =
 let
 val AlphaResult {alpha_bn_trms, ...} = alpha_result
 fun mk_map thm =
-thm |> `prop_of
+thm |> `Thm.prop_of
 |>> List.last  o snd o strip_comb
 |>> HOLogic.dest_Trueprop
 |>> head_of
 |>> fst o dest_Const
 fun raw_prove_perm_bn_tac alpha_result simps ctxt =
 SUBPROOF (fn {prems, context, ...} =>
 let
 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
-val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
 val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
 in
 HEADGOAL
 (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems'))
 THEN' TRY o REPEAT_ALL_NEW
 (FIRST' [ rtac @{thm TrueI},
 rtac @{thm conjI},
 rtac @{thm refl},
-resolve_tac prems',
+resolve_tac ctxt prems',
-resolve_tac prems'',
+resolve_tac ctxt prems'',
-resolve_tac alpha_intros ]))
+resolve_tac ctxt alpha_intros ]))
 end) ctxt
 fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
 let
 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =

changeset 3239	67370521c09c
parent 3229	b52e8651591f
child 3243	c4f31f1564b7