--- a/Nominal/FROOT.ML Mon Oct 14 11:23:18 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-
-no_document use_thys
- ["Nominal2",
- "Atoms",
- "Eqvt"
- ];
-
-
-
--- a/Nominal/Nominal2.thy Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/Nominal2.thy Sun Dec 15 15:14:40 2013 +1100
@@ -271,7 +271,8 @@
in
raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps)
(Local_Theory.restore lthy_tmp)
- |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})
+ |> map (rewrite_rule (Local_Theory.restore lthy_tmp)
+ @{thms permute_nat_def[THEN eq_reflection]})
|> map (fn thm => thm RS @{thm sym})
end
@@ -302,7 +303,7 @@
val raw_funs_rsp_aux =
raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs)
- val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux
+ 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 =
@@ -315,12 +316,12 @@
val raw_size_rsp =
raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt)
- |> map mk_funs_rsp
+ |> map (mk_funs_rsp lthy5)
val raw_constrs_rsp =
raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux)
- val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
+ val alpha_permute_rsp = map (mk_alpha_permute_rsp lthy5) alpha_eqvt
val alpha_bn_rsp =
raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms
@@ -744,4 +745,8 @@
(main_parser >> nominal_datatype2_cmd)
*}
+
end
+
+
+
--- a/Nominal/Nominal2_Base.thy Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/Nominal2_Base.thy Sun Dec 15 15:14:40 2013 +1100
@@ -272,7 +272,7 @@
lemma permute_diff [simp]:
shows "(p - q) \<bullet> x = p \<bullet> - q \<bullet> x"
- unfolding diff_minus by simp
+ using permute_plus [of p "- q" x] by simp
lemma permute_minus_cancel [simp]:
shows "p \<bullet> - p \<bullet> x = x"
@@ -365,7 +365,7 @@
instance
apply default
apply (simp add: permute_perm_def)
-apply (simp add: permute_perm_def diff_minus minus_add add_assoc)
+apply (simp add: permute_perm_def algebra_simps)
done
end
@@ -373,12 +373,12 @@
lemma permute_self:
shows "p \<bullet> p = p"
unfolding permute_perm_def
- by (simp add: diff_minus add_assoc)
+ by (simp add: add_assoc)
lemma pemute_minus_self:
shows "- p \<bullet> p = p"
unfolding permute_perm_def
- by (simp add: diff_minus add_assoc)
+ by (simp add: add_assoc)
subsection {* Permutations for functions *}
@@ -870,7 +870,8 @@
fixes p q::"perm"
shows "p \<bullet> (- q) = - (p \<bullet> q)"
unfolding permute_perm_def
- by (simp add: diff_minus minus_add add_assoc)
+ by (simp add: diff_add_eq_diff_diff_swap)
+
subsubsection {* Equivariance of Logical Operators *}
--- a/Nominal/nominal_dt_alpha.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_dt_alpha.ML Sun Dec 15 15:14:40 2013 +1100
@@ -33,8 +33,8 @@
val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
- val mk_funs_rsp: thm -> thm
- val mk_alpha_permute_rsp: thm -> thm
+ val mk_funs_rsp: Proof.context -> thm -> thm
+ val mk_alpha_permute_rsp: Proof.context -> thm -> thm
end
structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -623,9 +623,9 @@
let
val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result
- val refl' = map (fold_rule [reflp_def'] o atomize) refl
- val symm' = map (fold_rule [symp_def'] o atomize) symm
- val trans' = map (fold_rule [transp_def'] o atomize) trans
+ val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl
+ val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm
+ val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans
fun prep_goal t =
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
@@ -834,7 +834,7 @@
alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct
(raw_prove_perm_bn_tac alpha_result simps) ctxt
|> Proof_Context.export ctxt' ctxt
- |> map atomize
+ |> map (atomize ctxt)
|> map single
|> map (curry (op OF) perm_bn_rsp)
end
@@ -846,9 +846,9 @@
val fun_rsp = @{lemma
"(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}
-fun mk_funs_rsp thm =
+fun mk_funs_rsp ctxt thm =
thm
- |> atomize
+ |> atomize ctxt
|> single
|> curry (op OF) fun_rsp
@@ -857,9 +857,9 @@
"(!x y p. R x y --> R (permute p x) (permute p y))
==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)}
-fun mk_alpha_permute_rsp thm =
+fun mk_alpha_permute_rsp ctxt thm =
thm
- |> atomize
+ |> atomize ctxt
|> single
|> curry (op OF) permute_rsp
--- a/Nominal/nominal_dt_quot.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_dt_quot.ML Sun Dec 15 15:14:40 2013 +1100
@@ -338,7 +338,7 @@
end)
in
induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
- |> map atomize
+ |> map (atomize ctxt)
|> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]}))
end
@@ -591,14 +591,14 @@
(* for freshness conditions *)
val tac1 = SOLVED' (EVERY'
[ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
- rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
+ rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
conj_tac (DETERM o resolve_tac fprops') ])
(* for equalities between constructors *)
val tac2 = SOLVED' (EVERY'
[ rtac (@{thm ssubst} OF prems),
- rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
- rewrite_goal_tac (map safe_mk_equiv abs_eqs),
+ 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)) ])
(* proves goal "P" *)
--- a/Nominal/nominal_dt_rawfuns.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML Sun Dec 15 15:14:40 2013 +1100
@@ -467,7 +467,7 @@
fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
HEADGOAL
- (Object_Logic.full_atomize_tac
+ (Object_Logic.full_atomize_tac ctxt
THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))
THEN_ALL_NEW subproof_tac const_names simps ctxt)
--- a/Nominal/nominal_function_common.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_function_common.ML Sun Dec 15 15:14:40 2013 +1100
@@ -76,8 +76,11 @@
let
fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
in
- Morphism.thm_morphism f $> Morphism.term_morphism term
- $> Morphism.typ_morphism (Logic.type_map term)
+ Morphism.morphism "lift_morphism"
+ {binding = [],
+ typ = [Logic.type_map term],
+ term = [term],
+ fact = [map f]}
end
fun import_function_data t ctxt =
--- a/Nominal/nominal_induct.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_induct.ML Sun Dec 15 15:14:40 2013 +1100
@@ -90,7 +90,7 @@
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;
+ val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs;
val finish_rule =
split_all_tuples defs_ctxt
@@ -104,7 +104,7 @@
(fn i => fn st =>
rules
|> inst_mutual_rule ctxt insts avoiding
- |> Rule_Cases.consume (flat defs) facts
+ |> Rule_Cases.consume ctxt (flat defs) facts
|> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
(CONJUNCTS (ALLGOALS
@@ -122,10 +122,10 @@
else
Induct.arbitrary_tac defs_ctxt k xs)
end)
- THEN' Induct.inner_atomize_tac) j))
- THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
+ THEN' Induct.inner_atomize_tac ctxt) j))
+ THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' =>
Induct.guess_instance ctxt
- (finish_rule (Induct.internalize more_consumes rule)) i st'
+ (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
|> Seq.maps (fn rule' =>
CASES (rule_cases ctxt rule' cases)
(Tactic.rtac (rename_params_rule false [] rule') i THEN
@@ -133,7 +133,7 @@
THEN_ALL_NEW_CASES
((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
else K all_tac)
- THEN_ALL_NEW Induct.rulify_tac)
+ THEN_ALL_NEW Induct.rulify_tac ctxt)
end;
--- a/Nominal/nominal_library.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_library.ML Sun Dec 15 15:14:40 2013 +1100
@@ -99,9 +99,9 @@
val transform_prem2: Proof.context -> string list -> thm -> thm
(* transformation into the object logic *)
- val atomize: thm -> thm
- val atomize_rule: int -> thm -> thm
- val atomize_concl: thm -> thm
+ val atomize: Proof.context -> thm -> thm
+ val atomize_rule: Proof.context -> int -> thm -> thm
+ val atomize_concl: Proof.context -> thm -> thm
(* applies a tactic to a formula composed of conjunctions *)
val conj_tac: (int -> tactic) -> int -> tactic
@@ -492,10 +492,10 @@
(* transforms a theorem into one of the object logic *)
-val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars;
-fun atomize_rule i thm =
- Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm
-fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm
+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
(* applies a tactic to a formula composed of conjunctions *)
--- a/Nominal/nominal_mutual.ML Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_mutual.ML Sun Dec 15 15:14:40 2013 +1100
@@ -335,12 +335,12 @@
[thm] => thm
|> Drule.gen_all
|> Thm.permute_prems 0 1
- |> (fn thm => atomize_rule (length (prems_of thm) - 1) thm)
+ |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm)
| thms => thms
|> map Drule.gen_all
|> map (Rule_Cases.add_consumes 1)
|> snd o Rule_Cases.strict_mutual_rule ctxt'
- |> atomize_concl
+ |> atomize_concl ctxt'
fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
in