# HG changeset patch # User Cezary Kaliszyk # Date 1268910599 -3600 # Node ID be911e869fded335c11a11a96ce8fce5dd0a8005 # Parent a9cb6a51efc37fcb2c480640253cae20055d2370 Added fv,bn,distinct,perm to the simplifier. diff -r a9cb6a51efc3 -r be911e869fde Nominal/Fv.thy --- a/Nominal/Fv.thy Thu Mar 18 11:37:10 2010 +0100 +++ b/Nominal/Fv.thy Thu Mar 18 12:09:59 2010 +0100 @@ -33,7 +33,7 @@ *) (* -The overview of the generation of free variables: +An overview of the generation of free variables: 1) fv_bn functions are generated only for the non-recursive binds. @@ -76,6 +76,10 @@ - for nominal datatype ty' return: fv_ty' x *) +(* +An overview of the generation of alpha-equivalence: +*) + ML {* fun is_atom thy typ = Sign.of_sort thy (typ, @{sort at}) diff -r a9cb6a51efc3 -r be911e869fde Nominal/LFex.thy --- a/Nominal/LFex.thy Thu Mar 18 11:37:10 2010 +0100 +++ b/Nominal/LFex.thy Thu Mar 18 12:09:59 2010 +0100 @@ -45,7 +45,7 @@ "supp (Var x) = {atom x}" "supp (App M N) = supp M \ supp N" "supp trm = fv_trm trm \ supp (Lam ty name trm) = supp ty \ supp (Abs {atom name} trm)" - apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm) + apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt) apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen) apply(simp_all only: ex_out) apply(simp_all only: eqvts[symmetric]) @@ -58,7 +58,7 @@ lemma supp_fv: "supp t1 = fv_kind t1 \ supp t2 = fv_ty t2 \ supp t3 = fv_trm t3" apply(induct rule: kind_ty_trm_induct) - apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv) + apply(simp_all (no_asm) only: supp_eqs) apply(simp_all) apply(simp_all add: supp_eqs) apply(simp_all add: supp_Abs) @@ -74,7 +74,7 @@ "supp (Var x) = {atom x}" "supp (App M N) = supp M \ supp N" "supp (Lam A x M) = supp A \ (supp M - {atom x})" -apply (simp_all add: supp_fv kind_ty_trm_fv) +apply (simp_all add: supp_fv) end diff -r a9cb6a51efc3 -r be911e869fde Nominal/Parser.thy --- a/Nominal/Parser.thy Thu Mar 18 11:37:10 2010 +0100 +++ b/Nominal/Parser.thy Thu Mar 18 12:09:59 2010 +0100 @@ -381,15 +381,18 @@ val q_name = space_implode "_" qty_names; val _ = tracing "Lifting induction"; val q_induct = lift_thm lthy13 induct; + fun note_simp_suffix s th ctxt = + snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s), + [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; - val q_perm = map (lift_thm lthy14) raw_perm_def; - val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; + val q_perm = map (lift_thm lthy14) raw_perm_def; + val lthy15 = note_simp_suffix "perm" q_perm lthy14a; val q_fv = map (lift_thm lthy15) fv_def; - val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; + val lthy16 = note_simp_suffix "fv" q_fv lthy15; val q_bn = map (lift_thm lthy16) raw_bn_eqs; - val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; + val lthy17 = note_simp_suffix "bn" q_bn lthy16; val _ = tracing "Lifting eq-iff"; val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 @@ -400,7 +403,7 @@ val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) val q_dis = map (lift_thm lthy18) rel_dists; - val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; + val lthy19 = note_simp_suffix "distinct" q_dis lthy18; val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; diff -r a9cb6a51efc3 -r be911e869fde Nominal/Test.thy --- a/Nominal/Test.thy Thu Mar 18 11:37:10 2010 +0100 +++ b/Nominal/Test.thy Thu Mar 18 12:09:59 2010 +0100 @@ -23,13 +23,13 @@ lemma finite_fv: shows "finite (fv_lm t)" apply(induct t rule: lm_induct) -apply(simp_all add: lm_fv) +apply(simp_all) done lemma supp_fn: shows "supp t = fv_lm t" apply(induct t rule: lm_induct) -apply(simp_all add: lm_fv) +apply(simp_all) apply(simp only: supp_def) apply(simp only: lm_perm) apply(simp only: lm_eq_iff) @@ -77,7 +77,7 @@ apply(erule exE) apply(rule_tac t="p \ Lm name lm" and s="(((p \ name) \ new) + p) \ Lm name lm" in subst) - apply(simp) + apply(simp del: lm_perm) apply(subst lm_perm) apply(subst (2) lm_perm) apply(rule flip_fresh_fresh) @@ -85,7 +85,7 @@ apply(simp only: supp_fn') apply(simp) apply(simp add: fresh_Pair) - apply(simp add: lm_perm) + apply(simp) apply(rule a3) apply(drule_tac x="((p \ name) \ new) + p" in meta_spec) apply(simp) @@ -130,7 +130,7 @@ shows "supp t = fv_lam t" and "supp bp = fv_bp bp \ fv_bi bp = {a. infinite {b. \alpha_bi ((a \ b) \ bp) bp}}" apply(induct t and bp rule: lam_bp_inducts) -apply(simp_all add: lam_bp_fv) +apply(simp_all) (* VAR case *) apply(simp only: supp_def) apply(simp only: lam_bp_perm) @@ -218,7 +218,7 @@ shows "supp t = fv_lam' t" and "supp bp = fv_bp' bp" apply(induct t and bp rule: lam'_bp'_inducts) -apply(simp_all add: lam'_bp'_fv) +apply(simp_all) (* VAR case *) apply(simp only: supp_def) apply(simp only: lam'_bp'_perm) @@ -304,7 +304,7 @@ shows "supp t = fv_trm' t" and "supp bp = fv_pat' bp \ {a. infinite {b. \alpha_f ((a \ b) \ bp) bp}} = fv_f bp" apply(induct t and bp rule: trm'_pat'_inducts) -apply(simp_all add: trm'_pat'_fv) +apply(simp_all) (* VAR case *) apply(simp only: supp_def) apply(simp only: trm'_pat'_perm) @@ -439,7 +439,7 @@ shows "supp T = fv_t T" and "supp S = fv_tyS S" apply(induct T and S rule: t_tyS_inducts) -apply(simp_all add: t_tyS_fv) +apply(simp_all) (* VarTS case *) apply(simp only: supp_def) apply(simp only: t_tyS_perm) @@ -519,11 +519,6 @@ thm trm3_rassigns3_induct thm trm3_rassigns3_distinct -(* compat should be -compat (ANil) pi (PNil) \ TRue -compat (ACons x t ts) pi (ACons x' t' ts') \ pi o x = x' \ alpha t t' \ compat ts pi ts' -*) - (* example 5 from Terms.thy *) nominal_datatype trm5 = diff -r a9cb6a51efc3 -r be911e869fde Nominal/TySch.thy --- a/Nominal/TySch.thy Thu Mar 18 11:37:10 2010 +0100 +++ b/Nominal/TySch.thy Thu Mar 18 12:09:59 2010 +0100 @@ -36,7 +36,7 @@ shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" apply(simp add: t_tyS_eq_iff) apply(rule_tac x="(atom a \ atom b)" in exI) - apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts) + apply(simp add: alpha_gen fresh_star_def eqvts) apply auto done @@ -44,7 +44,7 @@ shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" apply(simp add: t_tyS_eq_iff) apply(rule_tac x="0::perm" in exI) - apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff) + apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff) oops lemma @@ -53,7 +53,7 @@ using a apply(simp add: t_tyS_eq_iff) apply(clarify) - apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff) + apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff) apply auto done diff -r a9cb6a51efc3 -r be911e869fde TODO --- a/TODO Thu Mar 18 11:37:10 2010 +0100 +++ b/TODO Thu Mar 18 12:09:59 2010 +0100 @@ -3,13 +3,9 @@ - case names for "weak" induction rules (names of the constructors); see page 61/62 and 170 in Tutorial -- _perm rules should be added to the simplifier; - maybe _perm whould be called permute_.simps; +- maybe _perm whould be called permute_.simps; that would conform with the terminology in Nominal2 -- _fv / _bn / _distinct should also be - added to the simplifier - Bigger things: