nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:4af8a92396ce
+:c4f31f1564b7
 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, NONE))) qtys_descr qty_args1
 val qty_args3 = qty_args2 ~~ alpha_equivp_thms
 in
-fold_map Quotient_Type.add_quotient_type qty_args3 lthy
+fold_map (Quotient_Type.add_quotient_type {overloaded = false}) qty_args3 lthy
 end
 (* a wrapper for lifting a raw constant *)
 fun lift_raw_const qtys (qconst_name, rconst, mx', rsp_thm) lthy =
 let
 val qty = Quotient_Term.derive_qtyp lthy qtys rty
 val lhs_raw = Free (qconst_name, qty)
 val rhs_raw = rconst
 val raw_var = (Binding.name qconst_name, NONE, mx')
-val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+val ((binding, _, mx), ctxt) = Proof_Context.cert_var raw_var lthy
 val lhs = Syntax.check_term ctxt lhs_raw
 val rhs = Syntax.check_term ctxt rhs_raw
 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
 (* defines quotient constants *)
 fun define_qconsts qtys consts_specs lthy =
 let
 val (qconst_infos, lthy') =
 fold_map (lift_raw_const qtys) consts_specs lthy
-val phi = Proof_Context.export_morphism lthy' lthy
+val phi =
+Proof_Context.export_morphism lthy'
+(Proof_Context.transfer (Proof_Context.theory_of lthy') lthy)
 in
 (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')
 end
 s |> raw_explode
 |> Scan.finite Symbol.stopper parser >> implode
 |> fst
 end
-fun unraw_vars_thm thm =
+fun unraw_vars_thm ctxt thm =
 let
 fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
 val vars = Term.add_vars (Thm.prop_of thm) []
-val vars' = map (Var o unraw_var_str) vars
+val vars' = map (Thm.cterm_of ctxt o Var o unraw_var_str) vars
 in
-Thm.certify_instantiate ([], (vars ~~ vars')) thm
+Thm.instantiate ([], (vars ~~ vars')) thm
 end
 fun unraw_bounds_thm th =
 let
 val trm = Thm.prop_of th
 end
 fun lift_thms qtys simps thms ctxt =
 (map (Quotient_Tacs.lifted ctxt qtys simps
 #> unraw_bounds_thm
-#> unraw_vars_thm
+#> unraw_vars_thm ctxt
 #> Drule.zero_var_indexes) thms, ctxt)
 fun mk_supports_goal ctxt qtrm =
 |> map (mk_finite o mk_supp)
 |> foldr1 (HOLogic.mk_conj)
 |> HOLogic.mk_Trueprop
 val tac =
-EVERY' [ rtac @{thm supports_finite},
+EVERY' [ resolve_tac ctxt' @{thms supports_finite},
 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)))
+(K (HEADGOAL (resolve_tac ctxt' [qinduct] THEN_ALL_NEW tac)))
 |> singleton (Proof_Context.export ctxt' ctxt)
 |> Old_Datatype_Aux.split_conj_thm
 |> map zero_var_indexes
 end
 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}
+(K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding1}
 THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss)))))
 end
 (* derives an abs_eq theorem of the form
 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas
 prems bclausess qexhaust_thm =
 let
 fun aux_tac prem bclauses =
 case (get_all_binders bclauses) of
-[] => EVERY' [rtac prem, assume_tac ctxt]
+[] => EVERY' [resolve_tac ctxt [prem], assume_tac ctxt]
 | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
 let
 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}
 val (([(_, fperm)], fprops), ctxt') = Obtain.result
-(fn ctxt' => EVERY1 [etac exE,
+(fn ctxt' => EVERY1 [eresolve_tac ctxt [exE],
 full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
-REPEAT o (etac @{thm conjE})]) [fthm] ctxt
+REPEAT o (eresolve_tac ctxt @{thms conjE})]) [fthm] ctxt
 val abs_eq_thms = flat
 (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses)
 val ((_, eqs), ctxt'') = Obtain.result
 (fn ctxt'' => EVERY1
-[ REPEAT o (etac @{thm exE}),
+[ REPEAT o (eresolve_tac ctxt @{thms exE}),
-REPEAT o (etac @{thm conjE}),
+REPEAT o (eresolve_tac ctxt @{thms conjE}),
-REPEAT o (dtac setify),
+REPEAT o (dresolve_tac ctxt [setify]),
 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
 (* for freshness conditions *)
 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 ctxt'' fprops') ])
+conj_tac ctxt'' (DETERM o resolve_tac ctxt'' fprops') ])
 (* for equalities between constructors *)
 val tac2 = SOLVED' (EVERY'
-[ rtac (@{thm ssubst} OF prems),
+[ resolve_tac ctxt [@{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 ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
+conj_tac ctxt'' (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
 (* proves goal "P" *)
 val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
-(K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
+(K (EVERY1 [ resolve_tac ctxt'' [prem], RANGE [tac1, tac2] ]))
 |> singleton (Proof_Context.export ctxt'' ctxt)
 in
-rtac side_thm 1
+resolve_tac ctxt [side_thm] 1
 end) ctxt
 in
-EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
+EVERY1 [resolve_tac ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)]
 end
 fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
 perm_bn_alphas =
 Subgoal.FOCUS (fn {params, context = ctxt', ...} =>
 let
 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 (Thm.cterm_of ctxt' o Var) vs
 val assigns = map (lookup ty_parms) vs_tys
+val thm' = infer_instantiate ctxt' (map #1 vs ~~ assigns) thm
-val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
 in
-rtac thm' 1
+resolve_tac ctxt' [thm'] 1
 end) ctxt
 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)
 fun size_simp_tac ctxt =
 simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms))

branch	Nominal2-Isabelle2016
changeset 3243	c4f31f1564b7
parent 3239	67370521c09c
child 3245	017e33849f4d