adapted to changes by Florian on the quotient package and removed local fix for function package
--- a/Nominal-General/nominal_library.ML Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal-General/nominal_library.ML Wed Nov 10 13:46:21 2010 +0000
@@ -256,46 +256,24 @@
end
-(** FIX: my_relation is necessary because of problem in Function Package *)
-
-fun inst_state_tac ctxt rel st =
- let
- val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
- val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
- val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
- in case Term.add_vars (prop_of st') [] of
- [v] =>
- PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
- | _ => Seq.empty
- end
-
-fun my_relation_tac ctxt rel i =
- TRY (Function_Common.apply_termination_rule ctxt i)
- THEN inst_state_tac ctxt rel
-
-(** FIX: end *)
-
-
-fun prove_termination_tac size_simps ctxt i st =
+fun prove_termination_tac size_simps ctxt =
let
fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
| mk_size_measure T = size_const T
- val ((_ $ (_ $ rel)) :: _) = prems_of st
- val measure_trm =
- fastype_of rel
- |> HOLogic.dest_setT
+ fun mk_measure_trm T =
+ HOLogic.dest_setT T
+ |> fst o HOLogic.dest_prodT
|> mk_size_measure
|> curry (op $) (Const (@{const_name measure}, dummyT))
|> Syntax.check_term ctxt
+
val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral
zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
-
in
- (*see above Function_Relation.relation_tac ctxt measure_trm*)
- (my_relation_tac ctxt measure_trm
- THEN_ALL_NEW simp_tac ss) i st
+ Function_Relation.relation_tac ctxt mk_measure_trm
+ THEN_ALL_NEW simp_tac ss
end
fun prove_termination size_simps ctxt =
--- a/Nominal/Abs.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Abs.thy Wed Nov 10 13:46:21 2010 +0000
@@ -546,6 +546,8 @@
lemma [quot_respect]:
shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+ unfolding fun_rel_def
+ unfolding prod_rel_def
by auto
lemma [quot_preserve]:
@@ -562,7 +564,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 prod_rel.simps
+ unfolding prod_rel_def
by (perm_simp) (rule refl)
lemma [eqvt]:
--- a/Nominal/Ex/Datatypes.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy Wed Nov 10 13:46:21 2010 +0000
@@ -1,3 +1,4 @@
+
theory Datatypes
imports "../Nominal2"
begin
--- a/Nominal/Ex/Foo1.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Foo1.thy Wed Nov 10 13:46:21 2010 +0000
@@ -74,7 +74,7 @@
lemma [quot_respect]:
shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
- apply simp
+ apply (simp add: fun_rel_def)
apply clarify
apply (erule alpha_assg_raw.cases)
apply simp_all
@@ -84,7 +84,7 @@
lemma [quot_respect]:
shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
- apply simp
+ apply (simp add: fun_rel_def)
apply clarify
apply (erule alpha_assg_raw.cases)
apply simp_all
@@ -94,7 +94,7 @@
lemma [quot_respect]:
shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
- apply simp
+ apply (simp add: fun_rel_def)
apply clarify
apply (erule alpha_assg_raw.cases)
apply simp_all
--- a/Nominal/Ex/Lambda.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Lambda.thy Wed Nov 10 13:46:21 2010 +0000
@@ -462,7 +462,7 @@
lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"
apply rule
- apply (induct_tac a b rule: alpha_lam_raw.induct)
+ apply (induct_tac x y rule: alpha_lam_raw.induct)
apply simp_all
done
--- a/Nominal/Ex/Let.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Let.thy Wed Nov 10 13:46:21 2010 +0000
@@ -42,7 +42,7 @@
"permute_bn_raw"
lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
- apply simp
+ apply (simp add: fun_rel_def)
apply clarify
apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
apply (rule TrueI)+
--- a/Nominal/Ex/SingleLet.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy Wed Nov 10 13:46:21 2010 +0000
@@ -48,7 +48,7 @@
lemma [quot_respect]:
shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
- apply simp
+ apply (simp add: fun_rel_def)
apply clarify
apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
apply (rule TrueI)+
--- a/Nominal/Nominal2.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Nominal2.thy Wed Nov 10 13:46:21 2010 +0000
@@ -514,7 +514,7 @@
(* lifting of the theorems *)
val _ = warning "Lifting of Theorems"
- val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+ val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
prod.cases}
val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) =
--- a/Nominal/Nominal2_FSet.thy Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Nominal2_FSet.thy Wed Nov 10 13:46:21 2010 +0000
@@ -6,6 +6,7 @@
lemma permute_fset_rsp[quot_respect]:
shows "(op = ===> list_eq ===> list_eq) permute permute"
+ unfolding fun_rel_def
by (simp add: set_eqvt[symmetric])
instantiation fset :: (pt) pt
--- a/Nominal/nominal_dt_alpha.ML Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML Wed Nov 10 13:46:21 2010 +0000
@@ -445,7 +445,7 @@
fun cases_tac intros ctxt =
let
- val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
+ val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def}
val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
@@ -493,7 +493,7 @@
in
resolve_tac prems' 1
end) ctxt
- val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
+ val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas}
in
EVERY'
[ etac exi_neg,
@@ -543,7 +543,7 @@
fun non_trivial_cases_tac pred_names intros ctxt =
let
- val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
+ val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}
in
resolve_tac intros
THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN'
@@ -596,8 +596,8 @@
fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt =
let
- val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
- val symm' = map (fold_rule @{thms symp_def} o atomize) symm
+ val refl' = map (fold_rule @{thms reflp_def[THEN eq_reflection]} o atomize) refl
+ val symm' = map (fold_rule @{thms symp_def[THEN eq_reflection]} o atomize) symm
val trans' = map (fold_rule [transp_def'] o atomize) trans
fun prep_goal t =
@@ -671,7 +671,7 @@
val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys
- val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps
+ val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def
permute_prod_def prod.cases prod.recs})
val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
@@ -685,7 +685,7 @@
fun raw_constr_rsp_tac alpha_intros simps =
let
val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
- val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps
+ val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def
prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
in
asm_full_simp_tac pre_ss
@@ -754,7 +754,7 @@
(* transformation of the natural rsp-lemmas into standard form *)
val fun_rsp = @{lemma
- "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}
+ "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}
fun mk_funs_rsp thm =
thm
@@ -765,7 +765,7 @@
val permute_rsp = @{lemma
"(!x y p. R x y --> R (permute p x) (permute p y))
- ==> ((op =) ===> R ===> R) permute permute" by simp}
+ ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)}
fun mk_alpha_permute_rsp thm =
thm
--- a/Nominal/nominal_dt_supp.ML Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML Wed Nov 10 13:46:21 2010 +0000
@@ -144,7 +144,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 prod_rel.simps permute_prod_def
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def
prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
fun p_tac msg i =