--- a/Nominal/Ex/Lambda.thy Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Ex/Lambda.thy Thu Jul 09 02:32:46 2015 +0100
@@ -12,6 +12,16 @@
atom_decl name
+thm obtain_atom
+
+lemma
+ "(\<forall>thesis. (finite X \<longrightarrow> (\<forall>a. ((a \<notin> X \<and> sort_of a = s) \<longrightarrow> thesis)) \<longrightarrow> thesis)) \<longleftrightarrow>
+ (finite X \<longrightarrow> (\<exists> a. (a \<notin> X \<and> sort_of a = s)))"
+apply(auto)
+done
+
+
+
ML {* trace := true *}
nominal_datatype lam =
@@ -19,6 +29,24 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
+nominal_datatype environment =
+ Ni
+ | En name closure environment
+and closure =
+ Clos "lam" "environment"
+
+thm environment_closure.exhaust(1)
+
+nominal_function
+ env_lookup :: "environment => name => closure"
+where
+ "env_lookup Ni x = Clos (Var x) Ni"
+| "env_lookup (En v clos rest) x = (if (v = x) then clos else env_lookup rest x)"
+ apply (auto)
+ apply (simp add: env_lookup_graph_aux_def eqvt_def)
+ by (metis environment_closure.strong_exhaust(1))
+
+
lemma
"Lam [x]. Var x = Lam [y]. Var y"
proof -
@@ -232,6 +260,16 @@
section {* free name function *}
+
+lemma fresh_removeAll_name:
+ fixes x::"name"
+ and xs:: "name list"
+ shows "atom x \<sharp> (removeAll y xs) \<longleftrightarrow> (atom x \<sharp> xs \<or> x = y)"
+ apply (induct xs)
+ apply(auto simp add: fresh_def supp_Nil supp_Cons supp_at_base)
+ done
+
+
text {* first returns an atom list *}
nominal_function
--- a/Nominal/Ex/TypeVarsTest.thy Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Ex/TypeVarsTest.thy Thu Jul 09 02:32:46 2015 +0100
@@ -2,6 +2,37 @@
imports "../Nominal2"
begin
+atom_decl var
+
+ML {* trace := true *}
+declare [[ML_print_depth = 1000]]
+
+nominal_datatype exp =
+ Var var
+ | App exp var
+ | LetA as::assn body::exp binds "bn as" in "body" "as"
+ | Lam x::var body::exp binds x in body
+ and assn =
+ ANil | ACons var exp assn
+ binder
+ bn
+ where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"
+
+nominal_datatype ('ann::fs) exp2 =
+ Var var
+| App "'ann exp2" var
+| LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as
+| Lam x::var body::"'ann exp2" binds x in body
+and ('ann::fs) assn2 =
+ ANil
+| ACons var "'ann exp2" 'ann "'ann assn2"
+binder
+ bnn :: "('ann::fs) assn2 \<Rightarrow> atom list"
+where
+ "bnn ANil = []"
+| "bnn (ACons x a t as) = (atom x) # (bnn as)"
+
+
(* a nominal datatype with type variables and sorts *)
@@ -54,7 +85,6 @@
-
end
--- a/Nominal/Nominal2.thy Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Nominal2.thy Thu Jul 09 02:32:46 2015 +0100
@@ -149,7 +149,7 @@
val bn_fun_strs = get_bn_fun_strs bn_funs
val bn_fun_strs' = add_raws bn_fun_strs
val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
- val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
+ val bn_fun_full_env = map (apply2 (Long_Name.qualify thy_name))
(bn_fun_strs ~~ bn_fun_strs')
val raw_dts = rawify_dts dts dts_env
@@ -157,14 +157,14 @@
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses
val (raw_full_dt_names', thy1) =
- Datatype.add_datatype Datatype.default_config raw_dts thy
+ Old_Datatype.add_datatype Old_Datatype_Aux.default_config raw_dts thy
val lthy1 = Named_Target.theory_init thy1
- val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names'
+ val dtinfos = map (Old_Datatype_Data.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names'
val {descr, ...} = hd dtinfos
- val raw_tys = Datatype_Aux.get_rec_types descr
+ val raw_tys = Old_Datatype_Aux.get_rec_types descr
val raw_ty_args = hd raw_tys
|> snd o dest_Type
|> map dest_TFree
@@ -179,7 +179,7 @@
val raw_exhaust_thms = map #exhaust dtinfos
val raw_size_trms = map HOLogic.size_const raw_tys
val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
- (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names')))
+ (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names')))
val raw_result = RawDtInfo
{raw_dt_names = raw_full_dt_names',
@@ -303,7 +303,7 @@
val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux
fun match_const cnst th =
- (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th =
+ (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o Thm.prop_of) th =
fst (dest_Const cnst);
fun find_matching_rsp cnst =
hd (filter (fn th => match_const cnst th) raw_funs_rsp);
@@ -398,7 +398,7 @@
val qperm_bns = map #qconst qperm_bns_info
val _ = trace_msg (K "Lifting of theorems...")
- val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def
+ val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_sel
prod.case}
val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts,
@@ -452,7 +452,7 @@
val qsupp_constrs = qfv_defs
|> map (simplify (put_simpset HOL_basic_ss lthyC
- addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms)))
+ addsimps (filter (is_qfv_thm o Thm.prop_of) qfv_supp_thms)))
val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
val transform_thms =
@@ -548,7 +548,7 @@
((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx')))
val (dts, spec_ctxt) =
- Datatype.read_specs (map prep_spec dt_strs) thy
+ Old_Datatype.read_specs (map prep_spec dt_strs) thy
fun augment ((tname, tvs, mx), constrs) =
((tname, map (apsnd (augment_sort thy)) tvs, mx),
@@ -736,10 +736,9 @@
end
(* Command Keyword *)
-val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"}
+val _ = Outer_Syntax.local_theory @{command_keyword nominal_datatype}
"declaration of nominal datatypes"
(main_parser >> nominal_datatype2_cmd)
*}
-
end
--- a/Nominal/Nominal2_Abs.thy Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Nominal2_Abs.thy Thu Jul 09 02:32:46 2015 +0100
@@ -923,15 +923,15 @@
ML {*
fun alpha_single_simproc thm _ ctxt ctrm =
- let
+ let
val thy = Proof_Context.theory_of ctxt
- val _ $ (_ $ x) $ (_ $ y) = term_of ctrm
+ val _ $ (_ $ x) $ (_ $ y) = Thm.term_of ctrm
val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])
|> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs}))
|> map Free
|> HOLogic.mk_tuple
- |> Thm.cterm_of thy
- val cvrs_ty = ctyp_of_term cvrs
+ |> Thm.cterm_of ctxt
+ val cvrs_ty = Thm.ctyp_of_cterm cvrs
val thm' = thm
|> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs]
in
@@ -1050,7 +1050,6 @@
lemma [quot_respect]:
shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv"
unfolding rel_fun_def
- unfolding rel_prod_def
by auto
lemma [quot_preserve]:
@@ -1067,7 +1066,7 @@
lemma [eqvt]:
shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
unfolding prod_alpha_def
- unfolding rel_prod_def
+ unfolding rel_prod_conv
by (perm_simp) (rule refl)
lemma [eqvt]:
--- a/Nominal/Nominal2_Base.thy Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Nominal2_Base.thy Thu Jul 09 02:32:46 2015 +0100
@@ -5,7 +5,7 @@
Nominal Isabelle.
*)
theory Nominal2_Base
-imports Main
+imports "~~/src/HOL/Library/Old_Datatype"
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Quotient_Examples/FSet"
"~~/src/HOL/Library/FinFun"
@@ -769,9 +769,8 @@
subsection {* Eqvt infrastructure *}
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw}. *}
-
+
ML_file "nominal_thmdecls.ML"
-setup "Nominal_ThmDecls.setup"
lemmas [eqvt] =
@@ -823,7 +822,7 @@
{* pushes permutations inside, raises an error if it cannot solve all permutations. *}
simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ctxt => fn ctrm =>
- case term_of (Thm.dest_arg ctrm) of
+ case Thm.term_of (Thm.dest_arg ctrm) of
Free _ => NONE
| Var _ => NONE
| Const (@{const_name permute}, _) $ _ $ _ => NONE
@@ -891,14 +890,14 @@
shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)"
by (simp add: permute_bool_def)
-declare imp_eqvt[folded induct_implies_def, eqvt]
+declare imp_eqvt[folded HOL.induct_implies_def, eqvt]
lemma all_eqvt [eqvt]:
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
unfolding All_def
by (perm_simp) (rule refl)
-declare all_eqvt[folded induct_forall_def, eqvt]
+declare all_eqvt[folded HOL.induct_forall_def, eqvt]
lemma ex_eqvt [eqvt]:
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
@@ -1885,17 +1884,18 @@
simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ctxt => fn ctrm =>
let
- val _ $ _ $ f = term_of ctrm
+ val _ $ _ $ f = Thm.term_of ctrm
in
case (Term.add_frees f [], Term.add_vars f []) of
([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]})
- | (x::_, []) => let
- val thy = Proof_Context.theory_of ctxt
- val argx = Free x
- val absf = absfree x f
- val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))]
- val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)]
- val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+ | (x::_, []) =>
+ let
+ val argx = Free x
+ val absf = absfree x f
+ val cty_inst =
+ [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
+ val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)]
+ val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
in
SOME(thm RS @{thm Eq_TrueI})
end
@@ -2952,7 +2952,7 @@
simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm =>
- case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
+ case Thm.term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
let
fun first_is_neg lhs rhs [] = NONE
| first_is_neg lhs rhs (thm::thms) =
@@ -2973,8 +2973,8 @@
member (op=) atms lhs andalso member (op=) atms rhs
end)
| _ => false)
- |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms))
- |> map HOLogic.conj_elims
+ |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms))
+ |> map (HOLogic.conj_elims ctxt)
|> flat
in
case first_is_neg lhs rhs prems of
@@ -3353,7 +3353,7 @@
simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm =>
let
- val _ $ h = term_of ctrm
+ val _ $ h = Thm.term_of ctrm
val cfresh = @{const_name fresh}
val catom = @{const_name atom}
--- a/Nominal/nominal_atoms.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_atoms.ML Thu Jul 09 02:32:46 2015 +0100
@@ -28,14 +28,13 @@
fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
let
- val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic";
val str = Sign.full_name thy name;
(* typedef *)
val set = atom_decl_set str;
- val tac = rtac @{thm exists_eq_simple_sort} 1;
- val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
- Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy;
+ fun tac _ = rtac @{thm exists_eq_simple_sort} 1;
+ val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
+ Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy;
(* definition of atom and permute *)
val newT = #abs_type (fst info);
@@ -77,7 +76,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.command @{command_spec "atom_decl"}
+ Outer_Syntax.command @{command_keyword atom_decl}
"declaration of a concrete atom type"
((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
(Toplevel.theory o add_atom_decl))
--- a/Nominal/nominal_dt_alpha.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_alpha.ML Thu Jul 09 02:32:46 2015 +0100
@@ -162,7 +162,7 @@
(* 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)
@@ -205,7 +205,7 @@
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)
@@ -315,14 +315,14 @@
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
- |> map Datatype_Aux.split_conj_thm
+ |> Old_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
@@ -365,11 +365,11 @@
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
@@ -392,7 +392,7 @@
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 =
@@ -410,7 +410,7 @@
(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
@@ -421,19 +421,19 @@
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;
@@ -463,16 +463,16 @@
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 =
@@ -502,13 +502,13 @@
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]
@@ -525,8 +525,10 @@
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
fun tac ctxt =
- resolve_tac alpha_intros THEN_ALL_NEW
- FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
+ resolve_tac ctxt alpha_intros THEN_ALL_NEW
+ 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
@@ -536,18 +538,18 @@
(* applies cases rules and resolves them with the last premise *)
fun ecases_tac cases =
- Subgoal.FOCUS (fn {prems, ...} =>
- HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
+ Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
+ HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems)))
fun aatac pred_names =
- SUBPROOF (fn {prems, context, ...} =>
- HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
+ SUBPROOF (fn {context = ctxt, 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
@@ -556,16 +558,16 @@
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},
- atac,
+ resolve_tac ctxt @{thms alpha_trans_eqvt},
+ 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) ])
@@ -630,9 +632,9 @@
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
@@ -644,16 +646,16 @@
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 prems'',
- resolve_tac alpha_intros ]))
+ resolve_tac ctxt prems',
+ resolve_tac ctxt prems'',
+ resolve_tac ctxt alpha_intros ]))
end) ctxt
@@ -706,7 +708,7 @@
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
@@ -720,12 +722,12 @@
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' resolve_tac alpha_intros
+ THEN' REPEAT o (resolve_tac ctxt @{thms allI impI})
+ THEN' resolve_tac ctxt alpha_intros
THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset)
end
@@ -752,7 +754,7 @@
|> 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
@@ -772,7 +774,7 @@
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
@@ -797,7 +799,7 @@
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
@@ -806,9 +808,9 @@
(FIRST' [ rtac @{thm TrueI},
rtac @{thm conjI},
rtac @{thm refl},
- resolve_tac prems',
- resolve_tac prems'',
- resolve_tac alpha_intros ]))
+ resolve_tac ctxt prems',
+ resolve_tac ctxt prems'',
+ resolve_tac ctxt alpha_intros ]))
end) ctxt
fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
--- a/Nominal/nominal_dt_data.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_data.ML Thu Jul 09 02:32:46 2015 +0100
@@ -25,7 +25,7 @@
val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
datatype user_data = UserData of
- {dts : Datatype.spec list,
+ {dts : Old_Datatype.spec list,
cn_names : string list,
cn_tys : (string * string) list,
bn_funs : (binding * typ * mixfix) list,
@@ -34,7 +34,7 @@
datatype raw_dt_info = RawDtInfo of
{raw_dt_names : string list,
- raw_dts : Datatype.spec list,
+ raw_dts : Old_Datatype.spec list,
raw_tys : typ list,
raw_ty_args : (string * sort) list,
raw_cns_info : cns_info list,
@@ -111,7 +111,7 @@
datatype user_data = UserData of
- {dts : Datatype.spec list,
+ {dts : Old_Datatype.spec list,
cn_names : string list,
cn_tys : (string * string) list,
bn_funs : (binding * typ * mixfix) list,
@@ -120,7 +120,7 @@
datatype raw_dt_info = RawDtInfo of
{raw_dt_names : string list,
- raw_dts : Datatype.spec list,
+ raw_dts : Old_Datatype.spec list,
raw_tys : typ list,
raw_ty_args : (string * sort) list,
raw_cns_info : cns_info list,
--- a/Nominal/nominal_dt_quot.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_quot.ML Thu Jul 09 02:32:46 2015 +0100
@@ -58,7 +58,7 @@
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
@@ -113,9 +113,9 @@
map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
|> Variable.exportT lthy3 lthy2
- fun tac _ =
- Class.intro_classes_tac [] THEN
- (ALLGOALS (resolve_tac lifted_perm_laws))
+ fun tac ctxt =
+ Class.intro_classes_tac ctxt [] THEN
+ (ALLGOALS (resolve_tac ctxt lifted_perm_laws))
in
lthy2
|> Class.prove_instantiation_exit tac
@@ -126,7 +126,7 @@
(* 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
@@ -157,7 +157,7 @@
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
@@ -229,14 +229,14 @@
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
@@ -250,9 +250,9 @@
|> Local_Theory.exit_global
|> Class.instantiation (qfull_ty_names, tvs, @{sort fs})
- fun tac _ =
- Class.intro_classes_tac [] THEN
- (ALLGOALS (resolve_tac qfsupp_thms))
+ fun tac ctxt =
+ Class.intro_classes_tac ctxt [] THEN
+ (ALLGOALS (resolve_tac ctxt qfsupp_thms))
in
lthy1
|> Class.prove_instantiation_exit tac
@@ -303,7 +303,7 @@
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
@@ -436,7 +436,7 @@
| Const (@{const_name "Abs_res"}, _) => true
| _ => false
in
- thm |> prop_of
+ thm |> Thm.prop_of
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq
|> fst
@@ -538,8 +538,8 @@
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}
+ then resolve_tac ctxt @{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),
@@ -559,10 +559,10 @@
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}
@@ -572,7 +572,7 @@
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
@@ -592,17 +592,17 @@
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
@@ -622,7 +622,7 @@
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
@@ -707,7 +707,7 @@
val c = Free (c_name, c_ty)
val (prems, concl) = induct'
- |> prop_of
+ |> Thm.prop_of
|> Logic.strip_horn
val concls = concl
@@ -721,13 +721,12 @@
|> 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 (term_of ct), ct)) params
- val vs = Term.add_vars (prop_of thm) []
+ 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 (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
@@ -739,7 +738,7 @@
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
--- a/Nominal/nominal_dt_rawfuns.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML Thu Jul 09 02:32:46 2015 +0100
@@ -125,7 +125,7 @@
val raw_bn_eqs = the simps
val raw_bn_info =
- prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs)
+ prep_bn_info lthy raw_dt_names raw_dts fs (map Thm.prop_of raw_bn_eqs)
in
(fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
end
@@ -166,7 +166,7 @@
binders
|> map (bind_fn lthy args)
|> split_list
- |> pairself combine_fn
+ |> apply2 combine_fn
end
val t1 = map (mk_fv_body fv_map args) bodies
@@ -199,7 +199,7 @@
fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses =
let
- val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names = Old_Datatype_Prop.make_tnames arg_tys
val args = map Free (arg_names ~~ arg_tys)
val fv = lookup fv_map ty
val lhs = fv $ list_comb (constr, args)
@@ -211,7 +211,7 @@
fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
let
- val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names = Old_Datatype_Prop.make_tnames arg_tys
val args = map Free (arg_names ~~ arg_tys)
val fv_bn = lookup fv_bn_map bn_trm
val lhs = fv_bn $ list_comb (constr, args)
@@ -287,7 +287,7 @@
fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) =
let
val p = Free ("p", @{typ perm})
- val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names = Old_Datatype_Prop.make_tnames arg_tys
val args = map Free (arg_names ~~ arg_tys)
val perm_bn = lookup perm_bn_map bn_trm
val lhs = perm_bn $ p $ list_comb (constr, args)
@@ -347,7 +347,7 @@
fun prove_permute_zero induct perm_defs perm_fns ctxt =
let
val perm_types = map (body_type o fastype_of) perm_fns
- val perm_indnames = Datatype_Prop.make_tnames perm_types
+ val perm_indnames = Old_Datatype_Prop.make_tnames perm_types
fun single_goal ((perm_fn, T), x) =
HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
@@ -358,11 +358,11 @@
val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs)
- val tac = (Datatype_Aux.ind_tac induct perm_indnames
+ val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
THEN_ALL_NEW asm_simp_tac simpset) 1
in
Goal.prove ctxt perm_indnames [] goals (K tac)
- |> Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
end
@@ -371,7 +371,7 @@
val p = Free ("p", @{typ perm})
val q = Free ("q", @{typ perm})
val perm_types = map (body_type o fastype_of) perm_fns
- val perm_indnames = Datatype_Prop.make_tnames perm_types
+ val perm_indnames = Old_Datatype_Prop.make_tnames perm_types
fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
(perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
@@ -383,11 +383,11 @@
(* FIXME proper goal context *)
val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs)
- val tac = (Datatype_Aux.ind_tac induct perm_indnames
+ val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
THEN_ALL_NEW asm_simp_tac simpset) 1
in
Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac)
- |> Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
end
@@ -403,7 +403,7 @@
fastype_of cnstr
|> strip_type
- val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+ val arg_names = Name.variant_list ["p"] (Old_Datatype_Prop.make_tnames arg_tys)
val args = map Free (arg_names ~~ arg_tys)
val lhs = lookup_perm p (ty, list_comb (cnstr, args))
@@ -430,8 +430,8 @@
val perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns)
- fun tac _ (_, _, simps) =
- Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+ fun tac ctxt (_, _, simps) =
+ Class.intro_classes_tac ctxt [] THEN ALLGOALS (resolve_tac ctxt simps)
fun morphism phi (fvs, dfs, simps) =
(map (Morphism.term phi) fvs,
@@ -442,7 +442,7 @@
lthy
|> Local_Theory.exit_global
|> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt})
- |> Primrec.add_primrec perm_fn_binds perm_eqs
+ |> BNF_LFP_Compat.primrec perm_fn_binds perm_eqs
val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy'
val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy'
@@ -468,7 +468,7 @@
fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
HEADGOAL
(Object_Logic.full_atomize_tac ctxt
- THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))
+ THEN' (DETERM o (Induct_Tacs.induct_tac ctxt insts (SOME ind_thms)))
THEN_ALL_NEW subproof_tac const_names simps ctxt)
fun mk_eqvt_goal pi const arg =
@@ -491,13 +491,13 @@
|> map fastype_of
|> map domain_type
val (arg_names, ctxt'') =
- Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
+ Variable.variant_fixes (Old_Datatype_Prop.make_tnames arg_tys) ctxt'
val args = map Free (arg_names ~~ arg_tys)
val goals = map2 (mk_eqvt_goal p) consts args
val insts = map (single o SOME) arg_names
val const_names = map (fst o dest_Const) consts
in
- Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} =>
+ Goal.prove_common ctxt'' NONE [] [] goals (fn {context, ...} =>
prove_eqvt_tac insts ind_thms const_names simps context)
|> Proof_Context.export ctxt'' ctxt
end
--- a/Nominal/nominal_eqvt.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_eqvt.ML Thu Jul 09 02:32:46 2015 +0100
@@ -32,8 +32,7 @@
fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
let
- val thy = Proof_Context.theory_of ctxt
- val cpi = Thm.cterm_of thy pi
+ val cpi = Thm.cterm_of ctxt pi
val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
val eqvt_sconfig = eqvt_strict_config addexcls pred_names
val simps1 =
@@ -48,7 +47,7 @@
val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems'
val prems''' = map (simplify simps2 o simplify simps1) prems''
in
- HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems'''))
+ HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems'''))
end) ctxt
end
@@ -92,7 +91,7 @@
val (([raw_concl], [raw_pi]), ctxt') =
ctxt
- |> Variable.import_terms false [concl_of raw_induct']
+ |> Variable.import_terms false [Thm.concl_of raw_induct']
||>> Variable.variant_fixes ["p"]
val pi = Free (raw_pi, @{typ perm})
@@ -108,7 +107,7 @@
in
Goal.prove ctxt' [] [] goal
(fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1)
- |> Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
|> Proof_Context.export ctxt' ctxt
|> map (fn th => th RS mp)
|> map zero_var_indexes
@@ -140,7 +139,7 @@
end
val _ =
- Outer_Syntax.local_theory @{command_spec "equivariance"}
+ Outer_Syntax.local_theory @{command_keyword equivariance}
"Proves equivariance for inductive predicate involving nominal datatypes."
(Parse.const >> equivariance_cmd)
--- a/Nominal/nominal_function.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_function.ML Thu Jul 09 02:32:46 2015 +0100
@@ -27,9 +27,6 @@
(Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config ->
bool -> local_theory -> Proof.state
- val setup : theory -> theory
- val get_congs : Proof.context -> thm list
-
val get_info : Proof.context -> term -> nominal_info
end
@@ -106,10 +103,10 @@
val simp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Code.add_default_eqn_attribute,
- Nitpick_Simps.add]
+ Named_Theorems.add @{named_theorems nitpick_simp}]
val psimp_attribs = map (Attrib.internal o K)
- [Nitpick_Psimps.add]
+ [Named_Theorems.add @{named_theorems nitpick_psimp}]
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
@@ -159,19 +156,19 @@
val fnames = map (fst o fst) fixes
fun qualify n = Binding.name n
|> Binding.qualify true defname
- val conceal_partial = if partials then I else Binding.conceal
+ val concealed_partial = if partials then I else Binding.concealed
val addsmps = add_simps fnames post sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (conceal_partial o Binding.qualify false "partial")
- "psimps" conceal_partial psimp_attribs psimps
- ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+ |> addsmps (concealed_partial o Binding.qualify false "partial")
+ "psimps" concealed_partial psimp_attribs psimps
+ ||>> Local_Theory.note ((concealed_partial (qualify "pinduct"),
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
- ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
+ ||>> Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination])
||> (snd o Local_Theory.note ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
||> (case domintros of NONE => I | SOME thms =>
@@ -216,7 +213,7 @@
prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
in
lthy'
- |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
+ |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
|> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
end
@@ -225,31 +222,6 @@
fun nominal_function_cmd a b c int =
gen_nominal_function int Specification.read_spec "_::type" a b c
-
-fun add_case_cong n thy =
- let
- val cong = #case_cong (Datatype.the_info thy n)
- |> safe_mk_meta_eq
- in
- Context.theory_map
- (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
- end
-
-val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
-
-
-
-(* setup *)
-
-val setup =
- Attrib.setup @{binding fundef_cong}
- (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
- "declaration of congruence rule for function definitions"
- #> setup_case_cong
- #> Function_Common.Termination_Simps.setup
-
-val get_congs = Function_Ctx_Tree.get_function_congs
-
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
|> the_single |> snd
@@ -275,7 +247,7 @@
(* nominal *)
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_function"}
+ Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function}
"define general recursive nominal functions"
(nominal_function_parser nominal_default_config
>> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
--- a/Nominal/nominal_function_common.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_function_common.ML Thu Jul 09 02:32:46 2015 +0100
@@ -15,7 +15,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms: *)
add_simps : (binding -> binding) -> string -> (binding -> binding) ->
- Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+ Token.src list -> thm list -> local_theory -> thm list * local_theory,
case_names : string list,
fs : term list,
R : term,
@@ -37,7 +37,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms: *)
add_simps : (binding -> binding) -> string -> (binding -> binding) ->
- Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+ Token.src list -> thm list -> local_theory -> thm list * local_theory,
case_names : string list,
fs : term list,
R : term,
@@ -64,7 +64,7 @@
structure NominalFunctionData = Generic_Data
(
type T = (term * nominal_info) Item_Net.T;
- val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
+ val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst);
val extend = I;
fun merge tabs : T = Item_Net.merge tabs;
)
@@ -72,9 +72,9 @@
val get_function = NominalFunctionData.get o Context.Proof;
-fun lift_morphism thy f =
+fun lift_morphism ctxt f =
let
- fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
+ fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t))
in
Morphism.morphism "lift_morphism"
{binding = [],
@@ -85,12 +85,11 @@
fun import_function_data t ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val ct = cterm_of thy t
- val inst_morph = lift_morphism thy o Thm.instantiate
+ val ct = Thm.cterm_of ctxt t
+ val inst_morph = lift_morphism ctxt o Thm.instantiate
fun match (trm, data) =
- SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+ SOME (morph_function_data data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))))
handle Pattern.MATCH => NONE
in
get_first match (Item_Net.retrieve (get_function ctxt) t)
--- a/Nominal/nominal_function_core.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_function_core.ML Thu Jul 09 02:32:46 2015 +0100
@@ -83,7 +83,7 @@
{no: int,
qglr : ((string * typ) list * term list * term * term),
cdata : clause_context,
- tree: Function_Ctx_Tree.ctx_tree,
+ tree: Function_Context_Tree.ctx_tree,
lGI: thm,
RCs: rec_call_info list}
@@ -109,7 +109,7 @@
([], (fixes, assumes, arg) :: xs)
| add_Ri _ _ _ _ = raise Match
in
- rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
+ rev (Function_Context_Tree.traverse_tree add_Ri tree [])
end
(* nominal *)
@@ -147,14 +147,14 @@
(** building proof obligations *)
fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) =
mk_eqvt_at (fvar, arg)
- |> curry Logic.list_implies (map prop_of assms)
+ |> curry Logic.list_implies (map Thm.prop_of assms)
|> fold_rev (Logic.all o Free) vs
|> fold_rev absfree qs
|> strip_abs_body
fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) =
mk_inv inv (fvar, arg)
- |> curry Logic.list_implies (map prop_of assms)
+ |> curry Logic.list_implies (map Thm.prop_of assms)
|> fold_rev (Logic.all o Free) vs
|> fold_rev absfree qs
|> strip_abs_body
@@ -207,17 +207,15 @@
val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
- val thy = Proof_Context.theory_of ctxt'
-
fun inst t = subst_bounds (rev qs, t)
val gs = map inst pre_gs
val lhs = inst pre_lhs
val rhs = inst pre_rhs
- val cqs = map (cterm_of thy) qs
- val ags = map (Thm.assume o cterm_of thy) gs
+ val cqs = map (Thm.cterm_of ctxt') qs
+ val ags = map (Thm.assume o Thm.cterm_of ctxt') gs
- val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+ val case_hyp = Thm.assume (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
in
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
cqs = cqs, ags = ags, case_hyp = case_hyp }
@@ -245,7 +243,7 @@
val Globals {h, ...} = globals
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Thm.cterm_of ctxt
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
val lGI = GIntro_thm
@@ -263,7 +261,7 @@
val h_assum =
HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (Logic.all o Free) rcfix
|> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] []
|> abstract_over_list (rev qs)
@@ -293,12 +291,12 @@
(* nominal *)
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
(* if j < i, then turn around *)
-fun get_compat_thm thy cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
+fun get_compat_thm ctxt cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
let
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
- val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+ val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
in if j < i then
let
@@ -333,7 +331,7 @@
(* Generates the replacement lemma in fully quantified form. *)
-fun mk_replacement_lemma thy h ih_elim clause =
+fun mk_replacement_lemma ctxt h ih_elim clause =
let
val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
RCs, tree, ...} = clause
@@ -346,16 +344,16 @@
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
val h_assums = map (fn RCInfo {h_assum, ...} =>
- Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+ Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs
val (eql, _) =
- Function_Ctx_Tree.rewrite_by_tree (Proof_Context.init_global thy)
+ Function_Context_Tree.rewrite_by_tree ctxt
h ih_elim_case (Ris ~~ h_assums) tree
val replace_lemma = (eql RS meta_eq_to_obj_eq)
- |> Thm.implies_intr (cprop_of case_hyp)
- |> fold_rev (Thm.implies_intr o cprop_of) h_assums
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
|> Thm.close_derivation
in
@@ -364,7 +362,7 @@
(* nominal *)
(* Generates the eqvt lemmas for each clause *)
-fun mk_eqvt_lemma thy ih_eqvt clause =
+fun mk_eqvt_lemma ctxt ih_eqvt clause =
let
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
@@ -377,18 +375,18 @@
fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_eqvt_case)
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
in
map prep_eqvt RCs
- |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
- |> map (Thm.implies_intr (cprop_of case_hyp))
+ |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
+ |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
|> map (fold_rev Thm.forall_intr cqs)
|> map (Thm.close_derivation)
end
(* nominal *)
-fun mk_invariant_lemma thy ih_inv clause =
+fun mk_invariant_lemma ctxt ih_inv clause =
let
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
@@ -401,19 +399,21 @@
fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_inv_case)
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
in
map prep_inv RCs
- |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
- |> map (Thm.implies_intr (cprop_of case_hyp))
+ |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
+ |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
|> map (fold_rev Thm.forall_intr cqs)
|> map (Thm.close_derivation)
end
(* nominal *)
-fun mk_uniqueness_clause thy globals compat_store eqvts invs clausei clausej RLj =
+fun mk_uniqueness_clause ctxt globals compat_store eqvts invs clausei clausej RLj =
let
+ val thy = Proof_Context.theory_of ctxt
+
val Globals {h, y, x, fvar, ...} = globals
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi,
ags = agsi, ...}, ...} = clausei
@@ -425,10 +425,11 @@
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
val Ghsj' = map
- (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+ (fn RCInfo {h_assum, ...} =>
+ Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj
- val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
- val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+ val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+ val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
(* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
@@ -458,7 +459,7 @@
|> map (fold Thm.elim_implies [case_hypj'])
|> map (fold Thm.elim_implies agsj')
- val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
+ val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
in
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
@@ -468,70 +469,71 @@
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
|> (fn it => trans OF [y_eq_rhsj'h, it])
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
- |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
- |> fold_rev (Thm.implies_intr o cprop_of) agsj'
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj'
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj'
(* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
- |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
- |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
- |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
+ |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h)
+ |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj')
+ |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj')
end
(* nominal *)
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems
- clausei =
+fun mk_uniqueness_case ctxt
+ globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei =
let
+ val thy = Proof_Context.theory_of ctxt
+
val Globals {x, y, ranT, fvar, ...} = globals
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
val ih_intro_case =
- full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+ full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp])
ih_intro
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_intro_case)
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
val existence = fold (curry op COMP o prep_RC) RCs lGI
- val P = cterm_of thy (mk_eq (y, rhsC))
- val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+ val P = Thm.cterm_of ctxt (mk_eq (y, rhsC))
+ val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y)))
val unique_clauses =
- map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
+ map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems
fun elim_implies_eta A AB =
- Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+ Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
|> Seq.list_of |> the_single
val uniqueness = G_cases
- |> Thm.forall_elim (cterm_of thy lhs)
- |> Thm.forall_elim (cterm_of thy y)
+ |> Thm.forall_elim (Thm.cterm_of ctxt lhs)
+ |> Thm.forall_elim (Thm.cterm_of ctxt y)
|> Thm.forall_elim P
|> Thm.elim_implies G_lhs_y
|> fold elim_implies_eta unique_clauses
- |> Thm.implies_intr (cprop_of G_lhs_y)
- |> Thm.forall_intr (cterm_of thy y)
+ |> Thm.implies_intr (Thm.cprop_of G_lhs_y)
+ |> Thm.forall_intr (Thm.cterm_of ctxt y)
- val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+ val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
val exactly_one =
- ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+ ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
- |> simplify
- (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym])
- |> Thm.implies_intr (cprop_of case_hyp)
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
val function_value =
existence
|> Thm.implies_intr ihyp
- |> Thm.implies_intr (cprop_of case_hyp)
- |> Thm.forall_intr (cterm_of thy x)
- |> Thm.forall_elim (cterm_of thy lhs)
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x)
+ |> Thm.forall_elim (Thm.cterm_of ctxt lhs)
|> curry (op RS) refl
in
(exactly_one, function_value)
@@ -539,57 +541,58 @@
(* nominal *)
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
+fun prove_stuff ctxt
+ globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
let
val Globals {h, domT, ranT, x, ...} = globals
- val thy = Proof_Context.theory_of ctxt
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
- |> instantiate' [] [NONE, SOME (cterm_of thy h)]
+ |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
val _ = trace_msg (K "Proving Replacement lemmas...")
- val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+ val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
val _ = trace_msg (K "Proving Equivariance lemmas...")
- val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
+ val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses
val _ = trace_msg (K "Proving Invariance lemmas...")
- val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses
+ val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses
val _ = trace_msg (K "Proving cases for unique existence...")
val (ex1s, values) =
- split_list (map (mk_uniqueness_case thy globals G f
+ split_list (map (mk_uniqueness_case ctxt globals G f
ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses)
val _ = trace_msg (K "Proving: Graph is a function")
val graph_is_function = complete
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) ex1s
- |> Thm.implies_intr (ihyp)
- |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
- |> Thm.forall_intr (cterm_of thy x)
+ |> Thm.implies_intr ihyp
+ |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+ |> Thm.forall_intr (Thm.cterm_of ctxt x)
|> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
- |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
+ |> (fn it =>
+ fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it)
val goalstate =
- Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
+ Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
|> Thm.close_derivation
|> Goal.protect 0
- |> fold_rev (Thm.implies_intr o cprop_of) compat
- |> Thm.implies_intr (cprop_of complete)
- |> Thm.implies_intr (cprop_of invariant)
- |> Thm.implies_intr (cprop_of G_eqvt)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
+ |> Thm.implies_intr (Thm.cprop_of complete)
+ |> Thm.implies_intr (Thm.cprop_of invariant)
+ |> Thm.implies_intr (Thm.cprop_of G_eqvt)
in
(goalstate, values)
end
@@ -599,7 +602,7 @@
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
lthy
- |> Local_Theory.conceal
+ |> Proof_Context.concealed
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
@@ -612,14 +615,14 @@
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
[] (* no special monos *)
- ||> Local_Theory.restore_naming lthy
+ ||> Proof_Context.restore_naming lthy
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Thm.cterm_of lthy
fun requantify orig_intro thm =
let
val (qs, t) = dest_all_all orig_intro
val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
- val vars = Term.add_vars (prop_of thm) []
+ val vars = Term.add_vars (Thm.prop_of thm) []
val varmap = AList.lookup (op =) (frees ~~ map fst vars)
#> the_default ("",0)
in
@@ -640,7 +643,7 @@
let
fun mk_h_assm (rcfix, rcassm, rcarg) =
HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (Logic.all o Free) rcfix
in
HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
@@ -663,7 +666,7 @@
in
Local_Theory.define
((Binding.name (function_name fname), mixfix),
- ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
+ ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
end
(* nominal *)
@@ -674,7 +677,7 @@
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (Logic.all o Free) rcfix
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
@@ -691,7 +694,7 @@
fun fix_globals domT ranT fvar ctxt =
let
- val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
+ val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes
["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
in
(Globals {h = Free (h, domT --> ranT),
@@ -708,11 +711,11 @@
ctxt')
end
-fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
+fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) =
let
fun inst_term t = subst_bound(f, abstract_over (fvar, t))
in
- (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
+ (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg)
end
@@ -721,23 +724,23 @@
* PROVING THE RULES
**********************************************************)
-fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
+fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function =
let
val Globals {domT, z, ...} = globals
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
let
- val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
in
((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
|> (fn it => it COMP graph_is_function)
|> Thm.implies_intr z_smaller
- |> Thm.forall_intr (cterm_of thy z)
+ |> Thm.forall_intr (Thm.cterm_of ctxt z)
|> (fn it => it COMP valthm)
|> Thm.implies_intr lhs_acc
- |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff])
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff])
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
in
@@ -751,34 +754,34 @@
val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
-fun mk_partial_induct_rule thy globals R complete_thm clauses =
+fun mk_partial_induct_rule ctxt globals R complete_thm clauses =
let
val Globals {domT, x, z, a, P, D, ...} = globals
val acc_R = mk_acc domT R
- val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
- val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
+ val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x)))
+ val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a))
- val D_subset = cterm_of thy (Logic.all x
+ val D_subset = Thm.cterm_of ctxt (Logic.all x
(Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
HOLogic.mk_Trueprop (D $ z)))))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (P $ Bound 0)))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val aihyp = Thm.assume ihyp
fun prove_case clause =
let
- val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
+ val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...},
RCs, qglr = (oqs, _, _, _), ...} = clause
val case_hyp_conv = K (case_hyp RS eq_reflection)
@@ -786,23 +789,23 @@
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
val sih =
fconv_rule (Conv.binder_conv
- (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+ (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp
end
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
- |> Thm.forall_elim (cterm_of thy rcarg)
+ |> Thm.forall_elim (Thm.cterm_of ctxt rcarg)
|> Thm.elim_implies llRI
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
val step = HOLogic.mk_Trueprop (P $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val P_lhs = Thm.assume step
|> fold Thm.forall_elim cqs
@@ -810,12 +813,13 @@
|> fold Thm.elim_implies ags
|> fold Thm.elim_implies P_recs
- val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
+ val res =
+ Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x))
|> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
|> Thm.symmetric (* P lhs == P x *)
|> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
- |> Thm.implies_intr (cprop_of case_hyp)
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
in
(res, step)
@@ -827,8 +831,8 @@
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) cases (* P x *)
|> Thm.implies_intr ihyp
- |> Thm.implies_intr (cprop_of x_D)
- |> Thm.forall_intr (cterm_of thy x)
+ |> Thm.implies_intr (Thm.cprop_of x_D)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x)
val subset_induct_rule =
acc_subset_induct
@@ -843,16 +847,16 @@
val simple_induct_rule =
subset_induct_rule
- |> Thm.forall_intr (cterm_of thy D)
- |> Thm.forall_elim (cterm_of thy acc_R)
- |> assume_tac 1 |> Seq.hd
+ |> Thm.forall_intr (Thm.cterm_of ctxt D)
+ |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
+ |> atac 1 |> Seq.hd
|> (curry op COMP) (acc_downward
- |> (instantiate' [SOME (ctyp_of thy domT)]
- (map (SOME o cterm_of thy) [R, x, z]))
- |> Thm.forall_intr (cterm_of thy z)
- |> Thm.forall_intr (cterm_of thy x))
- |> Thm.forall_intr (cterm_of thy a)
- |> Thm.forall_intr (cterm_of thy P)
+ |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
+ (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
+ |> Thm.forall_intr (Thm.cterm_of ctxt z)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x))
+ |> Thm.forall_intr (Thm.cterm_of ctxt a)
+ |> Thm.forall_intr (Thm.cterm_of ctxt P)
in
simple_induct_rule
end
@@ -861,16 +865,15 @@
(* FIXME: broken by design *)
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
let
- val thy = Proof_Context.theory_of ctxt
val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
|> fold_rev (curry Logic.mk_implies) gs
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
in
Goal.init goal
- |> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
+ |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the
+ |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (auto_tac ctxt)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -884,36 +887,36 @@
val wf_in_rel = @{thm Fun_Def.wf_in_rel}
val in_rel_def = @{thm Fun_Def.in_rel_def}
-fun mk_nest_term_case thy globals R' ihyp clause =
+fun mk_nest_term_case ctxt globals R' ihyp clause =
let
val Globals {z, ...} = globals
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
qglr=(oqs, _, _, _), ...} = clause
val ih_case =
- full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+ full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp])
ihyp
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = (u @ sub)
- |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
+ |> map (fn (ctx,thm) => Function_Context_Tree.export_thm ctxt ctx thm)
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
- |> Function_Ctx_Tree.export_term (fixes, assumes)
- |> fold_rev (curry Logic.mk_implies o prop_of) ags
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *)
+ |> Function_Context_Tree.export_term (fixes, assumes)
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val thm = Thm.assume hyp
|> fold Thm.forall_elim cqs
|> fold Thm.elim_implies ags
- |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
+ |> Function_Context_Tree.import_thm ctxt (fixes, assumes)
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
- |> cterm_of thy |> Thm.assume
+ |> Thm.cterm_of ctxt |> Thm.assume
val acc = thm COMP ih_case
val z_acc_local = acc
@@ -921,7 +924,7 @@
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
val ethm = z_acc_local
- |> Function_Ctx_Tree.export_thm thy (fixes,
+ |> Function_Context_Tree.export_thm ctxt (fixes,
z_eq_arg :: case_hyp :: ags @ assumes)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -931,11 +934,11 @@
end
| step _ _ _ _ = raise Match
in
- Function_Ctx_Tree.traverse_tree step tree
+ Function_Context_Tree.traverse_tree step tree
end
-fun mk_nest_term_rule thy globals R R_cases clauses =
+fun mk_nest_term_rule ctxt globals R R_cases clauses =
let
val Globals { domT, x, z, ... } = globals
val acc_R = mk_acc domT R
@@ -948,42 +951,42 @@
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
(domT --> domT --> boolT) --> boolT) $ R')
- |> cterm_of thy (* "wf R'" *)
+ |> Thm.cterm_of ctxt (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
HOLogic.mk_Trueprop (acc_R $ Bound 0)))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
- val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+ val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x))
- val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
+ val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
in
R_cases
- |> Thm.forall_elim (cterm_of thy z)
- |> Thm.forall_elim (cterm_of thy x)
- |> Thm.forall_elim (cterm_of thy (acc_R $ z))
+ |> Thm.forall_elim (Thm.cterm_of ctxt z)
+ |> Thm.forall_elim (Thm.cterm_of ctxt x)
+ |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z))
|> curry op COMP (Thm.assume R_z_x)
|> fold_rev (curry op COMP) cases
|> Thm.implies_intr R_z_x
- |> Thm.forall_intr (cterm_of thy z)
+ |> Thm.forall_intr (Thm.cterm_of ctxt z)
|> (fn it => it COMP accI)
|> Thm.implies_intr ihyp
- |> Thm.forall_intr (cterm_of thy x)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x)
|> (fn it => Drule.compose (it, 2, wf_induct_rule))
|> curry op RS (Thm.assume wfR')
|> forall_intr_vars
|> (fn it => it COMP allI)
|> fold Thm.implies_intr hyps
|> Thm.implies_intr wfR'
- |> Thm.forall_intr (cterm_of thy R')
- |> Thm.forall_elim (cterm_of thy (inrel_R))
+ |> Thm.forall_intr (Thm.cterm_of ctxt R')
+ |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R))
|> curry op RS wf_in_rel
- |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def])
- |> Thm.forall_intr (cterm_of thy Rrel)
+ |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
+ |> Thm.forall_intr (Thm.cterm_of ctxt Rrel)
end
@@ -1014,7 +1017,7 @@
val n = length abstract_qglrs
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
- Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
+ Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs
val trees = map build_tree clauses
val RCss = map find_calls trees
@@ -1025,8 +1028,8 @@
val ((f, (_, f_defthm)), lthy) =
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
- val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
- val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
+ val RCss = map (map (inst_RC lthy fvar f)) RCss
+ val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
val ((R, RIntro_thmss, R_elim), lthy) =
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
@@ -1037,10 +1040,10 @@
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Thm.cterm_of lthy
val xclauses = PROFILE "xclauses"
- (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
+ (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
RCss GIntro_thms) RIntro_thmss
val complete =
@@ -1062,7 +1065,8 @@
fun mk_partial_rules provedgoal =
let
- val newthy = theory_of_thm provedgoal (*FIXME*)
+ val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
+ val newctxt = Proof_Context.init_global newthy (*FIXME*)
val ((graph_is_function, complete_thm), graph_is_eqvt) =
provedgoal
@@ -1075,13 +1079,13 @@
val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
val psimps = PROFILE "Proving simplification rules"
- (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+ (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function
val simple_pinduct = PROFILE "Proving partial induction rule"
- (mk_partial_induct_rule newthy globals R complete_thm) xclauses
+ (mk_partial_induct_rule newctxt globals R complete_thm) xclauses
val total_intro = PROFILE "Proving nested termination rule"
- (mk_nest_term_rule newthy globals R R_elim) xclauses
+ (mk_nest_term_rule newctxt globals R R_elim) xclauses
val dom_intros =
if domintros then SOME (PROFILE "Proving domain introduction rules"
--- a/Nominal/nominal_induct.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_induct.ML Thu Jul 09 02:32:46 2015 +0100
@@ -57,7 +57,7 @@
end;
val substs =
map2 subst insts concls |> flat |> distinct (op =)
- |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
+ |> map (apply2 (Thm.cterm_of ctxt));
in
(((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule)
end;
@@ -86,9 +86,6 @@
fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
-
val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs;
@@ -99,7 +96,7 @@
fun rule_cases ctxt r =
let val r' = if simp then Induct.simplified_rule ctxt r else r
- in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
+ in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
in
(fn i => fn st =>
rules
@@ -110,7 +107,7 @@
(CONJUNCTS (ALLGOALS
let
val adefs = nth_list atomized_defs (j - 1);
- val frees = fold (Term.add_frees o prop_of) adefs [];
+ val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
val xs = nth_list fixings (j - 1);
val k = nth concls (j - 1) + more_consumes
in
@@ -131,7 +128,7 @@
(Tactic.rtac (rename_params_rule false [] rule') i THEN
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
THEN_ALL_NEW_CASES
- ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
+ ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
else K all_tac)
THEN_ALL_NEW Induct.rulify_tac ctxt)
end;
@@ -176,9 +173,8 @@
Scan.lift (Args.mode Induct.no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) >>
- (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
+ (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
+ HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
end
--- a/Nominal/nominal_inductive.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_inductive.ML Thu Jul 09 02:32:46 2015 +0100
@@ -35,7 +35,7 @@
| 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
@@ -81,7 +81,7 @@
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)
@@ -156,7 +156,7 @@
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
@@ -172,34 +172,33 @@
|> 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 cperms = map (cterm_of thy o perm_const) prm_tys
+ val prm_tys = map (fastype_of o Thm.term_of) prms
+ 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,
- helper_tac false prm p context ]
+ eqvt_stac ctxt',
+ 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
@@ -232,9 +231,8 @@
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
@@ -243,7 +241,7 @@
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},
@@ -256,7 +254,7 @@
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)
@@ -277,13 +275,13 @@
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)
- (fn {context, ...} =>
- EVERY1 [ CONVERSION (expand_conv_bot context),
- eqvt_stac context,
+ val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl)
+ (fn {context = ctxt'', ...} =>
+ EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
+ eqvt_stac ctxt'',
rtac prem',
RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
- |> singleton (Proof_Context.export ctxt' ctxt)
+ |> singleton (Proof_Context.export ctxt' ctxt)
in
rtac side_thm 1
end) ctxt
@@ -310,23 +308,22 @@
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
@@ -369,7 +366,7 @@
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}))
@@ -417,7 +414,7 @@
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
@@ -439,7 +436,7 @@
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
--- a/Nominal/nominal_library.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_library.ML Thu Jul 09 02:32:46 2015 +0100
@@ -86,7 +86,7 @@
(* datatype operations *)
type cns_info = (term * typ * typ list * bool list) list
- val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list
+ val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list
(* tactics for function package *)
val size_ss: simpset
@@ -333,10 +333,10 @@
let
fun aux ((ty_name, vs), (cname, args)) =
let
- val vs_tys = map (Datatype_Aux.typ_of_dtyp descr) vs
+ val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs
val ty = Type (ty_name, vs_tys)
- val arg_tys = map (Datatype_Aux.typ_of_dtyp descr) args
- val is_rec = map Datatype_Aux.is_rec_type args
+ val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args
+ val is_rec = map Old_Datatype_Aux.is_rec_type args
in
(Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
end
@@ -451,13 +451,13 @@
val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def}
in
EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
- REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac monos)),
- REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
+ REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)),
+ REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))]
end
fun map_thm ctxt f tac thm =
let
- val opt_goal_trm = map_term f (prop_of thm)
+ val opt_goal_trm = map_term f (Thm.prop_of thm)
in
case opt_goal_trm of
NONE => thm
@@ -495,7 +495,7 @@
fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars;
fun atomize_rule ctxt i thm =
Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm
-fun atomize_concl ctxt thm = atomize_rule ctxt (length (prems_of thm)) thm
+fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm
(* applies a tactic to a formula composed of conjunctions *)
--- a/Nominal/nominal_mutual.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_mutual.ML Thu Jul 09 02:32:46 2015 +0100
@@ -138,7 +138,7 @@
val ((f, (_, f_defthm)), lthy') =
Local_Theory.define
((Binding.name fname, mixfix),
- ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+ ((Binding.concealed (Binding.name (fname ^ "_def")), []),
Term.subst_bound (fsum, f_def))) lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
@@ -156,8 +156,6 @@
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
let
- val thy = Proof_Context.theory_of ctxt
-
val oqnames = map fst pre_qs
val (qs, _) = Variable.variant_fixes oqnames ctxt
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
@@ -167,13 +165,13 @@
val args = map inst pre_args
val rhs = inst pre_rhs
- val cqs = map (cterm_of thy) qs
- val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt
+ val cqs = map (Thm.cterm_of ctxt) qs
+ val (ags, ctxt') = fold_map Thm.assume_hyps (map (Thm.cterm_of ctxt) gs) ctxt
val import = fold Thm.forall_elim cqs
#> fold Thm.elim_implies ags
- val export = fold_rev (Thm.implies_intr o cprop_of) ags
+ val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags
#> fold_rev forall_intr_rename (oqnames ~~ cqs)
in
F ctxt' (f, qs, gs, args, rhs) import export
@@ -242,8 +240,7 @@
fun mk_applied_form ctxt caTs thm =
let
- val thy = Proof_Context.theory_of ctxt
- val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
+ val xs = map_index (fn (i,T) => Thm.cterm_of ctxt (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
in
fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
|> Conv.fconv_rule (Thm.beta_conversion true)
@@ -253,7 +250,7 @@
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
let
- val cert = cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Thm.cterm_of ctxt
val newPs =
map2 (fn Pname => fn MutualPart {cargTs, ...} =>
Free (Pname, cargTs ---> HOLogic.boolT))
@@ -314,7 +311,7 @@
(* extracting the acc-premises from the induction theorems *)
val acc_prems =
- map prop_of induct_thms
+ map Thm.prop_of induct_thms
|> map2 forall_elim_list argss
|> map (strip_qnt_body @{const_name Pure.all})
|> map (curry Logic.nth_prem 1)
@@ -333,19 +330,21 @@
val induct_thm = case induct_thms of
[thm] => thm
- |> Drule.gen_all
+ |> Drule.gen_all (Variable.maxidx_of ctxt')
|> Thm.permute_prems 0 1
- |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm)
+ |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm)
| thms => thms
- |> map Drule.gen_all
+ |> map (Drule.gen_all (Variable.maxidx_of ctxt'))
|> map (Rule_Cases.add_consumes 1)
|> snd o Rule_Cases.strict_mutual_rule ctxt'
|> atomize_concl ctxt'
- fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
+ fun tac ctxt thm =
+ rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt
in
Goal.prove ctxt' (flat arg_namess) [] goal
- (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
+ (fn {context = ctxt'', ...} =>
+ HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms)))
|> singleton (Proof_Context.export ctxt' ctxt)
|> split_conj_thm
|> map (fn th => th RS mp)
@@ -435,7 +434,7 @@
val G_name_aux = G_name ^ "_aux"
val subst = [(G, Free (G_name_aux, G_type))]
val GIntros_aux = GIntro_thms
- |> map prop_of
+ |> map Thm.prop_of
|> map (Term.subst_free subst)
|> map (subst_all case_sum_exp)
@@ -478,15 +477,16 @@
(K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1)))
fun aux_tac thm =
- rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (simpset1 addsimps [inj_thm]))
+ rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW
+ asm_full_simp_tac (simpset1 addsimps [inj_thm])
val iff1_thm = Goal.prove lthy''' [] [] goal_iff1
(K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms))))
- |> Drule.gen_all
+ |> Drule.gen_all (Variable.maxidx_of lthy''')
val iff2_thm = Goal.prove lthy''' [] [] goal_iff2
(K (HEADGOAL (DETERM o etac G_induct THEN' RANGE
(map (aux_tac o simplify simpset0) GIntro_aux_thms))))
- |> Drule.gen_all
+ |> Drule.gen_all (Variable.maxidx_of lthy''')
val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux)))
(K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm]))))
--- a/Nominal/nominal_permeq.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_permeq.ML Thu Jul 09 02:32:46 2015 +0100
@@ -101,8 +101,8 @@
fun trace_msg ctxt result =
let
- val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
- val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
+ val lhs_str = Syntax.string_of_term ctxt (Thm.term_of (Thm.lhs_of result))
+ val rhs_str = Syntax.string_of_term ctxt (Thm.term_of (Thm.rhs_of result))
in
warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
end
@@ -120,7 +120,7 @@
out the analysed term *)
fun trace_info_conv ctxt ctrm =
let
- val trm = term_of ctrm
+ val trm = Thm.term_of ctrm
val _ = case (head_of trm) of
@{const "Trueprop"} => ()
| _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
@@ -130,14 +130,14 @@
(* conversion for applications *)
fun eqvt_apply_conv ctrm =
- case (term_of ctrm) of
+ case Thm.term_of ctrm of
Const (@{const_name "permute"}, _) $ _ $ (_ $ _) =>
let
val (perm, t) = Thm.dest_comb ctrm
val (_, p) = Thm.dest_comb perm
val (f, x) = Thm.dest_comb t
- val a = ctyp_of_term x;
- val b = ctyp_of_term t;
+ val a = Thm.ctyp_of_cterm x;
+ val b = Thm.ctyp_of_cterm t;
val ty_insts = map SOME [b, a]
val term_insts = map SOME [p, f, x]
in
@@ -147,7 +147,7 @@
(* conversion for lambdas *)
fun eqvt_lambda_conv ctrm =
- case (term_of ctrm) of
+ case Thm.term_of ctrm of
Const (@{const_name "permute"}, _) $ _ $ (Abs _) =>
Conv.rewr_conv @{thm eqvt_lambda} ctrm
| _ => Conv.no_conv ctrm
@@ -166,7 +166,8 @@
(if strict_flag then error else warning)
("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
- val _ = case (term_of ctrm) of
+ val _ =
+ case Thm.term_of ctrm of
Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
| Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
| _ => ()
--- a/Nominal/nominal_termination.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_termination.ML Thu Jul 09 02:32:46 2015 +0100
@@ -26,7 +26,7 @@
val simp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Code.add_default_eqn_attribute,
- Nitpick_Simps.add]
+ Named_Theorems.add @{named_theorems nitpick_simp}]
val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
@@ -107,7 +107,7 @@
(Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (false))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_termination"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_termination}
"prove termination of a recursive nominal function"
(option_parser -- Scan.option Parse.term >>
(fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm))
--- a/Nominal/nominal_thmdecls.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_thmdecls.ML Thu Jul 09 02:32:46 2015 +0100
@@ -62,7 +62,6 @@
val eqvt_del: attribute
val eqvt_raw_add: attribute
val eqvt_raw_del: attribute
- val setup: theory -> theory
val get_eqvts_thms: Proof.context -> thm list
val get_eqvts_raw_thms: Proof.context -> thm list
val eqvt_transform: Proof.context -> thm -> thm
@@ -91,6 +90,11 @@
val eqvts = Item_Net.content o EqvtData.get
val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get
+val _ =
+ Theory.setup
+ (Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
+ Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw))
+
val get_eqvts_thms = eqvts o Context.Proof
val get_eqvts_raw_thms = eqvts_raw o Context.Proof
@@ -109,9 +113,9 @@
fun error_msg () =
error
("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^
- Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+ Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm))
in
- case prop_of thm of
+ case Thm.prop_of thm of
Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
c
@@ -151,7 +155,7 @@
(
if Item_Net.member (EqvtData.get context) thm then
warning ("Theorem already declared as equivariant:\n" ^
- Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+ Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm))
else ();
EqvtData.map (Item_Net.update thm) context
)
@@ -162,7 +166,7 @@
EqvtData.map (Item_Net.remove thm) context
else (
warning ("Cannot delete non-existing equivariance theorem:\n" ^
- Syntax.string_of_term (Context.proof_of context) (prop_of thm));
+ Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm));
context
)
)
@@ -187,7 +191,7 @@
fun thm_4_of_1 ctxt thm =
let
- val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop
+ val (p, c) = thm |> Thm.prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt)
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
@@ -209,7 +213,7 @@
let
val ss_thms = @{thms "permute_minus_cancel"(2)}
in
- EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac,
+ EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt,
rtac @{thm "permute_boolI"}, dtac thm',
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
end
@@ -218,7 +222,7 @@
fun thm_1_of_2 ctxt thm =
let
- val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop
+ val (prem, concl) = thm |> Thm.prop_of |> Logic.dest_implies |> apply2 HOLogic.dest_Trueprop
(* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded
or tuples, we need the following function to find ?p *)
fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p
@@ -228,10 +232,9 @@
val p = concl |> dest_comb |> snd |> find_perm
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
- val certify = cterm_of (theory_of_thm thm)
- val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm
+ val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm
in
- Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1)
+ Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1)
|> singleton (Proof_Context.export ctxt' ctxt)
end
handle TERM _ =>
@@ -254,7 +257,7 @@
(* Transforms a theorem of the form (1) or (2) into the form (4). *)
fun eqvt_transform ctxt thm =
- (case prop_of thm of @{const "Trueprop"} $ _ =>
+ (case Thm.prop_of thm of @{const "Trueprop"} $ _ =>
thm_4_of_1 ctxt thm
| @{const Pure.imp} $ _ $ _ =>
thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
@@ -268,7 +271,7 @@
(3)) and (4); transforms a theorem of the form (2) into
theorems of the form (3) and (4). *)
fun eqvt_and_raw_transform ctxt thm =
- (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) =>
+ (case Thm.prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) =>
let
val th' =
if fastype_of c_args = @{typ "bool"}
@@ -310,15 +313,11 @@
val eqvt_add = eqvt_add_or_del add_thm add_raw_thm
val eqvt_del = eqvt_add_or_del del_thm del_raw_thm
-
-(** setup function **)
-
-val setup =
- Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
- "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #>
- Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
- "Declaration of raw equivariance lemmas - no transformation is performed" #>
- Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
- Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
+ "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #>
+ Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
+ "Declaration of raw equivariance lemmas - no transformation is performed")
end;