--- 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 *)