diff -r 74888979e9cd -r 4355eb3b7161 Nominal/Test.thy
--- a/Nominal/Test.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Test.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -13,43 +13,7 @@
 | Ap "lm" "lm"
 | Lm x::"name" l::"lm"  bind x in l
 
-lemma finite_fv:
-  shows "finite (fv_lm t)"
-apply(induct t rule: lm.induct)
-apply(simp_all)
-done
-
-lemma supp_fn:
-  shows "supp t = fv_lm t"
-apply(induct t rule: lm.induct)
-apply(simp_all)
-apply(simp only: supp_def)
-apply(simp only: lm.perm)
-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.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)" and s="supp (Abs {atom name} lm)" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lm.perm)
-apply(simp only: permute_ABS)
-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)
-apply(simp only: supp_Abs)
-done
-
-lemmas supp_fn' = lm.fv[simplified supp_fn[symmetric]]
+lemmas supp_fn' = lm.fv[simplified lm.supp]
 
 lemma
   fixes c::"'a::fs"
@@ -67,6 +31,11 @@
     apply(blast)[1]
     apply(assumption)
     apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
+    defer
+    apply(simp add: fresh_def)
+    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
+    apply(simp add: supp_Pair finite_supp)
+    apply(blast)
     apply(erule exE)
     apply(rule_tac t="p \<bullet> Lm name lm" and 
                    s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
@@ -83,10 +52,6 @@
     apply(simp add: fresh_Pair)
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
-    apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
-    apply(simp add: supp_Pair finite_supp)
-    apply(blast)
     done
   then have "P c (0 \<bullet> lm)" by blast
   then show "P c lm" by simp
@@ -124,7 +89,6 @@
   then show "P c lm" by simp
 qed
 
-
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -138,6 +102,7 @@
   "bi (BP x t) = {atom x}"
 
 thm lam_bp.fv
+thm lam_bp.supp
 thm lam_bp.eq_iff
 thm lam_bp.bn
 thm lam_bp.perm
@@ -145,77 +110,7 @@
 thm lam_bp.inducts
 thm lam_bp.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-
-term "supp (x :: lam)"
-
-lemma bi_eqvt:
-  shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-  by (rule eqvts)
-
-lemma supp_fv:
-  shows "supp t = fv_lam t" 
-  and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
-apply(induct t and bp rule: lam_bp.inducts)
-apply(simp_all)
-(* VAR case *)
-apply(simp only: supp_def)
-apply(simp only: lam_bp.perm)
-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.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)" and s="supp (Abs {atom name} lam)" 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.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(simp only: supp_Abs)
-(* LET case *)
-apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" 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.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 only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(blast)
-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.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(simp only: supp_at_base)
-apply(simp)
-done
-
-thm lam_bp.fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+thm lam_bp.fv[simplified lam_bp.supp]
 
 ML {* val _ = recursive := true *}
 
@@ -240,69 +135,7 @@
 thm lam'_bp'.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
 
-lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
-apply (simp add: supp_Abs supp_Pair)
-apply blast
-done
-
-lemma supp_fv':
-  shows "supp t = fv_lam' t" 
-  and "supp bp = fv_bp' bp"
-apply(induct t and bp rule: lam'_bp'.inducts)
-apply(simp_all)
-(* VAR case *)
-apply(simp only: supp_def)
-apply(simp only: lam'_bp'.perm)
-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'.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')" and s="supp (Abs {atom name} lam')" 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'.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(simp only: supp_Abs)
-(* LET case *)
-apply(rule_tac t="supp (LET' bp' lam')" and 
-               s="supp (Abs (bi' bp') (bp', lam'))" 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'.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'.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(simp only: supp_at_base supp_atom)
-apply simp
-done
-
-thm lam'_bp'.fv[simplified supp_fv'[symmetric]]
+thm lam'_bp'.fv[simplified lam'_bp'.supp]
 
 
 text {* example 2 *}
@@ -330,83 +163,7 @@
 thm trm'_pat'.perm
 thm trm'_pat'.induct
 thm trm'_pat'.distinct
-
-lemma supp_fv_trm'_pat':
-  shows "supp t = fv_trm' t" 
-  and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
-apply(induct t and bp rule: trm'_pat'.inducts)
-apply(simp_all)
-(* VAR case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-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'.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')" and s="supp (Abs {atom name} trm')" 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'.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(simp only: supp_Abs)
-(* LET case *)
-apply(rule_tac t="supp (Let pat' trm'1 trm'2)" 
-           and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" 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'.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 only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(blast)
-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'.eq_iff)
-apply(simp)
-(* PS case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-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'.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(simp add: supp_at_base)
-done
-
-thm trm'_pat'.fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
+thm trm'_pat'.fv[simplified trm'_pat'.supp]
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -430,6 +187,7 @@
 thm trm0_pat0.perm
 thm trm0_pat0.induct
 thm trm0_pat0.distinct
+thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
 
 text {* example type schemes *}
 
@@ -445,61 +203,16 @@
 thm t_tyS.perm
 thm t_tyS.induct
 thm t_tyS.distinct
+thm t_tyS.fv[simplified t_tyS.supp]
 
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
 
-lemma finite_fv_t_tyS:
-  fixes T::"t"
-  and   S::"tyS"
-  shows "finite (fv_t T)" 
-  and   "finite (fv_tyS S)"
-apply(induct T and S rule: t_tyS.inducts)
-apply(simp_all add: t_tyS.fv)
-done
 
-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)
-(* VarTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS.perm)
-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.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 fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" 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.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: eqvts)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts eqvts_raw)
-apply(rule trans)
-apply(rule finite_supp_Abs)
-apply(simp add: finite_fv_t_tyS)
-apply(simp)
-done
 
 (* example 1 from Terms.thy *)
 
 
-  
-
-
 nominal_datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
@@ -522,6 +235,7 @@
 thm trm1_bp1.perm
 thm trm1_bp1.induct
 thm trm1_bp1.distinct
+thm trm1_bp1.fv[simplified trm1_bp1.supp]
 
 text {* example 3 from Terms.thy *}
 
@@ -545,6 +259,7 @@
 thm trm3_rassigns3.perm
 thm trm3_rassigns3.induct
 thm trm3_rassigns3.distinct
+thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp]
 
 (* example 5 from Terms.thy *)
 
@@ -567,47 +282,7 @@
 thm trm5_lts.perm
 thm trm5_lts.induct
 thm trm5_lts.distinct
-
-lemma
-  shows "fv_trm5 t = supp t"
-  and "fv_lts l = supp l \<and> fv_bv5 l = {a. infinite {b. \<not>alpha_bv5 ((a \<rightleftharpoons> b) \<bullet> l) l}}"
-apply(induct t and l rule: trm5_lts.inducts)
-apply(simp_all only: trm5_lts.fv)
-apply(simp_all only: supp_Abs[symmetric])
-(*apply(simp_all only: supp_abs_sum)*)
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: trm5_lts.perm)
-apply(simp_all only: permute_ABS)
-apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff)
-(*apply(simp_all only: alpha_gen2)*)
-apply(simp_all only: alpha_gen)
-apply(simp_all only: eqvts[symmetric] supp_Pair)
-apply(simp_all only: eqvts Pair_eq)
-apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-apply(simp_all only: de_Morgan_conj[symmetric])
-apply simp_all
-done
-
-(* example from my PHD *)
-
-atom_decl coname
-
-nominal_datatype phd =
-   Ax "name" "coname"
-|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
-|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
-|  AndL1 n::"name" t::"phd" "name"                              bind n in t
-|  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.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
+thm trm5_lts.fv[simplified trm5_lts.supp]
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -669,28 +344,30 @@
 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
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
 
-lemma
-"fv_mexp j = supp j \<and> fv_body k = supp k \<and> 
-(fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and>
-fv_sexp d = supp d \<and> fv_sbody e = supp e \<and> 
-(fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and>
-fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i"
-apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct)
-apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv)
-apply(simp_all only: supp_Abs[symmetric])
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm)
-apply(simp_all only: permute_ABS)
-apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff)
-apply(simp_all only: alpha_gen)
-apply(simp_all only: eqvts[symmetric] supp_Pair)
-apply(simp_all only: eqvts Pair_eq)
-apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-apply(simp_all only: de_Morgan_conj[symmetric])
-apply simp_all
-done
+
+(* example from my PHD *)
+
+atom_decl coname
+
+nominal_datatype phd =
+   Ax "name" "coname"
+|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"phd" "name"                              bind n in t
+|  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.eq_iff
+thm phd.bn
+thm phd.perm
+thm phd.induct
+thm phd.distinct
+thm phd.fv[simplified phd.supp]
 
 (* example 3 from Peter Sewell's bestiary *)
 
@@ -716,6 +393,7 @@
 thm exp_pat3.perm
 thm exp_pat3.induct
 thm exp_pat3.distinct
+thm exp_pat3.fv[simplified exp_pat3.supp]
 
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
@@ -740,6 +418,7 @@
 thm exp6_pat6.induct
 thm exp6_pat6.distinct
 
+
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 
 (* example 7 from Peter Sewell's bestiary *)