nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:b2e1a7b83e05
+:67370521c09c
 (* defines the quotient types *)
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
 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, false, NONE))) qtys_descr qty_args1
+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
 end
 val lifted_perm_laws =
 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
 |> Variable.exportT lthy3 lthy2
-fun tac _ =
+fun tac ctxt =
-Class.intro_classes_tac [] THEN
+Class.intro_classes_tac ctxt [] THEN
-(ALLGOALS (resolve_tac lifted_perm_laws))
+(ALLGOALS (resolve_tac ctxt lifted_perm_laws))
 in
 lthy2
 |> Class.prove_instantiation_exit tac
 |> Named_Target.theory_init
 end
 (* defines the size functions and proves size-class *)
 fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
 let
-val tac = K (Class.intro_classes_tac [])
+fun tac ctxt = Class.intro_classes_tac ctxt []
 in
 lthy
 |> Local_Theory.exit_global
 |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
 |> snd o (define_qconsts qtys size_specs)
 fun unraw_vars_thm thm =
 let
 fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
-val vars = Term.add_vars (prop_of thm) []
+val vars = Term.add_vars (Thm.prop_of thm) []
 val vars' = map (Var o unraw_var_str) vars
 in
 Thm.certify_instantiate ([], (vars ~~ vars')) thm
 end
 |> foldr1 (HOLogic.mk_conj)
 |> HOLogic.mk_Trueprop
 val tac =
 EVERY' [ rtac @{thm supports_finite},
-resolve_tac qsupports_thms,
+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)))
 |> singleton (Proof_Context.export ctxt' ctxt)
-|> Datatype_Aux.split_conj_thm
+|> Old_Datatype_Aux.split_conj_thm
 |> map zero_var_indexes
 end
 (* finite supp instances *)
 val lthy1 =
 lthy
 |> Local_Theory.exit_global
 |> Class.instantiation (qfull_ty_names, tvs, @{sort fs})
-fun tac _ =
+fun tac ctxt =
-Class.intro_classes_tac [] THEN
+Class.intro_classes_tac ctxt [] THEN
-(ALLGOALS (resolve_tac qfsupp_thms))
+(ALLGOALS (resolve_tac ctxt qfsupp_thms))
 in
 lthy1
 |> Class.prove_instantiation_exit tac
 |> Named_Target.theory_init
 end
 | _ => 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}
-val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_conv permute_prod_def
 prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps
 fv_bn_eqvts qinduct bclausess ctxt =
 let
 Const (@{const_name "Abs_set"}, _) => true
 | Const (@{const_name "Abs_lst"}, _) => true
 | Const (@{const_name "Abs_res"}, _) => true
 | _ => false
 in
-thm |> prop_of
+thm |> Thm.prop_of
 |> HOLogic.dest_Trueprop
 |> HOLogic.dest_eq
 |> fst
 |> is_abs
 end
 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
 fresh_star_set}
 val tac1 =
 if rec_flag
-then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+then resolve_tac ctxt @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
-else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
+else resolve_tac ctxt @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
 val tac2 =
 EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss),
 TRY o simp_tac (put_simpset HOL_ss ctxt)]
 in
 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, atac]
+[] => EVERY' [rtac prem, assume_tac ctxt]
 | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
 let
-val parms = map (term_of o snd) params
+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,
 full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
 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 (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 (etac @{thm conjE}),
 (* 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 fprops') ])
+conj_tac (DETERM o resolve_tac ctxt'' fprops') ])
 (* for equalities between constructors *)
 val tac2 = SOLVED' (EVERY'
 [ rtac (@{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 (@{thms refl} @ perm_bn_alphas)) ])
+conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
 (* proves goal "P" *)
-val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
+val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
 |> singleton (Proof_Context.export ctxt'' ctxt)
 in
 rtac side_thm 1
 end) ctxt
 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
 val c = Free (c, TFree (a, @{sort fs}))
 val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
-|> map prop_of
+|> map Thm.prop_of
 |> map Logic.strip_horn
 |> split_list
 val ecases' = (map o map) strip_full_horn ecases
 val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
 val c_ty = TFree (a, @{sort fs})
 val c = Free (c_name, c_ty)
 val (prems, concl) = induct'
-|> prop_of
+|> Thm.prop_of
 |> Logic.strip_horn
 val concls = concl
 |> HOLogic.dest_Trueprop
 |> HOLogic.dest_conj
 val prems' = prems
 |> map strip_full_horn
 |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
 fun pat_tac ctxt thm =
-Subgoal.FOCUS (fn {params, context, ...} =>
+Subgoal.FOCUS (fn {params, context = ctxt', ...} =>
 let
-val thy = Proof_Context.theory_of context
+val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params
-val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params
+val vs = Term.add_vars (Thm.prop_of thm) []
-val vs = Term.add_vars (prop_of thm) []
 val vs_tys = map (Type.legacy_freeze_type o snd) vs
-val vs_ctrms = map (cterm_of thy o Var) vs
+val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs
 val assigns = map (lookup ty_parms) vs_tys
 val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
 in
 rtac thm' 1
 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))
 in
-Goal.prove_multi lthy'' [] prems' concls
+Goal.prove_common lthy'' NONE [] prems' concls
 (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))

changeset 3239	67370521c09c
parent 3229	b52e8651591f
child 3243	c4f31f1564b7