--- a/Nominal/Ex/Datatypes.thy Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Ex/Datatypes.thy Thu Jun 16 20:07:03 2011 +0100
@@ -56,6 +56,7 @@
Baz x::name t::foo bind x in t
+
thm baz.distinct
thm baz.induct
thm baz.exhaust
@@ -78,7 +79,7 @@
| Fun "nat \<Rightarrow> nat"
| Var "name"
| Lam x::"name" t::"set_ty" bind x in t
-
+thm meta_eq_to_obj_eq
thm set_ty.distinct
thm set_ty.induct
thm set_ty.exhaust
--- a/Nominal/Ex/Lambda.thy Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Ex/Lambda.thy Thu Jun 16 20:07:03 2011 +0100
@@ -10,7 +10,8 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
-text {* free name function *}
+
+section {* free name function *}
text {* first returns an atom list *}
@@ -20,7 +21,8 @@
"frees_lst (Var x) = [atom x]"
| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
- unfolding eqvt_def frees_lst_graph_def
+ unfolding eqvt_def
+ unfolding frees_lst_graph_def
apply (rule, perm_simp, rule)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
@@ -74,7 +76,9 @@
by (metis fresh_fun_app)
-text {* A test with a locale and an interpretation. *}
+section {* A test with a locale and an interpretation. *}
+
+text {* conclusion: it is no necessary *}
locale test =
fixes f1::"name \<Rightarrow> ('a::pt)"
@@ -126,7 +130,7 @@
apply (simp_all add: eqvt_def permute_fun_def permute_pure)
done
-text {* height function *}
+section {* height function *}
nominal_primrec
height :: "lam \<Rightarrow> int"
@@ -149,7 +153,7 @@
thm height.simps
-text {* capture - avoiding substitution *}
+section {* capture-avoiding substitution *}
nominal_primrec
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90)
--- a/Nominal/Nominal2.thy Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Nominal2.thy Thu Jun 16 20:07:03 2011 +0100
@@ -261,43 +261,45 @@
val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
- val (alpha_eqvt, lthy6) =
- Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+ val alpha_eqvt =
+ Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+
+ val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
val _ = trace_msg (K "Proving equivalence of alpha...")
val alpha_refl_thms =
- raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6
+ raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5
val alpha_sym_thms =
- raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6
+ raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5
val alpha_trans_thms =
raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms)
- alpha_intros alpha_induct alpha_cases lthy6
+ alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5
val (alpha_equivp_thms, alpha_bn_equivp_thms) =
raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms
- alpha_trans_thms lthy6
+ alpha_trans_thms lthy5
val _ = trace_msg (K "Proving alpha implies bn...")
val alpha_bn_imp_thms =
- raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6
+ raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5
val _ = trace_msg (K "Proving respectfulness...")
val raw_funs_rsp_aux =
raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs
- raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
+ raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5
val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
val raw_size_rsp =
raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct
- (raw_size_thms @ raw_size_eqvt) lthy6
+ (raw_size_thms @ raw_size_eqvt) lthy5
|> map mk_funs_rsp
val raw_constrs_rsp =
raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
- (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6
+ (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5
val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
@@ -306,19 +308,19 @@
val raw_perm_bn_rsp =
raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct
- alpha_intros raw_perm_bn_simps lthy6
+ alpha_intros raw_perm_bn_simps lthy5
(* noting the quot_respects lemmas *)
- val (_, lthy6a) =
+ val (_, lthy6) =
Local_Theory.note ((Binding.empty, [rsp_attr]),
raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @
- alpha_bn_rsp @ raw_perm_bn_rsp) lthy6
+ alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
val _ = trace_msg (K "Defining the quotient types...")
val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
val (qty_infos, lthy7) =
- define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
+ define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
val qtys = map #qtyp qty_infos
val qty_full_names = map (fst o dest_Type) qtys
--- a/Nominal/Nominal2_Base.thy Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Nominal2_Base.thy Thu Jun 16 20:07:03 2011 +0100
@@ -1626,6 +1626,12 @@
definition
"eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
+lemma eqvt_boolI:
+ fixes f::"bool"
+ shows "eqvt f"
+unfolding eqvt_def by (simp add: permute_bool_def)
+
+
text {* equivariance of a function at a given argument *}
definition
--- a/Nominal/nominal_dt_alpha.ML Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/nominal_dt_alpha.ML Thu Jun 16 20:07:03 2011 +0100
@@ -26,8 +26,9 @@
(Proof.context -> int -> tactic) -> Proof.context -> thm list
val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
- val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
- val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
+ val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list
+ val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list ->
+ Proof.context -> thm list
val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list ->
Proof.context -> thm list * thm list
@@ -492,7 +493,7 @@
by (erule exE, rule_tac x="-p" in exI, auto)}
(* for premises that contain binders *)
-fun prem_bound_tac pred_names ctxt =
+fun prem_bound_tac pred_names alpha_eqvt ctxt =
let
fun trans_prem_tac pred_names ctxt =
SUBPROOF (fn {prems, context, ...} =>
@@ -507,20 +508,20 @@
[ etac exi_neg,
resolve_tac @{thms alpha_sym_eqvt},
asm_full_simp_tac (HOL_ss addsimps prod_simps),
- eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
- trans_prem_tac pred_names ctxt ]
+ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+ trans_prem_tac pred_names ctxt]
end
-fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
+fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt =
let
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
-
+
fun tac ctxt =
let
val alpha_names = map (fst o dest_Const) alpha_trms
in
resolve_tac alpha_intros THEN_ALL_NEW
- FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]
+ FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
end
in
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt
@@ -549,7 +550,7 @@
HEADGOAL (rtac exi_inst)
end)
-fun non_trivial_cases_tac pred_names intros ctxt =
+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 prod_rel_def}
in
@@ -562,15 +563,15 @@
resolve_tac @{thms alpha_trans_eqvt},
atac,
aatac pred_names ctxt,
- eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
+ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
end
-fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =
+fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt =
let
fun all_cases ctxt =
asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
- THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
+ THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt
in
EVERY' [ rtac @{thm allI}, rtac @{thm impI},
ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
@@ -585,13 +586,13 @@
HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
end
-fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
+fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt =
let
val alpha_names = map (fst o dest_Const) alpha_trms
val props = map prep_trans_goal alpha_trms
in
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
- (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
+ (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt
end
--- a/Nominal/nominal_eqvt.ML Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/nominal_eqvt.ML Thu Jun 16 20:07:03 2011 +0100
@@ -8,8 +8,7 @@
signature NOMINAL_EQVT =
sig
- val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
- val equivariance: string -> Proof.context -> (thm list * local_theory)
+ val raw_equivariance: term list -> thm -> thm list -> Proof.context -> thm list
val equivariance_cmd: string -> Proof.context -> local_theory
end
@@ -75,20 +74,10 @@
(* stores thm under name.eqvt and adds [eqvt]-attribute *)
-fun note_named_thm (name, thm) ctxt =
- let
- val thm_name = Binding.qualified_name
- (Long_Name.qualify (Long_Name.base_name name) "eqvt")
- val attr = Attrib.internal (K eqvt_add)
- val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
- in
- (thm', ctxt')
- end
-
fun get_name (Const (a, _)) = a
| get_name (Free (a, _)) = a
-fun raw_equivariance note_flag pred_trms raw_induct intrs ctxt =
+fun raw_equivariance pred_trms raw_induct intrs ctxt =
let
val is_already_eqvt =
filter (is_eqvt ctxt) pred_trms
@@ -110,36 +99,34 @@
(HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
val goal = HOLogic.mk_Trueprop
- (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds))
-
- val thms = Goal.prove ctxt' [] [] goal
+ (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds))
+ in
+ Goal.prove ctxt' [] [] goal
(fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1)
|> Datatype_Aux.split_conj_thm
|> ProofContext.export ctxt' ctxt
|> map (fn th => th RS mp)
|> map zero_var_indexes
- in
- if note_flag
- then fold_map note_named_thm (pred_names ~~ thms) ctxt
- else (thms, ctxt)
end
-fun equivariance pred_name ctxt =
+fun note_named_thm (name, thm) ctxt =
let
- val thy = ProofContext.theory_of ctxt
- val (_, {preds, raw_induct, intrs, ...}) =
- Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
+ val thm_name = Binding.qualified_name
+ (Long_Name.qualify (Long_Name.base_name name) "eqvt")
+ val attr = Attrib.internal (K eqvt_add)
+ val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
in
- raw_equivariance false preds raw_induct intrs ctxt
+ (thm', ctxt')
end
fun equivariance_cmd pred_name ctxt =
let
val thy = ProofContext.theory_of ctxt
- val (_, {preds, raw_induct, intrs, ...}) =
+ val ({names, ...}, {preds, raw_induct, intrs, ...}) =
Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
+ val thms = raw_equivariance preds raw_induct intrs ctxt
in
- raw_equivariance true preds raw_induct intrs ctxt |> snd
+ fold_map note_named_thm (names ~~ thms) ctxt |> snd
end
local structure P = Parse and K = Keyword in
--- a/Nominal/nominal_library.ML Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/nominal_library.ML Thu Jun 16 20:07:03 2011 +0100
@@ -479,8 +479,10 @@
(*
inductive premises can be of the form
- R ... /\ P ...; split_conj_i picks out
- the part R or P part
+
+ R ... /\ P ...;
+
+ split_conj_i picks out the part R or P part
*)
fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) =
(case head_of f1 of