--- a/Nominal/Equivp.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Equivp.thy Tue May 04 05:36:55 2010 +0100
@@ -1,5 +1,5 @@
theory Equivp
-imports "NewFv" "Tacs" "Rsp" "NewFv"
+imports "NewFv" "Tacs" "Rsp"
begin
ML {*
--- a/Nominal/Ex/Classical.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Ex/Classical.thy Tue May 04 05:36:55 2010 +0100
@@ -12,6 +12,10 @@
atom_decl name
atom_decl coname
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+ML {* val _ = cheat_fv_rsp := true *}
+
nominal_datatype trm =
Ax "name" "coname"
| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
--- a/Nominal/Ex/Ex2.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Ex/Ex2.thy Tue May 04 05:36:55 2010 +0100
@@ -1,35 +1,31 @@
theory Ex2
-imports "../Parser"
+imports "../NewParser"
begin
text {* example 2 *}
atom_decl name
-ML {* val _ = recursive := false *}
-nominal_datatype trm' =
+nominal_datatype trm =
Var "name"
-| App "trm'" "trm'"
-| Lam x::"name" t::"trm'" bind x in t
-| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t
-and pat' =
+| 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"
+ f::"pat \<Rightarrow> atom set"
where
"f PN = {}"
| "f (PD x y) = {atom x, atom y}"
| "f (PS x) = {atom x}"
-
-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]
+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 Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Ex/Ex3.thy Tue May 04 05:36:55 2010 +0100
@@ -1,35 +1,34 @@
theory Ex3
-imports "../Parser"
+imports "../NewParser"
begin
(* Example 3, identical to example 1 from Terms.thy *)
atom_decl name
-ML {* val _ = recursive := false *}
-nominal_datatype trm0 =
- Var0 "name"
-| App0 "trm0" "trm0"
-| Lam0 x::"name" t::"trm0" bind x in t
-| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t
-and pat0 =
- PN0
-| PS0 "name"
-| PD0 "pat0" "pat0"
+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
- f0::"pat0 \<Rightarrow> atom set"
+ f::"pat \<Rightarrow> atom set"
where
- "f0 PN0 = {}"
-| "f0 (PS0 x) = {atom x}"
-| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
+ "f PN = {}"
+| "f (PS x) = {atom x}"
+| "f (PD p1 p2) = (f p1) \<union> (f p2)"
-thm trm0_pat0.fv
-thm trm0_pat0.eq_iff
-thm trm0_pat0.bn
-thm trm0_pat0.perm
-thm trm0_pat0.induct
-thm trm0_pat0.distinct
-thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
+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/SingleLet.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy Tue May 04 05:36:55 2010 +0100
@@ -1,16 +1,14 @@
theory SingleLet
-imports "../Parser"
+imports "../NewParser"
begin
atom_decl name
-ML {* val _ = recursive := false *}
-
nominal_datatype trm =
Var "name"
| App "trm" "trm"
-| Lam x::"name" t::"trm" bind x in t
-| Let a::"assg" t::"trm" bind "bn a" in t
+| Lam x::"name" t::"trm" bind_set x in t
+| Let a::"assg" t::"trm" bind_set "bn a" in t
and assg =
As "name" "trm"
binder
@@ -18,19 +16,23 @@
where
"bn (As x t) = {atom x}"
-print_theorems
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
thm trm_assg.fv
thm trm_assg.supp
-thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]
+thm trm_assg.eq_iff
thm trm_assg.bn
thm trm_assg.perm
thm trm_assg.induct
thm trm_assg.inducts
thm trm_assg.distinct
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
-thm trm_assg.fv[simplified trm_assg.supp]
+thm trm_assg.fv[simplified trm_assg.supp(1-2)]
+
+(*
+setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+declare permute_trm_raw_permute_assg_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_trm_raw
+*)
end
--- a/Nominal/Fv.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Fv.thy Tue May 04 05:36:55 2010 +0100
@@ -650,4 +650,29 @@
end
*}
+
+ML {*
+fun define_fv_alpha_export dt binds bns ctxt =
+let
+ val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
+ define_fv dt binds bns ctxt;
+ val (alpha, ctxt'') =
+ define_alpha dt binds bns fv_ts_loc ctxt';
+ val alpha_ts_loc = #preds alpha
+ val alpha_induct_loc = #induct alpha
+ val alpha_intros_loc = #intrs alpha;
+ val alpha_cases_loc = #elims alpha
+ val morphism = ProofContext.export_morphism ctxt'' ctxt;
+ val fv_ts = map (Morphism.term morphism) fv_ts_loc;
+ val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
+ val fv_def = Morphism.fact morphism fv_def_loc;
+ val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
+ val alpha_induct = Morphism.thm morphism alpha_induct_loc;
+ val alpha_intros = Morphism.fact morphism alpha_intros_loc
+ val alpha_cases = Morphism.fact morphism alpha_cases_loc
+in
+ ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
+end;
+*}
+
end
--- a/Nominal/Lift.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Lift.thy Tue May 04 05:36:55 2010 +0100
@@ -1,8 +1,8 @@
theory Lift
-imports "../Nominal-General/Nominal2_Atoms"
- "../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
- "Abs" "Perm" "Equivp" "Rsp" "Attic/Fv"
+imports "../Nominal-General/Nominal2_Atoms"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
+ "Abs" "Perm" "Equivp" "Rsp"
begin
@@ -66,32 +66,5 @@
end
*}
-
-
-
-ML {*
-fun define_fv_alpha_export dt binds bns ctxt =
-let
- val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
- define_fv dt binds bns ctxt;
- val (alpha, ctxt'') =
- define_alpha dt binds bns fv_ts_loc ctxt';
- val alpha_ts_loc = #preds alpha
- val alpha_induct_loc = #induct alpha
- val alpha_intros_loc = #intrs alpha;
- val alpha_cases_loc = #elims alpha
- val morphism = ProofContext.export_morphism ctxt'' ctxt;
- val fv_ts = map (Morphism.term morphism) fv_ts_loc;
- val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
- val fv_def = Morphism.fact morphism fv_def_loc;
- val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
- val alpha_induct = Morphism.thm morphism alpha_induct_loc;
- val alpha_intros = Morphism.fact morphism alpha_intros_loc
- val alpha_cases = Morphism.fact morphism alpha_cases_loc
-in
- ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
-end;
-*}
-
end
--- a/Nominal/NewParser.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/NewParser.thy Tue May 04 05:36:55 2010 +0100
@@ -159,8 +159,9 @@
end
*}
-text {* What does the prep_bn code do? Cezary's Function? *}
-
+(* strip_bn_fun takes a bn function defined by the user as a union or
+ append of elements and returns those elements together with bn functions
+ applied *)
ML {*
fun strip_bn_fun t =
case t of
@@ -258,6 +259,31 @@
end
*}
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+ val thy = ProofContext.theory_of ctxt
+ val ty = domain_type (fastype_of rel)
+ val cty = ctyp_of thy ty
+ val ct = cterm_of thy rel
+in
+ Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_equivp = Unsynchronized.ref false *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
+ML {* val cheat_supp_eq = Unsynchronized.ref false *}
+
+ML {*
+fun remove_loop t =
+ let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end
+ handle TERM _ => @{thm eqTrueI} OF [t]
+*}
text {*
nominal_datatype2 does the following things in order:
@@ -335,7 +361,7 @@
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
val {descr, sorts, ...} = dtinfo;
val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
- val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+ val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
@@ -380,21 +406,26 @@
(* definition of raw_alpha_eq_iff lemmas *)
val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
-
+ val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
+ val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
+
(* proving equivariance lemmas *)
val _ = warning "Proving equivariance";
val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
- fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
+ fun alpha_eqvt_tac' _ =
+ if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
+ else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
(* provind alpha equivalence *)
val _ = warning "Proving equivalence";
val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
- val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
+ val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff_simp lthy6;
val alpha_equivp =
- build_equivps alpha_ts reflps alpha_induct
- inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+ if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+ else build_equivps alpha_ts reflps alpha_induct
+ inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6;
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
@@ -403,8 +434,8 @@
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);
+ Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
val _ = warning "Proving respects";
val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
@@ -412,8 +443,9 @@
fn (bn_t, _) => 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);
- (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
- fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
+
+ 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 qtys Binding.empty [fv]
@@ -421,11 +453,14 @@
val fv_rsp = flat (map snd fv_rsp_pre);
val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
(fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+ fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
+ else
+ let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
- (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
+ alpha_bn_rsp_tac) alpha_ts_bn lthy11
fun const_rsp_tac _ =
- 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
+ let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
+ in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
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) (fv @ fvbn)
@@ -463,7 +498,7 @@
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = warning "Lifting eq-iff";
(*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
- val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+ val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
@@ -487,7 +522,10 @@
val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
val (names, supp_eq_t) = supp_eq fv_alpha_all;
val _ = warning "Support Equations";
- val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+ fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
+ supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
+ val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
+ let val _ = warning ("Support eqs failed") in [] end;
val lthy23 = note_suffix "supp" q_supp lthy22;
in
(0, lthy23)
@@ -660,7 +698,7 @@
(main_parser >> nominal_datatype2_cmd)
*}
-atom_decl name
+(*atom_decl name
nominal_datatype lam =
Var name
@@ -740,7 +778,7 @@
thm ty_tys.fv[simplified ty_tys.supp]
thm ty_tys.eq_iff
-
+*)
(* some further tests *)
--- a/Nominal/Parser.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Parser.thy Tue May 04 05:36:55 2010 +0100
@@ -1,8 +1,8 @@
theory Parser
-imports "../Nominal-General/Nominal2_Atoms"
- "../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
- "Perm" "Equivp" "Rsp" "Lift"
+imports "../Nominal-General/Nominal2_Atoms"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
+ "Perm" "Equivp" "Rsp" "Lift" "Fv"
begin
section{* Interface for nominal_datatype *}
@@ -372,9 +372,9 @@
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
val {descr, sorts, ...} = dtinfo;
- fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+ fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i);
val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
- val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+ val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
val rel_dtinfos = List.take (dtinfos, (length dts));
@@ -423,8 +423,8 @@
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);
+ Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
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;
@@ -483,7 +483,7 @@
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 _ = map tracing (map PolyML.makestring alpha_eq_iff);
+(* val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
--- a/Nominal/Rsp.thy Tue May 04 05:36:43 2010 +0100
+++ b/Nominal/Rsp.thy Tue May 04 05:36:55 2010 +0100
@@ -97,7 +97,7 @@
ML {*
fun alpha_eqvt_tac induct simps ctxt =
rel_indtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps