nominal2: comparison Nominal/nominal

equal deleted inserted replaced

-:b2e1a7b83e05
+:67370521c09c
 (* fixme: move to nominal_library *)
 fun real_head_of (@{term Trueprop} $ t) = real_head_of t
 | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t
 | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t
 | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t
-| real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
+| real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t
 | real_head_of t = head_of t
 fun mk_vc_compat (avoid, avoid_trm) prems concl_args params =
 if null avoid then
 |> (fn t => HOLogic.all_const c_ty $ lambda c t )
 |> (fn t => HOLogic.all_const @{typ perm} $  lambda p t)
 end
 fun induct_forall_const T =
-Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool})
+Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool})
 fun mk_induct_forall (a, T) t =
 induct_forall_const T $ Abs (a, T, t)
 fun add_c_prop qnt Ps (c, c_name, c_ty) trm =
 end
 val all_elims =
 let
 fun spec' ct =
-Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}
+Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
 in
 fold (fn ct => fn th => th RS spec' ct)
 end
 fun helper_tac flag prm p ctxt =
 val prm' = (prems' MRS prm)
 |> flag ? (all_elims [p])
 |> flag ? (eqvt_srule context)
 in
-asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms induct_forall_def})) 1
+asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
 end) ctxt
 fun non_binder_tac prem intr_cvars Ps ctxt =
-Subgoal.SUBPROOF (fn {context, params, prems, ...} =>
+Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} =>
 let
-val thy = Proof_Context.theory_of context
 val (prms, p, _) = split_last2 (map snd params)
-val prm_tys = map (fastype_of o term_of) prms
+val prm_tys = map (fastype_of o Thm.term_of) prms
-val cperms = map (cterm_of thy o perm_const) prm_tys
+val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
 val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms
 val prem' = prem
 |> cterm_instantiate (intr_cvars ~~ p_prms)
 |> eqvt_srule ctxt
 (* for inductive-premises*)
-fun tac1 prm = helper_tac true prm p context
+fun tac1 prm = helper_tac true prm p ctxt'
 (* for non-inductive premises *)
 fun tac2 prm =
 EVERY' [ minus_permute_intro_tac p,
-eqvt_stac context,
+eqvt_stac ctxt',
-helper_tac false prm p context ]
+helper_tac false prm p ctxt' ]
 fun select prm (t, i) =
 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
 in
-EVERY1 [ eqvt_stac context,
+EVERY1 [ eqvt_stac ctxt',
 rtac prem',
 RANGE (map (SUBGOAL o select) prems) ]
 end) ctxt
 fun fresh_thm ctxt user_thm p c concl_args avoid_trm =
 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt =
 Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>
 let
-val thy = Proof_Context.theory_of ctxt
 val (prms, p, c) = split_last2 (map snd params)
-val prm_trms = map term_of prms
+val prm_trms = map Thm.term_of prms
 val prm_tys = map fastype_of prm_trms
 val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm
 val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args
 val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm
 |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems)))
-val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm'
+val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm'
 val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result
 (K (EVERY1 [etac @{thm exE},
 full_simp_tac (put_simpset HOL_basic_ss ctxt
 addsimps @{thms supp_Pair fresh_star_Un}),
 REPEAT o dtac supp_perm_eq'])) [fthm] ctxt
 val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs)
 fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt
-val cperms = map (cterm_of thy o perm_const) prm_tys
+val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys
 val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms
 val prem' = prem
 |> cterm_instantiate (intr_cvars ~~ qp_prms)
 |> eqvt_srule ctxt
 helper_tac false prm (mk_cplus q p) ctxt' ]
 fun select prm (t, i) =
 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
-val side_thm = Goal.prove ctxt' [] [] (term_of concl)
+val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl)
-(fn {context, ...} =>
+(fn {context = ctxt'', ...} =>
-EVERY1 [ CONVERSION (expand_conv_bot context),
+EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
-eqvt_stac context,
+eqvt_stac ctxt'',
 rtac prem',
 RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
 |> singleton (Proof_Context.export ctxt' ctxt)
 in
 rtac side_thm 1
 end) ctxt
 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}
 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =
 let
-val thy = Proof_Context.theory_of ctxt
 val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt
 val (ind_prems, ind_concl) = raw_induct'
-|> prop_of
+|> Thm.prop_of
 |> Logic.strip_horn
 |>> map strip_full_horn
 val params = map (fn (x, _, _) => x) ind_prems
 val param_trms = (map o map) Free params
-val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs
+val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs
 val intr_vars = (map o map) fst intr_vars_tys
 val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms
-val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys
+val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys
 val (intr_prems, intr_concls) = intrs
-|> map prop_of
+|> map Thm.prop_of
 |> map2 subst_Vars intr_vars_substs
 |> map Logic.strip_horn
 |> split_list
 val intr_concls_args =
 fun after_qed ctxt_outside user_thms ctxt =
 let
 val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl'
 (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args)
 |> singleton (Proof_Context.export ctxt ctxt_outside)
-|> Datatype_Aux.split_conj_thm
+|> Old_Datatype_Aux.split_conj_thm
 |> map (fn thm => thm RS normalise)
 |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt
 addsimps @{thms permute_zero induct_rulify}))
 |> map (Drule.rotate_prems (length ind_prems'))
 |> map zero_var_indexes
 fun read_avoids avoid_trms intr =
 let
 (* fixme hack *)
 val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt
-val trms = map (term_of o snd) ctrms
+val trms = map (Thm.term_of o snd) ctrms
 val ctxt'' = fold Variable.declare_term trms ctxt'
 in
 map (Syntax.read_term ctxt'') avoid_trms
 end
 Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) []
 val main_parser = Parse.xname -- avoids_parser
 in
 val _ =
-Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
+Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
 "prove strong induction theorem for inductive predicate involving nominal datatypes"
 (main_parser >> prove_strong_inductive_cmd)
 end
 end

changeset 3239	67370521c09c
parent 3231	188826f1ccdb
child 3243	c4f31f1564b7