# HG changeset patch # User Christian Urban # Date 1268823262 -3600 # Node ID 4d01ab140f237dbed06f15efd95d4f04e5843431 # Parent 1ea4ca823266448fbf691c334fd4134825c993ba# Parent 4ac3485899e182247e346fc211470e539af41bac merged diff -r 1ea4ca823266 -r 4d01ab140f23 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Wed Mar 17 11:53:56 2010 +0100 +++ b/Nominal/Rsp.thy Wed Mar 17 11:54:22 2010 +0100 @@ -186,7 +186,7 @@ (split_conjs THEN_ALL_NEW TRY o resolve_tac @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) + asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) *} ML {* diff -r 1ea4ca823266 -r 4d01ab140f23 Nominal/Term5.thy --- a/Nominal/Term5.thy Wed Mar 17 11:53:56 2010 +0100 +++ b/Nominal/Term5.thy Wed Mar 17 11:54:22 2010 +0100 @@ -50,7 +50,7 @@ (*lemma alpha5_eqvt: "(xa \5 y \ (p \ xa) \5 (p \ y)) \ (xb \l ya \ (p \ xb) \l (p \ ya)) \ - (alpha_rbv5 a b c \ alpha_rbv5 (p \ a) (p \ b) (p \ c))" + (alpha_rbv5 b c \ alpha_rbv5 (p \ b) (p \ c))" apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) done*) @@ -75,10 +75,21 @@ apply (simp_all add: alpha5_inj) apply (erule exE) apply (rule_tac x="- pi" in exI) +apply (simp add: alpha_gen) + apply(simp add: fresh_star_def fresh_minus_perm) apply clarify apply (rule conjI) -apply (erule_tac [!] alpha_gen_compose_sym) -apply (simp_all add: alpha5_eqvt) +apply (rotate_tac 3) +apply (frule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (rule conjI) +apply (rotate_tac 5) +apply (frule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 6) +apply simp +apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) +apply (simp) done lemma alpha5_transp: @@ -94,19 +105,29 @@ apply (simp_all add: alpha5_inj) apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) apply (simp_all add: alpha5_inj) -apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) -apply clarify -apply (rule conjI) -apply (erule alpha_gen_compose_trans) -apply (assumption) -apply (simp add: alpha5_eqvt) -apply (erule alpha_gen_compose_trans) -apply (assumption) -apply (simp add: alpha5_eqvt) +defer apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) apply (simp_all add: alpha5_inj) apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) apply (simp_all add: alpha5_inj) +apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) +apply (simp add: alpha_gen) +apply clarify +apply(simp add: fresh_star_plus) +apply (rule conjI) +apply (erule_tac x="- pi \ rltsaa" in allE) +apply (rotate_tac 5) +apply (drule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (drule_tac p="pi" in alpha5_eqvt(2)) +apply simp +apply (erule_tac x="- pi \ rtrm5aa" in allE) +apply (rotate_tac 7) +apply (drule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 3) +apply (drule_tac p="pi" in alpha5_eqvt(1)) +apply simp done lemma alpha5_equivp: @@ -146,7 +167,7 @@ apply(simp_all add: eqvts) apply(simp add: alpha_gen) apply(clarify) - apply(simp) + apply blast done lemma bv_list_rsp: @@ -234,20 +255,25 @@ lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] lemmas bv5[simp] = rbv5.simps[quot_lifted] lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] -lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] +lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] lemmas alpha5_DIS = alpha_dis[quot_lifted] +(* why is this not in Isabelle? *) +lemma set_sub: "{a, b} - {b} = {a} - {b}" +by auto + lemma lets_bla: "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" -apply (simp only: alpha5_INJ) -apply (simp only: bv5) +apply (simp only: alpha5_INJ bv5) apply simp apply (rule allI) apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) apply (rule impI) apply (rule impI) -sorry (* The assumption is false, so it is true *) +apply (rule impI) +apply (simp add: set_sub) +done lemma lets_ok: "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" @@ -256,6 +282,7 @@ apply (rule_tac x="(x \ y)" in exI) apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) +apply (simp add: eqvts) done lemma lets_ok3: diff -r 1ea4ca823266 -r 4d01ab140f23 Nominal/Term5a.thy --- a/Nominal/Term5a.thy Wed Mar 17 11:53:56 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -theory Term5 -imports "Parser" -begin - -atom_decl name - -ML {* restricted_nominal := 2 *} - -nominal_datatype trm5 = - Vr5 "name" -| Ap5 "trm5" "trm5" -| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t -and lts = - Lnil -| Lcons "name" "trm5" "lts" -binder - bv5 -where - "bv5 Lnil = {}" -| "bv5 (Lcons n t ltl) = {atom n} \ (bv5 ltl)" - -lemma lets_ok: - "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -apply (simp add: trm5_lts_inject) -apply (rule_tac x="(x \ y)" in exI) -apply (simp_all add: alpha_gen) -apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn) -done - -lemma lets_nok: - "x \ y \ (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \ (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))" -apply (simp only: trm5_lts_inject not_ex) -apply (rule allI) -apply (simp add: alpha_gen) -apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject) -done - -end diff -r 1ea4ca823266 -r 4d01ab140f23 Nominal/Term5n.thy --- a/Nominal/Term5n.thy Wed Mar 17 11:53:56 2010 +0100 +++ b/Nominal/Term5n.thy Wed Mar 17 11:54:22 2010 +0100 @@ -53,10 +53,34 @@ build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} print_theorems +lemma alpha5_reflp: +"y \5 y \ (x \l x \ alpha_rbv5 x x)" +apply (rule rtrm5_rlts.induct) +apply (simp_all add: alpha5_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) +done + +lemma alpha5_symp: +"(a \5 b \ b \5 a) \ +(x \l y \ y \l x) \ +(alpha_rbv5 x y \ alpha_rbv5 y x)" +sorry + +lemma alpha5_transp: +"(a \5 b \ (\c. b \5 c \ a \5 c)) \ +(x \l y \ (\z. y \l z \ x \l z)) \ +(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" +sorry + lemma alpha5_equivp: "equivp alpha_rtrm5" "equivp alpha_rlts" - sorry + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def + apply (simp_all only: alpha5_reflp) + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done quotient_type trm5 = rtrm5 / alpha_rtrm5 @@ -96,14 +120,34 @@ apply simp done -lemma alpha_rbv5_rsp: "xa \l y \ xb \l ya \ alpha_rbv5 xa xb = alpha_rbv5 y ya" +local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} +print_theorems + +lemma alpha_rbv_rsp_pre: + "x \l y \ \z. alpha_rbv5 x z = alpha_rbv5 y z" apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all) - defer defer (* should follow from distinctness *) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply (case_tac [!] z) + apply (simp_all add: alpha_dis alpha5_inj) apply clarify - apply (simp add: alpha5_inj) - sorry (* should be true? *) + apply auto + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done + +lemma alpha_rbv_rsp_pre2: + "x \l y \ \z. alpha_rbv5 z x = alpha_rbv5 z y" + apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply (case_tac [!] z) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply auto + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done lemma [quot_respect]: "(alpha_rlts ===> op =) fv_rlts fv_rlts" @@ -117,12 +161,8 @@ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv5_rsp) + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp) apply (clarify) - apply (rule conjI) - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha5_inj) - apply clarify apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) done @@ -168,7 +208,7 @@ apply (simp add: alpha5_INJ) apply (rule_tac x="(x \ y)" in exI) apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) +apply (simp add: permute_trm5_lts fresh_star_def eqvts) done lemma lets_ok3: @@ -185,6 +225,7 @@ apply (simp add: alpha5_INJ alpha_gen) apply (rule_tac x="0::perm" in exI) apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) +apply blast done lemma distinct_helper: diff -r 1ea4ca823266 -r 4d01ab140f23 Nominal/TySch.thy --- a/Nominal/TySch.thy Wed Mar 17 11:53:56 2010 +0100 +++ b/Nominal/TySch.thy Wed Mar 17 11:54:22 2010 +0100 @@ -1,99 +1,123 @@ theory TySch -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +imports "Parser" "../Attic/Prove" begin atom_decl name -text {* type schemes *} -datatype ty = - Var "name" -| Fun "ty" "ty" +ML {* val _ = cheat_fv_rsp := false *} +ML {* val _ = cheat_const_rsp := false *} +ML {* val _ = cheat_equivp := false *} +ML {* val _ = cheat_fv_eqvt := false *} +ML {* val _ = cheat_alpha_eqvt := false *} +ML {* val _ = recursive := false *} -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} -print_theorems - -datatype tyS = - All "name set" "ty" +nominal_datatype t = + Var "name" +| Fun "t" "t" +and tyS = + All xs::"name set" ty::"t" bind xs in ty -lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s" -apply (simp add: supp_def) -apply (simp add: eqvts eqvts_raw) -(* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*) -sorry +thm t_tyS_fv +thm t_tyS_inject +thm t_tyS_bn +thm t_tyS_perm +thm t_tyS_induct +thm t_tyS_distinct -lemma atom_image_swap_fresh: "\a \ atom ` (fn :: ('a :: at) set); b \ atom ` fn\ \ (a \ b) \ fn = fn" -apply (simp add: fresh_def) -apply (simp add: support_image) -apply (fold fresh_def) -apply (simp add: swap_fresh_fresh) -done - -lemma "\a \ atom ` fun; a \ t; b \ atom ` fun; b \ t\ \ All ((a \ b) \ fun) t = All fun t" -apply (simp add: atom_image_swap_fresh) +lemma supports: + "(supp (atom i)) supports (Var i)" + "(supp A \ supp M) supports (Fun A M)" +apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm) +apply clarify +apply(simp_all add: fresh_atom) done -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} -print_theorems +lemma fs: + "finite (supp (x\t)) \ finite (supp (z\tyS))" +apply(induct rule: t_tyS_induct) +apply(rule supports_finite) +apply(rule supports) +apply(simp add: supp_atom) +apply(rule supports_finite) +apply(rule supports) +apply(simp add: supp_atom) +sorry -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") - [[[[]], [[], []]]] *} -print_theorems +instance t and tyS :: fs +apply default +apply (simp_all add: fs) +sorry + +(* Should be moved to a proper place *) +lemma infinite_Un: + shows "infinite (S \ T) \ infinite S \ infinite T" + by simp -(* -Doesnot work yet since we do not refer to fv_ty -local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *} -print_theorems -*) - -primrec - fv_tyS -where - "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" - -inductive - alpha_tyS :: "tyS \ tyS \ bool" ("_ \tyS _" [100, 100] 100) -where - a1: "\pi. ((atom ` xs1, T1) \gen (op =) fv_ty pi (atom ` xs2, T2)) - \ All xs1 T1 \tyS All xs2 T2" +lemma supp_fv_t_tyS: + 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) +(* VarTS case *) +apply(simp only: supp_def) +apply(simp only: t_tyS_perm) +apply(simp only: t_tyS_inject) +apply(simp only: supp_def[symmetric]) +apply(simp only: supp_at_base) +(* FunTS case *) +apply(simp only: supp_def) +apply(simp only: t_tyS_perm) +apply(simp only: t_tyS_inject) +apply(simp only: de_Morgan_conj) +apply(simp only: Collect_disj_eq) +apply(simp only: infinite_Un) +apply(simp only: Collect_disj_eq) +(* All case *) +apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst) +apply(simp (no_asm) only: supp_def) +apply(simp only: t_tyS_perm) +apply(simp only: permute_ABS) +apply(simp only: t_tyS_inject) +apply(simp only: Abs_eq_iff) +apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) +apply(simp only: alpha_gen) +apply(simp only: supp_eqvt[symmetric]) +apply(simp only: eqvts) +apply(simp only: supp_Abs) +done lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {b, a} (Fun (Var a) (Var b))" - apply(rule a1) + shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" + apply(simp add: t_tyS_inject) + apply(rule_tac x="0::perm" in exI) apply(simp add: alpha_gen) - apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) + apply(auto) + apply(simp add: fresh_star_def fresh_zero_perm) done lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var b) (Var a))" - apply(rule a1) - apply(simp add: alpha_gen) + shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" + apply(simp add: t_tyS_inject) apply(rule_tac x="(atom a \ atom b)" in exI) - apply(simp add: fresh_star_def) + apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts) + apply auto done lemma - shows "All {a, b, c} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var a) (Var b))" - apply(rule a1) - apply(simp add: alpha_gen) + shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" + apply(simp add: t_tyS_inject) apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) - done + apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) +oops lemma assumes a: "a \ b" - shows "\(All {a, b} (Fun (Var a) (Var b)) \tyS All {c} (Fun (Var c) (Var c)))" + shows "\(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" using a + apply(simp add: t_tyS_inject) apply(clarify) - apply(erule alpha_tyS.cases) - apply(simp add: alpha_gen) - apply(erule conjE)+ - apply(erule exE) - apply(erule conjE)+ - apply(clarify) - apply(simp) - apply(simp add: fresh_star_def) - apply(auto) + apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) + apply auto done