nominal2: comparison Nominal/Test.thy

equal deleted inserted replaced

-:219e3ff68de8
+:fd483d8f486b
 shows "supp t = fv_lm t"
 apply(induct t rule: lm_induct)
 apply(simp_all add: lm_fv)
 apply(simp only: supp_def)
 apply(simp only: lm_perm)
-apply(simp only: lm_inject)
+apply(simp only: lm_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lm_perm)
-apply(simp only: lm_inject)
+apply(simp only: lm_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lm_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lm_inject)
+apply(simp only: lm_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 bi::"bp \<Rightarrow> atom set"
 where
 "bi (BP x t) = {atom x}"
 thm lam_bp_fv
-thm lam_bp_inject
+thm lam_bp_eq_iff
 thm lam_bp_bn
 thm lam_bp_perm
 thm lam_bp_induct
 thm lam_bp_inducts
 thm lam_bp_distinct
 apply(induct t and bp rule: lam_bp_inducts)
 apply(simp_all add: lam_bp_fv)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
 apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 (* LET case *)
 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp add: supp_Abs)
 apply(blast)
 (* BP case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 bi'::"bp' \<Rightarrow> atom set"
 where
 "bi' (BP' x t) = {atom x}"
 thm lam'_bp'_fv
-thm lam'_bp'_inject[no_vars]
+thm lam'_bp'_eq_iff[no_vars]
 thm lam'_bp'_bn
 thm lam'_bp'_perm
 thm lam'_bp'_induct
 thm lam'_bp'_inducts
 thm lam'_bp'_distinct
 apply(induct t and bp rule: lam'_bp'_inducts)
 apply(simp_all add: lam'_bp'_fv)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
 apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and
 s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen)
 apply(simp only: eqvts split_def fst_conv snd_conv)
 apply(simp only: eqvts[symmetric] supp_Pair)
 apply(simp only: eqvts Pair_eq)
 apply(simp add: supp_Abs supp_Pair)
 apply blast
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 "f PN = {}"
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
 thm trm'_pat'_fv
-thm trm'_pat'_inject
+thm trm'_pat'_eq_iff
 thm trm'_pat'_bn
 thm trm'_pat'_perm
 thm trm'_pat'_induct
 thm trm'_pat'_distinct
 apply(induct t and bp rule: trm'_pat'_inducts)
 apply(simp_all add: trm'_pat'_fv)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
 apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)"
 and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp add: supp_Abs)
 apply(blast)
 (* PN case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp)
 (* PS case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp)
 (* PD case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 "f0 PN0 = {}"
 | "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 thm trm0_pat0_fv
-thm trm0_pat0_inject
+thm trm0_pat0_eq_iff
 thm trm0_pat0_bn
 thm trm0_pat0_perm
 thm trm0_pat0_induct
 thm trm0_pat0_distinct
 | FunTS "t" "t"
 and  tyS =
 All xs::"name set" ty::"t" bind xs in ty
 thm t_tyS_fv
-thm t_tyS_inject
+thm t_tyS_eq_iff
 thm t_tyS_bn
 thm t_tyS_perm
 thm t_tyS_induct
 thm t_tyS_distinct
 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: t_tyS_eq_iff)
 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: t_tyS_eq_iff)
 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: t_tyS_eq_iff)
 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)
 "bv1 (BUnit1) = {}"
 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
 thm trm1_bp1_fv
-thm trm1_bp1_inject
+thm trm1_bp1_eq_iff
 thm trm1_bp1_bn
 thm trm1_bp1_perm
 thm trm1_bp1_induct
 thm trm1_bp1_distinct
 where
 "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 thm trm3_rassigns3_fv
-thm trm3_rassigns3_inject
+thm trm3_rassigns3_eq_iff
 thm trm3_rassigns3_bn
 thm trm3_rassigns3_perm
 thm trm3_rassigns3_induct
 thm trm3_rassigns3_distinct
 where
 "bv5 Lnil = {}"
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 thm trm5_lts_fv
-thm trm5_lts_inject
+thm trm5_lts_eq_iff
 thm trm5_lts_bn
 thm trm5_lts_perm
 thm trm5_lts_induct
 thm trm5_lts_distinct
 |  AndL2 n::"name" t::"phd" "name"                              bind n in t
 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
 thm phd_fv
-thm phd_inject
+thm phd_eq_iff
 thm phd_bn
 thm phd_perm
 thm phd_induct
 thm phd_distinct
 | "Cbinders (Type2 t T) = {atom t}"
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_eq_iff
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
 "bp'' (PVar x) = {atom x}"
 | "bp'' (PUnit) = {}"
 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
 thm exp_pat3_fv
-thm exp_pat3_inject
+thm exp_pat3_eq_iff
 thm exp_pat3_bn
 thm exp_pat3_perm
 thm exp_pat3_induct
 thm exp_pat3_distinct
 "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 thm exp6_pat6_fv
-thm exp6_pat6_inject
+thm exp6_pat6_eq_iff
 thm exp6_pat6_bn
 thm exp6_pat6_perm
 thm exp6_pat6_induct
 thm exp6_pat6_distinct

changeset 1496	fd483d8f486b
parent 1486	f86710d35146
child 1498	2ff84b1f551f