# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268894624 -3600
# Node ID fd483d8f486bc233a178ffd6d9c55e0241698d77
# Parent  219e3ff68de8c489ede6a7bdad212d4f5a55e9fe
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.

diff -r 219e3ff68de8 -r fd483d8f486b Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -46,7 +46,7 @@
   "supp (App M N) = supp M \<union> supp N"
   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
-  apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen)
+  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])
   apply(simp_all only: Collect_neg_conj)
diff -r 219e3ff68de8 -r fd483d8f486b Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -329,8 +329,7 @@
   val alpha_cases_loc = #elims alpha
   val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
-  val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4
-  val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
+  val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
@@ -344,13 +343,13 @@
   val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6a 1
+    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
   val _ = tracing "Proving equivalence";
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
     else build_equivps alpha_ts induct alpha_induct
-      inject alpha_inj distincts alpha_cases alpha_eqvt lthy6a;
+      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
@@ -377,7 +376,7 @@
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-    else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1
+    else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
@@ -403,13 +402,13 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_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 _ = tracing "Lifting pseudo-injectivity";
-  val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
-  val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
-  val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
-  val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1
-  val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2
-  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
+  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
+  val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
+  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
+  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17;
   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;
diff -r 219e3ff68de8 -r fd483d8f486b Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -32,12 +32,12 @@
 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)
@@ -47,7 +47,7 @@
 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)
@@ -116,7 +116,7 @@
   "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
@@ -138,13 +138,13 @@
 (* 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)
@@ -154,7 +154,7 @@
 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)
@@ -166,7 +166,7 @@
 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)
@@ -183,7 +183,7 @@
 (* 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)
@@ -211,7 +211,7 @@
   "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
@@ -227,13 +227,13 @@
 (* 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)
@@ -243,7 +243,7 @@
 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)
@@ -256,7 +256,7 @@
 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)
@@ -266,7 +266,7 @@
 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)
@@ -299,7 +299,7 @@
 | "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
@@ -313,13 +313,13 @@
 (* 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)
@@ -329,7 +329,7 @@
 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)
@@ -342,7 +342,7 @@
 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)
@@ -359,19 +359,19 @@
 (* 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)
@@ -399,7 +399,7 @@
 | "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
@@ -414,7 +414,7 @@
   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
@@ -448,13 +448,13 @@
 (* 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)
@@ -464,7 +464,7 @@
 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)
@@ -495,7 +495,7 @@
 | "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
@@ -518,7 +518,7 @@
 | "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
@@ -545,7 +545,7 @@
 | "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
@@ -565,7 +565,7 @@
 |  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
@@ -625,7 +625,7 @@
 | "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
@@ -651,7 +651,7 @@
 | "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
@@ -674,7 +674,7 @@
 | "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
diff -r 219e3ff68de8 -r fd483d8f486b Nominal/TySch.thy
--- a/Nominal/TySch.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -18,7 +18,7 @@
   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
@@ -61,13 +61,13 @@
 (* 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)
@@ -77,7 +77,7 @@
 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)
@@ -88,7 +88,7 @@
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_inject)
+  apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen)
   apply(auto)
@@ -97,7 +97,7 @@
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
-  apply(simp add: t_tyS_inject)
+  apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
   apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts)
   apply auto
@@ -105,18 +105,18 @@
 
 lemma
   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(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_inject)
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
 oops
 
 lemma
   assumes a: "a \<noteq> b"
   shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
   using a
-  apply(simp add: t_tyS_inject)
+  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_inject)
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
   apply auto
   done