--- a/Nominal/Ex/Classical.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Classical.thy Thu Aug 26 02:08:00 2010 +0800
@@ -7,8 +7,6 @@
atom_decl name
atom_decl coname
-declare [[STEPS = 21]]
-
nominal_datatype trm =
Ax "name" "coname"
| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
@@ -18,15 +16,15 @@
| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
+thm trm.distinct
+thm trm.induct
+thm trm.exhaust
+thm trm.fv_defs
+thm trm.bn_defs
+thm trm.perm_simps
+thm trm.eq_iff
+thm trm.fv_bn_eqvt
+thm trm.size_eqvt
--- a/Nominal/Ex/CoreHaskell.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy Thu Aug 26 02:08:00 2010 +0800
@@ -8,9 +8,10 @@
atom_decl cvar
atom_decl tvar
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
-nominal_datatype tkind =
+nominal_datatype core_haskell:
+ tkind =
KStar
| KFun "tkind" "tkind"
and ckind =
@@ -85,31 +86,19 @@
| "bv_cvs CvsNil = []"
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
-(* can lift *)
-
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
-
+(* generated theorems *)
-
-
+thm core_haskell.distinct
+thm core_haskell.induct
+thm core_haskell.exhaust
+thm core_haskell.fv_defs
+thm core_haskell.bn_defs
+thm core_haskell.perm_simps
+thm core_haskell.eq_iff
+thm core_haskell.fv_bn_eqvt
+thm core_haskell.size_eqvt
-lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
-lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
-lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
-lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
-lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts
-
-lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts
-lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros
-
+(*
lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
unfolding fresh_star_def Ball_def
by auto (simp_all add: fresh_minus_perm)
@@ -397,7 +386,7 @@
apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
-(* GOAL1 *)
+--"GOAL1"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
apply clarify
@@ -435,7 +424,7 @@
apply (simp only: supp_abs eqvts)
apply blast
-(* GOAL2 *)
+--"GOAL2"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
apply clarify
@@ -474,7 +463,7 @@
apply blast
-(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
+--"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
@@ -512,7 +501,7 @@
apply (simp only: supp_abs eqvts)
apply blast
-(* GOAL4 a copy-and-paste *)
+--"GOAL4 a copy-and-paste"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
@@ -551,7 +540,7 @@
apply blast
-(* GOAL5 a copy-and-paste *)
+--"GOAL5 a copy-and-paste"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
@@ -590,7 +579,7 @@
apply blast
-(* GOAL6 a copy-and-paste *)
+--"GOAL6 a copy-and-paste"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
apply clarify
@@ -629,7 +618,7 @@
apply (simp only: supp_abs eqvts)
apply blast
-(* MAIN ACons Goal *)
+--"MAIN ACons Goal"
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
@@ -655,6 +644,7 @@
moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
qed
+*)
section {* test about equivariance for alpha *}
--- a/Nominal/Ex/Ex1rec.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-theory Ex1rec
-imports "../NewParser"
-begin
-
-declare [[STEPS = 9]]
-
-atom_decl name
-
-nominal_datatype lam =
- Var "name"
-| App "lam" "lam"
-| Lam x::"name" t::"lam" bind_set x in t
-| Let bp::"bp" t::"lam" bind_set "bi bp" in bp t
-and bp =
- Bp "name" "lam"
-binder
- bi::"bp \<Rightarrow> atom set"
-where
- "bi (Bp x t) = {atom x}"
-
-
-thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros
-
-thm lam_bp.fv
-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
-thm lam_bp.supp
-ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp(1-2)]
-
-
-
-end
-
-
-
--- a/Nominal/Ex/Ex2.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-theory Ex2
-imports "../NewParser"
-begin
-
-text {* example 2 *}
-declare [[STEPS = 9]]
-
-atom_decl name
-
-nominal_datatype trm =
- Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm" bind_set x in t
-| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
-and pat =
- PN
-| PS "name"
-| PD "name" "name"
-binder
- f::"pat \<Rightarrow> atom set"
-where
- "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
-
-thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]
-thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
-
-
-
-
-thm trm_pat.bn
-thm trm_pat.perm
-thm trm_pat.induct
-thm trm_pat.distinct
-thm trm_pat.fv[simplified trm_pat.supp(1-2)]
-
-
-end
-
-
-
--- a/Nominal/Ex/Ex3.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-theory Ex3
-imports "../NewParser"
-begin
-
-(* Example 3, identical to example 1 from Terms.thy *)
-
-atom_decl name
-
-nominal_datatype trm =
- Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm" bind_set x in t
-| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
-and pat =
- PN
-| PS "name"
-| PD "pat" "pat"
-binder
- f::"pat \<Rightarrow> atom set"
-where
- "f PN = {}"
-| "f (PS x) = {atom x}"
-| "f (PD p1 p2) = (f p1) \<union> (f p2)"
-
-thm trm_pat.fv
-thm trm_pat.eq_iff
-thm trm_pat.bn
-thm trm_pat.perm
-thm trm_pat.induct
-thm trm_pat.distinct
-thm trm_pat.fv[simplified trm_pat.supp(1-2)]
-
-
-
-end
-
-
-
--- a/Nominal/Ex/Ex4.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-theory Ex4
-imports "../NewParser"
-begin
-
-declare [[STEPS = 5]]
-
-atom_decl name
-
-nominal_datatype trm =
- Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm" bind_set x in t
-| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
-| Foo1 p::"pat" q::"pat" t::"trm" bind_set "f p" "f q" in t
-| Foo2 x::"name" p::"pat" t::"trm" bind_set x "f p" in t
-and pat =
- PN
-| PS "name"
-| PD "pat" "pat"
-binder
- f::"pat \<Rightarrow> atom set"
-where
- "f PN = {}"
-| "f (PS x) = {atom x}"
-| "f (PD p1 p2) = (f p1) \<union> (f p2)"
-
-thm permute_trm_raw_permute_pat_raw.simps
-thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps
-
-thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
-
-(*
-inductive
- alpha_trm_raw and alpha_pat_raw and alpha_f_raw
-where
-(* alpha_trm_raw *)
- "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
-| "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk>
- \<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)"
-| "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow>
- alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
-| "\<lbrakk>\<exists>p. (f_raw pat_raw, trm_raw2) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_rawa, trm_raw2a);
- alpha_f_raw pat_raw pat_rawa; alpha_trm_raw trm_raw1 trm_raw1a\<rbrakk>
- \<Longrightarrow> alpha_trm_raw (Let_raw pat_raw trm_raw1 trm_raw2) (Let_raw pat_rawa trm_raw1a trm_raw2a)"
-| "\<lbrakk>\<exists>p. (f_raw pat_raw1 \<union> f_raw pat_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_raw1a \<union> f_raw pat_raw2a, trm_rawa);
- alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
- \<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)"
-| "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa);
- alpha_f_raw pat_raw pat_rawa\<rbrakk>
- \<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)"
-
-(* alpha_pat_raw *)
-| "alpha_pat_raw PN_raw PN_raw"
-| "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)"
-| "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk>
- \<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
-
-(* alpha_f_raw *)
-| "alpha_f_raw PN_raw PN_raw"
-| "alpha_f_raw (PS_raw name) (PS_raw namea)"
-| "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
- \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
-*)
-
-lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros
-
-lemma
- shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x))
- (Foo2_raw y (PS_raw y) (Var_raw y))"
-apply(rule all)
-apply(rule_tac x="(atom x \<rightleftharpoons> atom y)" in exI)
-apply(simp add: alphas)
-apply(simp add: supp_at_base fresh_star_def)
-apply(rule conjI)
-apply(rule all)
-apply(simp)
-apply(perm_simp)
-apply(simp)
-apply(rule all)
-done
-
-
-
-end
-
-
-
--- a/Nominal/Ex/ExLet.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-theory ExLet
-imports "../NewParser" "../../Attic/Prove"
-begin
-
-text {* example 3 or example 5 from Terms.thy *}
-
-atom_decl name
-
-nominal_datatype trm =
- Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind_set x in t
-| Lt a::"lts" t::"trm" bind "bn a" in t
-(*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*)
-and lts =
- Lnil
-| Lcons "name" "trm" "lts"
-binder
- bn
-where
- "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-
-thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros
-
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct[no_vars]
-thm trm_lts.inducts[no_vars]
-thm trm_lts.distinct
-(*thm trm_lts.supp*)
-thm trm_lts.fv[simplified trm_lts.supp(1-2)]
-
-
-primrec
- permute_bn_raw
-where
- "permute_bn_raw pi (Lnil_raw) = Lnil_raw"
-| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
-
-quotient_definition
- "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
-is
- "permute_bn_raw"
-
-lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
- apply simp
- apply clarify
- apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
- apply (rule TrueI)+
- apply simp_all
- apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
- apply simp_all
- done
-
-lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
-
-lemma permute_bn_zero:
- "permute_bn 0 a = a"
- apply(induct a rule: trm_lts.inducts(2))
- apply(rule TrueI)+
- apply(simp_all add:permute_bn)
- done
-
-lemma permute_bn_add:
- "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
- oops
-
-lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
- apply(induct lts rule: trm_lts.inducts(2))
- apply(rule TrueI)+
- apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
- done
-
-lemma perm_bn:
- "p \<bullet> bn l = bn(permute_bn p l)"
- apply(induct l rule: trm_lts.inducts(2))
- apply(rule TrueI)+
- apply(simp_all add:permute_bn eqvts)
- done
-
-lemma fv_perm_bn:
- "fv_bn l = fv_bn (permute_bn p l)"
- apply(induct l rule: trm_lts.inducts(2))
- apply(rule TrueI)+
- apply(simp_all add:permute_bn eqvts)
- done
-
-lemma Lt_subst:
- "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
- apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
- apply (rule_tac x="q" in exI)
- apply (simp add: alphas)
- apply (simp add: perm_bn[symmetric])
- apply(rule conjI)
- apply(drule supp_perm_eq)
- apply(simp add: abs_eq_iff)
- apply(simp add: alphas_abs alphas)
- apply(drule conjunct1)
- apply (simp add: trm_lts.supp)
- apply(simp add: supp_abs)
- apply (simp add: trm_lts.supp)
- done
-
-
-lemma fin_bn:
- "finite (set (bn l))"
- apply(induct l rule: trm_lts.inducts(2))
- apply(simp_all add:permute_bn eqvts)
- done
-
-thm trm_lts.inducts[no_vars]
-
-lemma
- fixes t::trm
- and l::lts
- and c::"'a::fs"
- assumes a1: "\<And>name c. P1 c (Vr name)"
- and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
- and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
- and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
- and a5: "\<And>c. P2 c Lnil"
- and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
- shows "P1 c t" and "P2 c l"
-proof -
- have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
- b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
- apply(induct rule: trm_lts.inducts)
- apply(simp)
- apply(rule a1)
- apply(simp)
- apply(rule a2)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
- apply(erule exE)
- apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)"
- and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
- apply(rule supp_perm_eq)
- apply(simp)
- apply(simp)
- apply(rule a3)
- apply(simp add: atom_eqvt)
- apply(subst permute_plus[symmetric])
- apply(blast)
- apply(rule at_set_avoiding2_atom)
- apply(simp add: finite_supp)
- apply(simp add: finite_supp)
- apply(simp add: fresh_def)
- apply(simp add: trm_lts.fv[simplified trm_lts.supp])
- apply(simp)
- apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
- apply(erule exE)
- apply(erule conjE)
- thm Lt_subst
- apply(subst Lt_subst)
- apply assumption
- apply(rule a4)
- apply(simp add:perm_bn[symmetric])
- apply(simp add: eqvts)
- apply (simp add: fresh_star_def fresh_def)
- apply(rotate_tac 1)
- apply(drule_tac x="q + p" in meta_spec)
- apply(simp)
- apply(rule at_set_avoiding2)
- apply(rule fin_bn)
- apply(simp add: finite_supp)
- apply(simp add: finite_supp)
- apply(simp add: fresh_star_def fresh_def supp_abs)
- apply(simp add: eqvts permute_bn)
- apply(rule a5)
- apply(simp add: permute_bn)
- apply(rule a6)
- apply simp
- apply simp
- done
- then have a: "P1 c (0 \<bullet> t)" by blast
- have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
- then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
-qed
-
-
-
-lemma lets_bla:
- "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
- by (simp add: trm_lts.eq_iff)
-
-lemma lets_ok:
- "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
- apply (simp add: trm_lts.eq_iff)
- apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
- done
-
-lemma lets_ok3:
- "x \<noteq> y \<Longrightarrow>
- (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
- (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
- apply (simp add: alphas trm_lts.eq_iff)
- done
-
-
-lemma lets_not_ok1:
- "x \<noteq> y \<Longrightarrow>
- (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
- (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
- apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
- done
-
-lemma lets_nok:
- "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
- (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
- apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
- done
-
-
-end
-
-
-
--- a/Nominal/Ex/ExLetMult.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-theory ExLetMult
-imports "../NewParser"
-begin
-
-atom_decl name
-
-nominal_datatype trm =
- Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind_set x in t
-| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t s
-and lts =
- Lnil
-| Lcons "name" "trm" "lts"
-binder
- bn
-where
- "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-thm trm_lts.eq_iff
-thm trm_lts.induct
-thm trm_lts.fv[simplified trm_lts.supp]
-
-
-
-end
-
-
-
--- a/Nominal/Ex/ExLetRec.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-theory ExLetRec
-imports "../NewParser"
-begin
-
-
-text {* example 3 or example 5 from Terms.thy *}
-
-atom_decl name
-
-ML {* val _ = cheat_equivp := true *}
-
-nominal_datatype trm =
- Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind_set x in t
-| Lt a::"lts" t::"trm" bind "bn a" in a t
-and lts =
- Lnil
-| Lcons "name" "trm" "lts"
-binder
- bn
-where
- "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct
-thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp]
-
-
-(* why is this not in HOL simpset? *)
-lemma set_sub: "{a, b} - {b} = {a} - {b}"
-by auto
-
-lemma lets_bla:
- "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
- apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
- done
-
-lemma lets_ok:
- "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
- apply (simp add: trm_lts.eq_iff)
- apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
- done
-
-lemma lets_ok3:
- "x \<noteq> y \<Longrightarrow>
- (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
- (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
- apply (simp add: alphas trm_lts.eq_iff)
- done
-
-
-lemma lets_not_ok1:
- "x \<noteq> y \<Longrightarrow>
- (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
- (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
- apply (simp add: alphas trm_lts.eq_iff)
- done
-
-lemma lets_nok:
- "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
- (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
- apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
- done
-
-lemma lets_ok4:
- "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
- (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
- apply (simp add: alphas trm_lts.eq_iff supp_at_base)
- apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp add: atom_eqvt fresh_star_def)
- done
-
-end
-
-
-
--- a/Nominal/Ex/ExPS3.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/ExPS3.thy Thu Aug 26 02:08:00 2010 +0800
@@ -6,14 +6,11 @@
atom_decl name
-ML {* val _ = cheat_equivp := true *}
-ML {* val _ = cheat_alpha_bn_rsp := true *}
-
nominal_datatype exp =
Var "name"
| App "exp" "exp"
-| Lam x::"name" e::"exp" bind_set x in e
-| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
+| Lam x::"name" e::"exp" bind x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1
and pat =
PVar "name"
| PUnit
@@ -25,16 +22,16 @@
| "bp (PUnit) = {}"
| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
-thm exp_pat.fv
-thm exp_pat.eq_iff
-thm exp_pat.bn
-thm exp_pat.perm
+
+thm exp_pat.distinct
thm exp_pat.induct
-thm exp_pat.distinct
-thm exp_pat.fv
-thm exp_pat.supp(1-2)
-
-
+thm exp_pat.exhaust
+thm exp_pat.fv_defs
+thm exp_pat.bn_defs
+thm exp_pat.perm_simps
+thm exp_pat.eq_iff
+thm exp_pat.fv_bn_eqvt
+thm exp_pat.size_eqvt
end
--- a/Nominal/Ex/ExPS6.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-theory ExPS6
-imports "../NewParser"
-begin
-
-(* example 6 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-(* Is this binding structure supported - I think not
- because e1 occurs twice as body *)
-
-nominal_datatype exp =
- Var name
-| Pair exp exp
-| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1
-and pat =
- PVar name
-| PUnit
-| PPair pat pat
-binder
- bp :: "pat \<Rightarrow> atom list"
-where
- "bp (PVar x) = [atom x]"
-| "bp (PUnit) = []"
-| "bp (PPair p1 p2) = bp p1 @ bp p2"
-
-thm exp_pat.fv
-thm exp_pat.eq_iff
-thm exp_pat.bn
-thm exp_pat.perm
-thm exp_pat.induct
-thm exp_pat.distinct
-thm exp_pat.supp
-
-
-
-
-end
-
-
-
--- a/Nominal/Ex/ExPS7.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/ExPS7.thy Thu Aug 26 02:08:00 2010 +0800
@@ -11,7 +11,7 @@
Var name
| Unit
| Pair exp exp
-| LetRec l::"lrbs" e::"exp" bind_set "bs l" in l e
+| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e
and lrb =
Assign name exp
and lrbs =
@@ -25,8 +25,6 @@
| "bs (Single a) = b a"
| "bs (More a as) = (b a) \<union> (bs as)"
-thm exp_lrb_lrbs.eq_iff
-thm exp_lrb_lrbs.supp
end
--- a/Nominal/Ex/ExPS8.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/ExPS8.thy Thu Aug 26 02:08:00 2010 +0800
@@ -6,17 +6,13 @@
atom_decl name
-ML {* val _ = cheat_fv_rsp := true *}
-ML {* val _ = cheat_equivp := true *}
-ML {* val _ = cheat_alpha_bn_rsp := true *}
-
nominal_datatype exp =
EVar name
| EUnit
| EPair exp exp
-| ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e
+| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
and fnclause =
- K x::name p::pat f::exp bind_set "b_pat p" in f
+ K x::name p::pat f::exp bind (set) "b_pat p" in f
and fnclauses =
S fnclause
| ORs fnclause fnclauses
@@ -46,8 +42,6 @@
| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
| "b_fnclause (K x pat exp) = {atom x}"
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
end
--- a/Nominal/Ex/LF.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/LF.thy Thu Aug 26 02:08:00 2010 +0800
@@ -2,7 +2,7 @@
imports "../NewParser"
begin
-declare [[STEPS = 9]]
+declare [[STEPS = 20]]
atom_decl name
atom_decl ident
@@ -13,17 +13,14 @@
and ty =
TConst "ident"
| TApp "ty" "trm"
- | TPi "ty" n::"name" t::"ty" bind n in t
+ | TPi "ty" n::"name" ty::"ty" bind n in ty
and trm =
Const "ident"
| Var "name"
| App "trm" "trm"
| Lam "ty" n::"name" t::"trm" bind n in t
-thm kind_ty_trm.supp
-
-
-
+(*thm kind_ty_trm.supp*)
end
--- a/Nominal/Ex/Lambda.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Lambda.thy Thu Aug 26 02:08:00 2010 +0800
@@ -5,32 +5,22 @@
atom_decl name
declare [[STEPS = 21]]
-class s1
-class s2
-
-nominal_datatype lambda:
- ('a, 'b) lam =
+nominal_datatype lam =
Var "name"
-| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
-| Lam x::"name" l::"('a, 'b) lam" bind x in l
+| App "lam" "lam"
+| Lam x::"name" l::"lam" bind x in l
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
+thm lam.distinct
+thm lam.induct
+thm lam.exhaust
+thm lam.fv_defs
+thm lam.bn_defs
+thm lam.perm_simps
+thm lam.eq_iff
+thm lam.fv_bn_eqvt
+thm lam.size_eqvt
-thm lam.fv
-thm lam.supp
-lemmas supp_fn' = lam.fv[simplified lam.supp]
-
-declare lam.perm[eqvt]
-
section {* Strong Induction Principles*}
@@ -38,6 +28,7 @@
Old way of establishing strong induction
principles by chosing a fresh name.
*)
+(*
lemma
fixes c::"'a::fs"
assumes a1: "\<And>name c. P c (Var name)"
@@ -79,11 +70,12 @@
then have "P c (0 \<bullet> lam)" by blast
then show "P c lam" by simp
qed
-
+*)
(*
New way of establishing strong induction
principles by using a appropriate permutation.
*)
+(*
lemma
fixes c::"'a::fs"
assumes a1: "\<And>name c. P c (Var name)"
@@ -121,6 +113,7 @@
then have "P c (0 \<bullet> lam)" by blast
then show "P c lam" by simp
qed
+*)
section {* Typing *}
@@ -131,6 +124,7 @@
notation
TFun ("_ \<rightarrow> _")
+(*
declare ty.perm[eqvt]
inductive
@@ -237,7 +231,7 @@
apply(simp add: finite_supp)
apply(rule_tac p="-p" in permute_boolE)
apply(perm_strict_simp add: permute_minus_cancel)
- (* supplied by the user *)
+ --"supplied by the user"
apply(simp add: fresh_star_prod)
apply(simp add: fresh_star_def)
sorry
@@ -246,86 +240,9 @@
then show "P c \<Gamma> t T" by simp
qed
-
-
-
-
-
-
-inductive
- tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
- for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
-where
- aa: "tt r a a"
- | bb: "tt r a b ==> tt r a c"
-
-(* PROBLEM: derived eqvt-theorem does not conform with [eqvt]
-equivariance tt
*)
-inductive
- alpha_lam_raw'
-where
- a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
-| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
- alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
-| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
- alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
-
-equivariance alpha_lam_raw'
-
-thm eqvts_raw
-
-section {* size function *}
-
-lemma size_eqvt_raw:
- fixes t::"lam_raw"
- shows "size (pi \<bullet> t) = size t"
- apply (induct rule: lam_raw.inducts)
- apply simp_all
- done
-
-instantiation lam :: size
-begin
-
-quotient_definition
- "size_lam :: lam \<Rightarrow> nat"
-is
- "size :: lam_raw \<Rightarrow> nat"
-
-lemma size_rsp:
- "alpha_lam_raw x y \<Longrightarrow> size x = size y"
- apply (induct rule: alpha_lam_raw.inducts)
- apply (simp_all only: lam_raw.size)
- apply (simp_all only: alphas)
- apply clarify
- apply (simp_all only: size_eqvt_raw)
- done
-
-lemma [quot_respect]:
- "(alpha_lam_raw ===> op =) size size"
- by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
- "(rep_lam ---> id) size = size"
- by (simp_all add: size_lam_def)
-
-instance
- by default
-
-end
-
-lemmas size_lam[simp] =
- lam_raw.size(4)[quot_lifted]
- lam_raw.size(5)[quot_lifted]
- lam_raw.size(6)[quot_lifted]
-
-(* is this needed? *)
-lemma [measure_function]:
- "is_measure (size::lam\<Rightarrow>nat)"
- by (rule is_measure_trivial)
-
section {* Matching *}
definition
@@ -512,6 +429,7 @@
| "match_App_raw (App_raw x y) = Some (x, y)"
| "match_App_raw (Lam_raw n t) = None"
+(*
quotient_definition
"match_App :: lam \<Rightarrow> (lam \<times> lam) option"
is match_App_raw
@@ -547,7 +465,7 @@
apply (simp add: lam_half_inj)
apply auto
done
-
+*)
(*
lemma match_Lam_simps2:
"atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)"
@@ -627,7 +545,7 @@
lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted]
*)
-
+(*
lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
by (induct x rule: lam.induct) (simp_all add: match_App_simps)
@@ -767,7 +685,7 @@
apply (simp only: option.simps)
apply (simp only: prod.simps)
sorry
-
+*)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Let.thy Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,224 @@
+theory Let
+imports "../NewParser"
+begin
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+nominal_datatype trm =
+ Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm" bind x in t
+| Let a::"lts" t::"trm" bind "bn a" in t
+and lts =
+ Lnil
+| Lcons "name" "trm" "lts"
+binder
+ bn
+where
+ "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+
+(*
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct[no_vars]
+thm trm_lts.inducts[no_vars]
+thm trm_lts.distinct
+thm trm_lts.supp
+thm trm_lts.fv[simplified trm_lts.supp(1-2)]
+
+
+primrec
+ permute_bn_raw
+where
+ "permute_bn_raw pi (Lnil_raw) = Lnil_raw"
+| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
+
+quotient_definition
+ "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
+is
+ "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
+ apply simp
+ apply clarify
+ apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+ apply (rule TrueI)+
+ apply simp_all
+ apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+ apply simp_all
+ done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma permute_bn_zero:
+ "permute_bn 0 a = a"
+ apply(induct a rule: trm_lts.inducts(2))
+ apply(rule TrueI)+
+ apply(simp_all add:permute_bn)
+ done
+
+lemma permute_bn_add:
+ "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
+ oops
+
+lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
+ apply(induct lts rule: trm_lts.inducts(2))
+ apply(rule TrueI)+
+ apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
+ done
+
+lemma perm_bn:
+ "p \<bullet> bn l = bn(permute_bn p l)"
+ apply(induct l rule: trm_lts.inducts(2))
+ apply(rule TrueI)+
+ apply(simp_all add:permute_bn eqvts)
+ done
+
+lemma fv_perm_bn:
+ "fv_bn l = fv_bn (permute_bn p l)"
+ apply(induct l rule: trm_lts.inducts(2))
+ apply(rule TrueI)+
+ apply(simp_all add:permute_bn eqvts)
+ done
+
+lemma Lt_subst:
+ "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+ apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
+ apply (rule_tac x="q" in exI)
+ apply (simp add: alphas)
+ apply (simp add: perm_bn[symmetric])
+ apply(rule conjI)
+ apply(drule supp_perm_eq)
+ apply(simp add: abs_eq_iff)
+ apply(simp add: alphas_abs alphas)
+ apply(drule conjunct1)
+ apply (simp add: trm_lts.supp)
+ apply(simp add: supp_abs)
+ apply (simp add: trm_lts.supp)
+ done
+
+
+lemma fin_bn:
+ "finite (set (bn l))"
+ apply(induct l rule: trm_lts.inducts(2))
+ apply(simp_all add:permute_bn eqvts)
+ done
+
+thm trm_lts.inducts[no_vars]
+
+lemma
+ fixes t::trm
+ and l::lts
+ and c::"'a::fs"
+ assumes a1: "\<And>name c. P1 c (Vr name)"
+ and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
+ and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
+ and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
+ and a5: "\<And>c. P2 c Lnil"
+ and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
+ shows "P1 c t" and "P2 c l"
+proof -
+ have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
+ b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
+ apply(induct rule: trm_lts.inducts)
+ apply(simp)
+ apply(rule a1)
+ apply(simp)
+ apply(rule a2)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+ apply(erule exE)
+ apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)"
+ and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
+ apply(rule supp_perm_eq)
+ apply(simp)
+ apply(simp)
+ apply(rule a3)
+ apply(simp add: atom_eqvt)
+ apply(subst permute_plus[symmetric])
+ apply(blast)
+ apply(rule at_set_avoiding2_atom)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: fresh_def)
+ apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+ apply(simp)
+ apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+ apply(erule exE)
+ apply(erule conjE)
+ thm Lt_subst
+ apply(subst Lt_subst)
+ apply assumption
+ apply(rule a4)
+ apply(simp add:perm_bn[symmetric])
+ apply(simp add: eqvts)
+ apply (simp add: fresh_star_def fresh_def)
+ apply(rotate_tac 1)
+ apply(drule_tac x="q + p" in meta_spec)
+ apply(simp)
+ apply(rule at_set_avoiding2)
+ apply(rule fin_bn)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: fresh_star_def fresh_def supp_abs)
+ apply(simp add: eqvts permute_bn)
+ apply(rule a5)
+ apply(simp add: permute_bn)
+ apply(rule a6)
+ apply simp
+ apply simp
+ done
+ then have a: "P1 c (0 \<bullet> t)" by blast
+ have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+ then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+
+
+
+lemma lets_bla:
+ "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
+ by (simp add: trm_lts.eq_iff)
+
+lemma lets_ok:
+ "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+ apply (simp add: trm_lts.eq_iff)
+ apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
+ done
+
+lemma lets_ok3:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+ apply (simp add: alphas trm_lts.eq_iff)
+ done
+
+
+lemma lets_not_ok1:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+ apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
+ done
+
+lemma lets_nok:
+ "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+ apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+ done
+*)
+
+end
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetPat.thy Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,39 @@
+theory LetPat
+imports "../NewParser"
+begin
+
+declare [[STEPS = 100]]
+
+atom_decl name
+
+nominal_datatype trm =
+ Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm" bind (set) x in t
+| Let p::"pat" "trm" t::"trm" bind (set) "f p" in t
+and pat =
+ PN
+| PS "name"
+| PD "name" "name"
+binder
+ f::"pat \<Rightarrow> atom set"
+where
+ "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
+| "f (PS x) = {atom x}"
+
+thm trm_pat.distinct
+thm trm_pat.induct
+thm trm_pat.exhaust
+thm trm_pat.fv_defs
+thm trm_pat.bn_defs
+thm trm_pat.perm_simps
+thm trm_pat.eq_iff
+thm trm_pat.fv_bn_eqvt
+thm trm_pat.size_eqvt
+
+
+end
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetRec.thy Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,36 @@
+theory LetRec
+imports "../NewParser"
+begin
+
+declare [[STEPS = 14]]
+
+atom_decl name
+
+nominal_datatype let_rec:
+ lam =
+ Var "name"
+| App "lam" "lam"
+| Lam x::"name" t::"lam" bind (set) x in t
+| Let_Rec bp::"bp" t::"lam" bind (set) "bi bp" in bp t
+and bp =
+ Bp "name" "lam"
+binder
+ bi::"bp \<Rightarrow> atom set"
+where
+ "bi (Bp x t) = {atom x}"
+
+thm let_rec.distinct
+thm let_rec.induct
+thm let_rec.exhaust
+thm let_rec.fv_defs
+thm let_rec.bn_defs
+thm let_rec.perm_simps
+thm let_rec.eq_iff
+thm let_rec.fv_bn_eqvt
+thm let_rec.size_eqvt
+
+
+end
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetRec2.thy Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,82 @@
+theory LetRec2
+imports "../NewParser"
+begin
+
+atom_decl name
+
+nominal_datatype trm =
+ Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm" bind (set) x in t
+| Lt a::"lts" t::"trm" bind "bn a" in a t
+and lts =
+ Lnil
+| Lcons "name" "trm" "lts"
+binder
+ bn
+where
+ "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct
+thm trm_lts.distinct
+thm trm_lts.supp
+thm trm_lts.fv[simplified trm_lts.supp]
+
+
+(* why is this not in HOL simpset? *)
+(*
+lemma set_sub: "{a, b} - {b} = {a} - {b}"
+by auto
+
+lemma lets_bla:
+ "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
+ apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
+ done
+
+lemma lets_ok:
+ "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+ apply (simp add: trm_lts.eq_iff)
+ apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
+ done
+
+lemma lets_ok3:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+ apply (simp add: alphas trm_lts.eq_iff)
+ done
+
+
+lemma lets_not_ok1:
+ "x \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+ apply (simp add: alphas trm_lts.eq_iff)
+ done
+
+lemma lets_nok:
+ "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+ apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+ done
+
+lemma lets_ok4:
+ "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+ (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
+ apply (simp add: alphas trm_lts.eq_iff supp_at_base)
+ apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ apply (simp add: atom_eqvt fresh_star_def)
+ done
+
+end
+
+
+
--- a/Nominal/Ex/Modules.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Modules.thy Thu Aug 26 02:08:00 2010 +0800
@@ -7,15 +7,16 @@
atom_decl name
-nominal_datatype mexp =
+nominal_datatype modules:
+ mexp =
Acc "path"
| Stru "body"
-| Funct x::"name" "sexp" m::"mexp" bind_set x in m
+| Funct x::"name" "sexp" m::"mexp" bind (set) x in m
| FApp "mexp" "path"
| Ascr "mexp" "sexp"
and body =
Empty
-| Seq c::defn d::"body" bind_set "cbinders c" in d
+| Seq c::"defn" d::"body" bind (set) "cbinders c" in d
and defn =
Type "name" "ty"
| Dty "name"
@@ -26,7 +27,7 @@
| SFunc "name" "sexp" "sexp"
and sbody =
SEmpty
-| SSeq C::spec D::sbody bind_set "Cbinders C" in D
+| SSeq C::"spec" D::"sbody" bind (set) "Cbinders C" in D
and spec =
Type1 "name"
| Type2 "name" "ty"
@@ -42,7 +43,7 @@
and trm =
Tref1 "name"
| Tref2 "path" "name"
-| Lam' v::"name" "ty" M::"trm" bind_set v in M
+| Lam' v::"name" "ty" M::"trm" bind (set) v in M
| App' "trm" "trm"
| Let' "body" "trm"
binder
@@ -58,15 +59,16 @@
| "Cbinders (SStru x S) = {atom x}"
| "Cbinders (SVal v T) = {atom v}"
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
+
+thm modules.distinct
+thm modules.induct
+thm modules.exhaust
+thm modules.fv_defs
+thm modules.bn_defs
+thm modules.perm_simps
+thm modules.eq_iff
+thm modules.fv_bn_eqvt
+thm modules.size_eqvt
--- a/Nominal/Ex/NoneExamples.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/NoneExamples.thy Thu Aug 26 02:08:00 2010 +0800
@@ -4,6 +4,40 @@
atom_decl name
+
+text {*
+ "Weirdo" example from Peter Sewell's bestiary.
+
+ This example is not covered by our binding
+ specification.
+
+*}
+
+nominal_datatype weird =
+ Foo_var "name"
+| Foo_pair "weird" "weird"
+| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+ bind x in p1 p2,
+ bind y in p2 p3
+
+(* e1 occurs in two bodies *)
+
+nominal_datatype exp =
+ Var name
+| Pair exp exp
+| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1
+and pat =
+ PVar name
+| PUnit
+| PPair pat pat
+binder
+ bp :: "pat \<Rightarrow> atom list"
+where
+ "bp (PVar x) = [atom x]"
+| "bp (PUnit) = []"
+| "bp (PPair p1 p2) = bp p1 @ bp p2"
+
+
(* this example binds bound names and
so is not respectful *)
(*
--- a/Nominal/Ex/SingleLet.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy Thu Aug 26 02:08:00 2010 +0800
@@ -4,9 +4,9 @@
atom_decl name
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
-nominal_datatype singlelet: trm =
+nominal_datatype single_let: trm =
Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm" bind x in t
@@ -21,19 +21,18 @@
where
"bn (As x y t) = {atom x}"
-
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
+thm single_let.distinct
+thm single_let.induct
+thm single_let.exhaust
+thm single_let.fv_defs
+thm single_let.bn_defs
+thm single_let.perm_simps
+thm single_let.eq_iff
+thm single_let.fv_bn_eqvt
+thm single_let.size_eqvt
-
+(*
lemma supp_fv:
@@ -67,10 +66,9 @@
thm trm_assg.inducts
thm trm_assg.distinct
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
+*)
-(* TEMPORARY
-thm trm_assg.fv[simplified trm_assg.supp(1-2)]
-*)
+
end
--- a/Nominal/Ex/Term8.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Term8.thy Thu Aug 26 02:08:00 2010 +0800
@@ -6,21 +6,21 @@
atom_decl name
-ML {* val _ = cheat_alpha_bn_rsp := true *}
-
nominal_datatype foo =
Foo0 "name"
-| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
+| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
and bar =
Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind_set s in b
+| Bar1 "name" s::"name" b::"bar" bind (set) s in b
binder
bv
where
"bv (Bar0 x) = {}"
| "bv (Bar1 v x b) = {atom v}"
+(*
thm foo_bar.supp
+*)
end
--- a/Nominal/Ex/Test.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-theory Test
-imports "../NewParser"
-begin
-
-declare [[STEPS = 4]]
-
-atom_decl name
-
-(*
-nominal_datatype trm =
- Vr "name"
-| Ap "trm" "trm"
-
-thm fv_trm_raw.simps[no_vars]
-*)
-
-(* This file contains only the examples that are not supposed to work yet. *)
-
-
-declare [[STEPS = 2]]
-
-
-(* example 4 from Terms.thy *)
-(* fv_eqvt does not work, we need to repaire defined permute functions
- defined fv and defined alpha... *)
-(* lists-datastructure does not work yet *)
-
-nominal_datatype trm =
- Vr "name"
-| Ap "trm" "trm list"
-| Lm x::"name" t::"trm" bind x in t
-
-(*
-thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
-*)
-
-end
-
-
--- a/Nominal/Ex/TestMorePerm.thy Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-theory TestMorePerm
-imports "../NewParser"
-begin
-
-text {*
- "Weirdo" example from Peter Sewell's bestiary.
-
- This example is not covered by our binding
- specification.
-
-*}
-ML {* val _ = cheat_equivp := true *}
-
-atom_decl name
-
-nominal_datatype weird =
- Foo_var "name"
-| Foo_pair "weird" "weird"
-| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
- bind x in p1 p2,
- bind y in p2 p3
-
-thm alpha_weird_raw.intros[no_vars]
-
-thm permute_weird_raw.simps[no_vars]
-thm alpha_weird_raw.intros[no_vars]
-thm fv_weird_raw.simps[no_vars]
-
-equivariance alpha_weird_raw
-
-
-end
-
-
-
--- a/Nominal/Ex/TypeSchemes.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy Thu Aug 26 02:08:00 2010 +0800
@@ -6,7 +6,7 @@
atom_decl name
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
nominal_datatype ty =
Var "name"
@@ -19,74 +19,11 @@
Var2 "name"
| Fun2 "ty2" "ty2"
-
nominal_datatype tys2 =
All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
-lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
-
-
-
-(* below we define manually the function for size *)
-
-lemma size_eqvt_raw:
- "size (pi \<bullet> t :: ty_raw) = size t"
- "size (pi \<bullet> ts :: tys_raw) = size ts"
- apply (induct rule: ty_raw_tys_raw.inducts)
- apply simp_all
- done
-
-instantiation ty and tys :: size
-begin
-
-quotient_definition
- "size_ty :: ty \<Rightarrow> nat"
-is
- "size :: ty_raw \<Rightarrow> nat"
-
-quotient_definition
- "size_tys :: tys \<Rightarrow> nat"
-is
- "size :: tys_raw \<Rightarrow> nat"
-
-lemma size_rsp:
- "alpha_ty_raw x y \<Longrightarrow> size x = size y"
- "alpha_tys_raw a b \<Longrightarrow> size a = size b"
- apply (induct rule: alpha_ty_raw_alpha_tys_raw.inducts)
- apply (simp_all only: ty_raw_tys_raw.size)
- apply (simp_all only: alphas)
- apply clarify
- apply (simp_all only: size_eqvt_raw)
- done
-
-lemma [quot_respect]:
- "(alpha_ty_raw ===> op =) size size"
- "(alpha_tys_raw ===> op =) size size"
- by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
- "(rep_ty ---> id) size = size"
- "(rep_tys ---> id) size = size"
- by (simp_all add: size_ty_def size_tys_def)
-
-instance
- by default
-
-end
-
-thm ty_raw_tys_raw.size(4)[quot_lifted]
-thm ty_raw_tys_raw.size(5)[quot_lifted]
-thm ty_raw_tys_raw.size(6)[quot_lifted]
-
-
-thm ty_tys.fv
-thm ty_tys.eq_iff
-thm ty_tys.bn
-thm ty_tys.perm
-thm ty_tys.inducts
-thm ty_tys.distinct
-
+(*
ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}
lemma strong_induct:
@@ -278,19 +215,6 @@
done
end
-
-(* PROBLEM:
-Type schemes with separate datatypes
-
-nominal_datatype T =
- TVar "name"
-| TFun "T" "T"
-nominal_datatype TyS =
- TAll xs::"name list" ty::"T" bind xs in ty
-
-*** exception Datatype raised
-*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
-*** At command "nominal_datatype".
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,30 @@
+theory TypeVarsTest
+imports "../NewParser"
+begin
+
+atom_decl name
+declare [[STEPS = 21]]
+
+class s1
+class s2
+
+nominal_datatype ('a, 'b) lam =
+ Var "name"
+| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
+| Lam x::"name" l::"('a, 'b) lam" bind x in l
+
+thm lam.distinct
+thm lam.induct
+thm lam.exhaust
+thm lam.fv_defs
+thm lam.bn_defs
+thm lam.perm_simps
+thm lam.eq_iff
+thm lam.fv_bn_eqvt
+thm lam.size_eqvt
+
+
+end
+
+
+
--- a/Nominal/NewParser.thy Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/NewParser.thy Thu Aug 26 02:08:00 2010 +0800
@@ -251,7 +251,7 @@
(* for testing porposes - to exit the procedure early *)
exception TEST of Proof.context
-val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0);
+val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100);
fun get_STEPS ctxt = Config.get ctxt STEPS
*}
@@ -259,7 +259,7 @@
setup STEPS_setup
ML {*
-fun nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses lthy =
+fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
let
(* definition of the raw datatypes *)
val _ = warning "Definition of raw datatypes";
@@ -437,7 +437,6 @@
val qty_full_names = map (fst o dest_Type) qtys
val qty_names = map Long_Name.base_name qty_full_names
-
(* defining of quotient term-constructors, binding functions, free vars functions *)
val _ = warning "Defining the quotient constants"
val qconstrs_descr =
@@ -517,24 +516,24 @@
||>> lift_thms qtys [] raw_exhaust_thms
else raise TEST lthyA
-
- (* temporary theorem bindings *)
+ (* noting the theorems *)
+
+ (* generating the prefix for the theorem names *)
+ val thms_name =
+ the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name
+ fun thms_suffix s = Binding.qualified true s thms_name
+
val (_, lthy9') = lthyB
- |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts)
- ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs)
- ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs)
- ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs)
- ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps)
- ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts)
- ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt)
- ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct])
- ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts)
+ |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts)
+ ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
+ ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs)
+ ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs)
+ ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps)
+ ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts)
+ ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
+ ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct])
+ ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
-
- val _ =
- if get_STEPS lthy > 21
- then true else raise TEST lthy9'
-
in
(0, lthy9')
end handle TEST ctxt => (0, ctxt)
@@ -692,11 +691,10 @@
*}
ML {*
-fun nominal_datatype2_cmd (opt_thm_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy =
+fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy =
let
- val (pre_typ_names, pre_typs) = split_list
- (map (fn (tvs, tname, mx, _) =>
- (Binding.name_of tname, (tname, length tvs, mx))) dt_strs)
+ val pre_typs =
+ map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs
(* this theory is used just for parsing *)
val thy = ProofContext.theory_of lthy
@@ -710,10 +708,8 @@
||>> prepare_bclauses dt_strs
val bclauses' = complete dt_strs bclauses
- val thm_name =
- the_default (Binding.name (space_implode "_" pre_typ_names)) opt_thm_name
in
- timeit (fn () => nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd)
+ timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd)
end
*}