# HG changeset patch # User Christian Urban # Date 1306352330 -7200 # Node ID 1a6593bc494de663c4dd9d72f204896a41180fa4 # Parent bccda961a61253372b074dcdf8e40f3d36512bc8 added eq_iff and distinct lemmas of nominal datatypes to the simplifier diff -r bccda961a612 -r 1a6593bc494d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue May 24 19:39:38 2011 +0200 +++ b/Nominal/Ex/Lambda.thy Wed May 25 21:38:50 2011 +0200 @@ -10,15 +10,17 @@ | eVar nat inductive - eval :: "expr \ nat \ bool" + eval :: "expr \ nat list \ bool" where - evCnst: "eval (eCnst c) 0" -| evVar: "eval (eVar n) 2" + evCnst1: "eval (eCnst c) [2,1]" +| evCnst2: "eval (eCnst b) [1,2]" +| evVar: "eval (eVar n) [1]" inductive_cases - evInv_Cnst: "eval (eCnst c) m" + evInv_Cnst: "eval (eCnst c) [1,2]" -thm evInv_Cnst[simplified expr.distinct expr.eq_iff] +thm evInv_Cnst + atom_decl name @@ -143,7 +145,8 @@ defer apply(rule_tac y="x" in lam.exhaust) apply(simp_all)[3] -apply(simp_all add: lam.distinct lam.eq_iff) +apply(auto)[1] +apply(simp_all) apply (erule Abs1_eq_fdest) apply(simp add: supp_removeAll fresh_def) apply(drule supp_eqvt_at) diff -r bccda961a612 -r 1a6593bc494d Nominal/Ex/Multi_Recs2.thy --- a/Nominal/Ex/Multi_Recs2.thy Tue May 24 19:39:38 2011 +0200 +++ b/Nominal/Ex/Multi_Recs2.thy Wed May 25 21:38:50 2011 +0200 @@ -83,9 +83,6 @@ thm fun_recs.fsupp thm fun_recs.supp - - - lemma fixes c::"'a::fs" assumes "\name c. P1 c (Var name)" @@ -106,16 +103,21 @@ apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1)) apply(simp_all)[4] + apply(blast) apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2)) - apply(simp_all)[1] + apply(blast) apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3)) - apply(simp_all)[2] + apply(blast) + apply(blast) apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4)) - apply(simp_all)[1] + apply(blast) apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5)) - apply(simp_all)[2] + apply(blast) + apply(blast) apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6)) - apply(simp_all)[3] + apply(blast) + apply(blast) + apply(blast) apply(tactic {* prove_termination_ind @{context} 1 *}) apply(simp_all add: fun_recs.size) done diff -r bccda961a612 -r 1a6593bc494d Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue May 24 19:39:38 2011 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Wed May 25 21:38:50 2011 +0200 @@ -184,15 +184,14 @@ apply (case_tac x) apply simp apply clarify apply (rule_tac y="b" in ty_tys.exhaust(1)) -apply (auto simp add: ty_tys.eq_iff)[1] -apply (auto simp add: ty_tys.eq_iff)[1] -apply blast +apply (auto)[1] +apply (auto)[1] apply simp apply clarify apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) -apply (auto simp add: ty_tys.eq_iff)[1] -apply (auto simp add: ty_tys.distinct) -apply (auto simp add: ty_tys.eq_iff ty_tys.distinct)[2] +apply (auto)[1] +apply (auto)[5] --"LAST GOAL" +apply(simp del: ty_tys.eq_iff) thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff] apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) apply (subgoal_tac "eqvt_at (\(l, r). subst l r) (\', T)") @@ -230,7 +229,6 @@ apply clarify --"This is exactly the assumption for the properly defined function" defer -apply (simp add: ty_tys.eq_iff) apply (simp only: Abs_eq_res_set) apply (subgoal_tac "(atom ` fset xsa \ supp Ta - atom ` fset xs \ supp T) \* ([atom ` fset xs \ supp (subst \' T)]set. T)") apply (subst (asm) Abs_eq_iff2) @@ -361,8 +359,6 @@ apply(blast) apply(blast) apply(simp_all add: ty2.distinct) -apply(simp add: ty2.eq_iff) -apply(simp add: ty2.eq_iff) apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ r)") apply(simp add: eqvt_def) apply(rule allI) diff -r bccda961a612 -r 1a6593bc494d Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue May 24 19:39:38 2011 +0200 +++ b/Nominal/Nominal2.thy Wed May 25 21:38:50 2011 +0200 @@ -43,6 +43,7 @@ val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) val simp_attr = Attrib.internal (K Simplifier.simp_add) +val induct_attr = Attrib.internal (K Induct.induct_simp_add) *} section{* Interface for nominal_datatype *} @@ -455,8 +456,8 @@ val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) val (_, lthy9') = lthyC - |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) - ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs') + |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) + ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)