--- a/Nominal/Abs.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Abs.thy Mon Mar 29 00:30:47 2010 +0200
@@ -419,8 +419,9 @@
lemma Abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
- by (lifting alpha_abs.simps(1))
-
+ and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ by (lifting alphas_abs)
lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
--- a/Nominal/ExCoreHaskell.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/ExCoreHaskell.thy Mon Mar 29 00:30:47 2010 +0200
@@ -11,6 +11,7 @@
(* there are types, coercion types and regular types list-data-structure *)
+ML {* val _ = alpha_type := AlphaGen *}
nominal_datatype tkind =
KStar
| KFun "tkind" "tkind"
@@ -18,18 +19,18 @@
CKEq "ty" "ty"
and ty =
TVar "tvar"
-| TC "char"
+| TC "string"
| TApp "ty" "ty"
-| TFun "char" "ty_lst"
+| TFun "string" "ty_lst"
| TAll tv::"tvar" "tkind" T::"ty" bind tv in T
| TEq "ty" "ty" "ty"
and ty_lst =
TsNil
| TsCons "ty" "ty_lst"
and co =
- CC "char"
+ CC "string"
| CApp "co" "co"
-| CFun "char" "co_lst"
+| CFun "string" "co_lst"
| CAll tv::"tvar" "ckind" C::"co" bind tv in C
| CEq "co" "co" "co"
| CSym "co"
@@ -46,7 +47,7 @@
| CsCons "co" "co_lst"
and trm =
Var "var"
-| C "char"
+| C "string"
| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
| LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
| APP "trm" "ty"
@@ -59,7 +60,7 @@
ANil
| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
and pat =
- K "char" "tvtk_lst" "tvck_lst" "vt_lst"
+ K "string" "tvtk_lst" "tvck_lst" "vt_lst"
and vt_lst =
VTNil
| VTCons "var" "ty" "vt_lst"
@@ -141,7 +142,18 @@
apply (simp_all add: rsp_pre)
done
-lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted]
+thm permute_bv_raw.simps[no_vars]
+ permute_bv_vt_raw.simps[quot_lifted]
+ permute_bv_tvck_raw.simps[quot_lifted]
+ permute_bv_tvtk_raw.simps[quot_lifted]
+
+lemma permute_bv_pre:
+ "permute_bv p (K c l1 l2 l3) =
+ K c (permute_bv_tvtk p l1) (permute_bv_tvck p l2) (permute_bv_vt p l3)"
+ by (lifting permute_bv_raw.simps)
+
+lemmas permute_bv[simp] =
+ permute_bv_pre
permute_bv_vt_raw.simps[quot_lifted]
permute_bv_tvck_raw.simps[quot_lifted]
permute_bv_tvtk_raw.simps[quot_lifted]
@@ -318,17 +330,17 @@
and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
and a04: "\<And>tvar b. P3 b (TVar tvar)"
- and a05: "\<And>char b. P3 b (TC char)"
+ and a05: "\<And>string b. P3 b (TC string)"
and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
- and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)"
+ and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P3 b (TAll tvar tkind ty)"
and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)"
and a10: "\<And>b. P4 b TsNil"
and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"
- and a12: "\<And>char b. P5 b (CC char)"
+ and a12: "\<And>string b. P5 b (CC string)"
and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
- and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)"
+ and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P5 b (CAll tvar ckind co)"
and a16: "\<And>co1 co2 co3 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2; \<And>c. P5 c co3\<rbrakk> \<Longrightarrow> P5 b (CEq co1 co2 co3)"
@@ -343,7 +355,7 @@
and a25: "\<And>b. P6 b CsNil"
and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"
and a27: "\<And>var b. P7 b (Var var)"
- and a28: "\<And>char b. P7 b (C char)"
+ and a28: "\<And>string b. P7 b (C string)"
and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P7 b (LAMT tvar tkind trm)"
and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
@@ -358,8 +370,8 @@
and a37: "\<And>b. P8 b ANil"
and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; bv(pat) \<sharp>* b\<rbrakk>
\<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
- and a39: "\<And>char tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk>
- \<Longrightarrow> P9 b (K char tvtk_lst tvck_lst vt_lst)"
+ and a39: "\<And>string tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk>
+ \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)"
and a40: "\<And>b. P10 b VTNil"
and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)"
and a42: "\<And>b. P11 b TVTKNil"
--- a/Nominal/ExLet.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/ExLet.thy Mon Mar 29 00:30:47 2010 +0200
@@ -7,7 +7,7 @@
atom_decl name
ML {* val _ = recursive := false *}
-
+ML {* val _ = alpha_type := AlphaLst *}
nominal_datatype trm =
Vr "name"
| Ap "trm" "trm"
@@ -19,8 +19,8 @@
binder
bn
where
- "bn Lnil = {}"
-| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
+ "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
thm trm_lts.fv
thm trm_lts.eq_iff
@@ -29,7 +29,7 @@
thm trm_lts.induct[no_vars]
thm trm_lts.inducts[no_vars]
thm trm_lts.distinct
-thm trm_lts.fv[simplified trm_lts.supp]
+thm trm_lts.fv[simplified trm_lts.supp(1-2)]
primrec
permute_bn_raw
@@ -80,7 +80,7 @@
done
lemma Lt_subst:
- "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+ "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
apply (simp only: trm_lts.eq_iff)
apply (rule_tac x="q" in exI)
apply (simp add: alphas)
@@ -98,7 +98,7 @@
lemma fin_bn:
- "finite (bn l)"
+ "finite (set (bn l))"
apply(induct l rule: trm_lts.inducts(2))
apply(simp_all add:permute_bn eqvts)
done
@@ -110,7 +110,7 @@
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>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts 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"
@@ -142,14 +142,14 @@
apply(simp add: fresh_def)
apply(simp add: trm_lts.fv[simplified trm_lts.supp])
apply(simp)
- apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+ 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)
apply(subst Lt_subst)
apply assumption
apply(rule a4)
- apply(simp add:perm_bn)
- apply assumption
+ 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)
@@ -157,8 +157,6 @@
apply(rule at_set_avoiding2)
apply(rule fin_bn)
apply(simp add: finite_supp)
- apply(simp add: supp_abs)
- apply(rule finite_Diff)
apply(simp add: finite_supp)
apply(simp add: fresh_star_def fresh_def supp_abs)
apply(simp add: eqvts permute_bn)
@@ -196,12 +194,10 @@
lemma lets_not_ok1:
- "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+ "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)
- apply (rule_tac x="0::perm" in exI)
- apply (simp add: fresh_star_def eqvts)
- apply blast
+ apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
done
lemma lets_nok:
--- a/Nominal/ExLetRec.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/ExLetRec.thy Mon Mar 29 00:30:47 2010 +0200
@@ -2,11 +2,13 @@
imports "Parser"
begin
+
text {* example 3 or example 5 from Terms.thy *}
atom_decl name
ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
nominal_datatype trm =
Vr "name"
| Ap "trm" "trm"
@@ -18,8 +20,8 @@
binder
bn
where
- "bn Lnil = {}"
-| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
+ "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
thm trm_lts.fv
thm trm_lts.eq_iff
@@ -27,6 +29,7 @@
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? *)
@@ -35,14 +38,13 @@
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 (simp add: trm_lts.eq_iff alpha_gen2 set_sub)
- done
+ by (simp add: trm_lts.eq_iff alphas2 set_sub)
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: alpha_gen2 fresh_star_def eqvts)
+ apply (simp_all add: alphas2 fresh_star_def eqvts)
done
lemma lets_ok3:
@@ -67,6 +69,13 @@
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)
+ apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ apply (simp add: atom_eqvt fresh_star_def)
+ done
end
--- a/Nominal/ExTySch.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/ExTySch.thy Mon Mar 29 00:30:47 2010 +0200
@@ -5,13 +5,15 @@
(* Type Schemes *)
atom_decl name
-(*ML {* val _ = alpha_type := AlphaRes *}*)
+ML {* val _ = alpha_type := AlphaRes *}
nominal_datatype t =
Var "name"
| Fun "t" "t"
and tyS =
All xs::"name fset" ty::"t" bind xs in ty
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
+
lemma size_eqvt_raw:
"size (pi \<bullet> t :: t_raw) = size t"
"size (pi \<bullet> ts :: tyS_raw) = size ts"
@@ -69,8 +71,6 @@
thm t_tyS.distinct
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
-
lemma induct:
assumes a1: "\<And>name b. P b (Var name)"
and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
@@ -120,7 +120,6 @@
apply(simp add: t_tyS.eq_iff)
apply(rule_tac x="0::perm" in exI)
apply(simp add: alphas)
- apply(auto)
apply(simp add: fresh_star_def fresh_zero_perm)
done
@@ -128,16 +127,15 @@
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
apply(simp add: t_tyS.eq_iff)
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: alpha_gen fresh_star_def eqvts)
- apply auto
+ apply(simp add: alphas fresh_star_def eqvts)
done
lemma
shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
apply(simp add: t_tyS.eq_iff)
apply(rule_tac x="0::perm" in exI)
- apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
-oops
+ apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
+done
lemma
assumes a: "a \<noteq> b"
@@ -145,7 +143,7 @@
using a
apply(simp add: t_tyS.eq_iff)
apply(clarify)
- apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
+ apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
apply auto
done
--- a/Nominal/FSet.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/FSet.thy Mon Mar 29 00:30:47 2010 +0200
@@ -424,4 +424,7 @@
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
*}
+no_notation
+ list_eq (infix "\<approx>" 50)
+
end
--- a/Nominal/Fv.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Fv.thy Mon Mar 29 00:30:47 2010 +0200
@@ -409,6 +409,12 @@
length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1
*}
+ML {*
+fun setify x =
+ if fastype_of x = @{typ "atom list"} then
+ Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
+*}
+
(* TODO: Notice datatypes without bindings and replace alpha with equality *)
ML {*
fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
@@ -439,6 +445,7 @@
alpha_bns dt_info alpha_frees bns bns_rec
val alpha_bn_frees = map snd bn_alpha_bns;
val alpha_bn_types = map fastype_of alpha_bn_frees;
+
fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -464,8 +471,9 @@
if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
(* TODO we do not know what to do with non-atomizable things *)
@{term "{} :: atom set"}
- | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i);
+ | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i)
fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
+ fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant)
fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE
| find_nonrec_binder _ _ = NONE
fun fv_arg ((dt, x), arg_no) =
@@ -485,7 +493,7 @@
@{term "{} :: atom set"};
(* If i = j then we generate it only once *)
val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs;
- val sub = fv_binds args relevant
+ val sub = fv_binds_as_set args relevant
in
mk_diff arg sub
end;
@@ -883,20 +891,46 @@
end
*}
-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
+(* TODO: this is a hack, it assumes that only one type of Abs's is present
+ in the type and chooses this supp_abs. Additionally single atoms are
+ treated properly. *)
+ML {*
+fun choose_alpha_abs eqiff =
+let
+ fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
+ val terms = map prop_of eqiff;
+ fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
+ val no =
+ if check @{const_name alpha_lst} then 2 else
+ if check @{const_name alpha_res} then 1 else
+ if check @{const_name alpha_gen} then 0 else
+ error "Failure choosing supp_abs"
+in
+ nth @{thms supp_abs[symmetric]} no
+end
+*}
+lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
+by (rule supp_abs(1))
+
+lemma supp_abs_sum:
+ "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+ "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+ "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
+ apply (simp_all add: supp_abs supp_Pair)
+ apply blast+
done
+
ML {*
fun supp_eq_tac ind fv perm eqiff ctxt =
rel_indtac ind THEN_ALL_NEW
asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
@@ -918,7 +952,7 @@
val typ = domain_type (fastype_of fnctn);
val arg = the (AList.lookup (op=) frees typ);
in
- ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+ ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
end
*}
@@ -927,7 +961,7 @@
let
val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
val pi = Free (pi, @{typ perm});
- val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt'))
+ val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
val ths = Variable.export ctxt' ctxt ths_loc
val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
--- a/Nominal/Lift.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Lift.thy Mon Mar 29 00:30:47 2010 +0200
@@ -2,14 +2,20 @@
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
begin
+
ML {*
-fun define_quotient_type args tac ctxt =
+fun define_quotient_types binds tys alphas equivps ctxt =
let
- val mthd = Method.SIMPLE_METHOD tac
- val mthdt = Method.Basic (fn _ => mthd)
- val bymt = Proof.global_terminal_proof (mthdt, NONE)
+ fun def_ty ((b, ty), (alpha, equivp)) ctxt =
+ Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha)), equivp) ctxt;
+ val alpha_equivps = List.take (equivps, length alphas)
+ val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
+ val quot_thms = map fst thms;
+ val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms;
+ val reps = map (hd o rev o snd o strip_comb) quots;
+ val qtys = map (domain_type o fastype_of) reps;
in
- bymt (Quotient_Type.quotient_type args ctxt)
+ (qtys, ctxt')
end
*}
@@ -49,24 +55,11 @@
*}
ML {*
-fun lift_thm ctxt thm =
+fun lift_thm qtys ctxt thm =
let
val un_raw_names = rename_vars un_raws
in
- rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))))
-end
-*}
-
-ML {*
-fun quotient_lift_consts_export spec ctxt =
-let
- val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;
- val (ts_loc, defs_loc) = split_list result;
- val morphism = ProofContext.export_morphism ctxt' ctxt;
- val ts = map (Morphism.term morphism) ts_loc
- val defs = Morphism.fact morphism defs_loc
-in
- (ts, defs, ctxt')
+ rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm))
end
*}
--- a/Nominal/Nominal2_FSet.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy Mon Mar 29 00:30:47 2010 +0200
@@ -3,7 +3,7 @@
begin
lemma permute_rsp_fset[quot_respect]:
- "(op = ===> op \<approx> ===> op \<approx>) permute permute"
+ "(op = ===> list_eq ===> list_eq) permute permute"
apply (simp add: eqvts[symmetric])
apply clarify
apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
@@ -44,7 +44,7 @@
end
-lemma permute_fset[simp,eqvt]:
+lemma permute_fset[eqvt]:
"p \<bullet> ({||} :: 'a :: pt fset) = {||}"
"p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
by (lifting permute_list.simps)
--- a/Nominal/Parser.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Parser.thy Mon Mar 29 00:30:47 2010 +0200
@@ -157,22 +157,18 @@
*}
ML {*
-fun strip_union t =
+fun strip_bn_fun t =
case t of
- Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r
- | (h as (Const (@{const_name insert}, T))) $ x $ y =>
- (h $ x $ Const (@{const_name bot}, range_type (range_type T))) :: strip_union y
+ Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+ | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+ | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+ (i, NONE) :: strip_bn_fun y
+ | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+ (i, NONE) :: strip_bn_fun y
| Const (@{const_name bot}, _) => []
- | _ => [t]
-*}
-
-ML {*
-fun bn_or_atom t =
- case t of
- Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $
- Const (@{const_name bot}, _) => (i, NONE)
- | f $ Bound i => (i, SOME f)
- | _ => error "Unsupported binding function"
+ | Const (@{const_name Nil}, _) => []
+ | (f as Free _) $ Bound i => [(i, SOME f)]
+ | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
*}
ML {*
@@ -189,7 +185,7 @@
val (ty_name, _) = dest_Type (domain_type ty)
val dt_index = find_index (fn x => x = ty_name) dt_names
val (cnstr_head, cnstr_args) = strip_comb cnstr
- val rhs_elements = map bn_or_atom (strip_union rhs)
+ val rhs_elements = strip_bn_fun rhs
val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
in
(dt_index, (bn_fun, (cnstr_head, included)))
@@ -357,7 +353,6 @@
val distincts = flat (map #distinct dtinfos);
val rel_distinct = map #distinct rel_dtinfos;
val induct = #induct dtinfo;
- val inducts = #inducts dtinfo;
val exhausts = map #exhaust dtinfos;
val _ = tracing "Defining permutations, fv and alpha";
val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
@@ -395,60 +390,57 @@
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
- val lthy7 = define_quotient_type
- (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
- (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
+ val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
val raw_consts =
flat (map (fn (i, (_, _, l)) =>
map (fn (cname, dts) =>
Const (cname, map (typ_of_dtyp descr sorts) dts --->
typ_of_dtyp descr sorts (DtRec i))) l) descr);
- val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7;
- (* Could be done nicer *)
- val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
+ val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
val _ = tracing "Proving respects";
val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
+ val _ = map tracing (map PolyML.makestring bns_rsp_pre')
val (bns_rsp_pre, lthy9) = fold_map (
- fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
+ fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
resolve_tac bns_rsp_pre' 1)) bns lthy8;
val bns_rsp = flat (map snd bns_rsp_pre);
fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
val (fv_rsp_pre, lthy10) = fold_map
- (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv]
+ (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
(fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9;
val fv_rsp = flat (map snd fv_rsp_pre);
- val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
+ val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
(fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;
- val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+ val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
(fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11
(* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*)
fun const_rsp_tac _ =
if !cheat_const_rsp then Skip_Proof.cheat_tac thy
else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
- val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+ val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
const_rsp_tac) raw_consts lthy11a
val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
- val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
+ val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12;
val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
- val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
+ val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
- val (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+ val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
val _ = tracing "Lifting permutations";
val thy = Local_Theory.exit_global lthy12c;
val perm_names = map (fn x => "permute_" ^ x) qty_names
- val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
+ val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
val lthy13 = Theory_Target.init NONE thy';
val q_name = space_implode "_" qty_names;
fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
val _ = tracing "Lifting induction";
val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
- val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct);
+ val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
fun note_suffix s th ctxt =
snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
fun note_simp_suffix s th ctxt =
@@ -457,27 +449,27 @@
[Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
- val q_perm = map (lift_thm lthy14) raw_perm_def;
+ val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
- val q_fv = map (lift_thm lthy15) fv_def;
+ val q_fv = map (lift_thm qtys lthy15) fv_def;
val lthy16 = note_simp_suffix "fv" q_fv lthy15;
- val q_bn = map (lift_thm lthy16) raw_bn_eqs;
+ val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = tracing "Lifting eq-iff";
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff
val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1
- val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
+ val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
- val q_dis = map (lift_thm lthy18) rel_dists;
+ val q_dis = map (lift_thm qtys lthy18) rel_dists;
val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
- val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt);
+ val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
val (_, lthy20) = Local_Theory.note ((Binding.empty,
[Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
val _ = tracing "Finite Support";
val supports = map (prove_supports lthy20 q_perm) consts;
- val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
+ val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
val thy3 = Local_Theory.exit_global lthy20;
val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
@@ -602,7 +594,7 @@
end
in
- map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
+ map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
(map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
end
*}
--- a/Nominal/Perm.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Perm.thy Mon Mar 29 00:30:47 2010 +0200
@@ -9,6 +9,19 @@
*}
ML {*
+fun quotient_lift_consts_export qtys spec ctxt =
+let
+ val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
+ val (ts_loc, defs_loc) = split_list result;
+ val morphism = ProofContext.export_morphism ctxt' ctxt;
+ val ts = map (Morphism.term morphism) ts_loc
+ val defs = Morphism.fact morphism defs_loc
+in
+ (ts, defs, ctxt')
+end
+*}
+
+ML {*
fun prove_perm_empty lthy induct perm_def perm_frees =
let
val perm_types = map fastype_of perm_frees;
@@ -118,12 +131,12 @@
*}
ML {*
-fun define_lifted_perms full_tnames name_term_pairs thms thy =
+fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
let
val lthy =
Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
- val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
- val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms
+ val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
+ val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
fun tac _ =
Class.intro_classes_tac [] THEN
(ALLGOALS (resolve_tac lifted_thms))
--- a/Nominal/Rsp.thy Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Rsp.thy Mon Mar 29 00:30:47 2010 +0200
@@ -3,9 +3,9 @@
begin
ML {*
-fun const_rsp lthy const =
+fun const_rsp qtys lthy const =
let
- val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
+ val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy)
val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
in
HOLogic.mk_Trueprop (rel $ const $ const)
@@ -39,9 +39,9 @@
*}
ML {*
-fun prove_const_rsp bind consts tac ctxt =
+fun prove_const_rsp qtys bind consts tac ctxt =
let
- val rsp_goals = map (const_rsp ctxt) consts
+ val rsp_goals = map (const_rsp qtys ctxt) consts
val thy = ProofContext.theory_of ctxt
val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
val fixed' = distinct (op =) (flat fixed)
@@ -94,8 +94,6 @@
in
Const (@{const_name permute}, @{typ perm} --> ty --> ty)
end
-
-val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
*}
lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
--- a/TODO Mon Mar 29 00:30:20 2010 +0200
+++ b/TODO Mon Mar 29 00:30:47 2010 +0200
@@ -42,3 +42,7 @@
- fv_rsp uses 'blast' to show goals of the type:
a u b = c u d ==> a u x u b = c u x u d
+
+When cleaning:
+
+- remove all 'PolyML.makestring'.
\ No newline at end of file