--- a/Nominal/NewParser.thy Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/NewParser.thy Fri May 21 05:58:23 2010 +0100
@@ -185,7 +185,7 @@
*}
ML {*
-fun prep_bn lthy dt_names dts eqs =
+fun prep_bn_descr lthy dt_names dts eqs =
let
fun aux eq =
let
@@ -252,16 +252,16 @@
val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
- val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
+ val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
- val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+ val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
- val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
+ val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr;
in
- (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2)
+ (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy2)
end
*}
@@ -290,70 +290,6 @@
handle TERM _ => @{thm eqTrueI} OF [t]
*}
-text {*
- nominal_datatype2 does the following things in order:
-
-Parser.thy/raw_nominal_decls
- 1) define the raw datatype
- 2) define the raw binding functions
-
-Perm.thy/define_raw_perms
- 3) define permutations of the raw datatype and show that the raw type is
- in the pt typeclass
-
-Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
- 4) define fv and fv_bn
- 5) define alpha and alpha_bn
-
-Perm.thy/distinct_rel
- 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp)
-
-Tacs.thy/build_rel_inj
- 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...)
- (left-to-right by intro rule, right-to-left by cases; simp)
-Equivp.thy/prove_eqvt
- 7) prove bn_eqvt (common induction on the raw datatype)
- 8) prove fv_eqvt (common induction on the raw datatype with help of above)
-Rsp.thy/build_alpha_eqvts
- 9) prove alpha_eqvt and alpha_bn_eqvt
- (common alpha-induction, unfolding alpha_gen, permute of #* and =)
-Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
- 10) prove that alpha and alpha_bn are equivalence relations
- (common induction and application of 'compose' lemmas)
-Lift.thy/define_quotient_types
- 11) define quotient types
-Rsp.thy/build_fvbv_rsps
- 12) prove bn respects (common induction and simp with alpha_gen)
-Rsp.thy/prove_const_rsp
- 13) prove fv respects (common induction and simp with alpha_gen)
- 14) prove permute respects (unfolds to alpha_eqvt)
-Rsp.thy/prove_alpha_bn_rsp
- 15) prove alpha_bn respects
- (alpha_induct then cases then sym and trans of the relations)
-Rsp.thy/prove_alpha_alphabn
- 16) show that alpha implies alpha_bn (by unduction, needed in following step)
-Rsp.thy/prove_const_rsp
- 17) prove respects for all datatype constructors
- (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
-Perm.thy/quotient_lift_consts_export
- 18) define lifted constructors, fv, bn, alpha_bn, permutations
-Perm.thy/define_lifted_perms
- 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
-Lift.thy/lift_thm
- 20) lift permutation simplifications
- 21) lift induction
- 22) lift fv
- 23) lift bn
- 24) lift eq_iff
- 25) lift alpha_distincts
- 26) lift fv and bn eqvts
-Equivp.thy/prove_supports
- 27) prove that union of arguments supports constructors
-Equivp.thy/prove_fs
- 28) show that the lifted type is in fs typeclass (* by q_induct, supports *)
-Equivp.thy/supp_eq
- 29) prove supp = fv
-*}
ML {*
(* for testing porposes - to exit the procedure early *)
@@ -370,12 +306,17 @@
fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
let
(* definition of the raw datatypes and raw bn-functions *)
- val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) =
+ val (raw_dt_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_funs, raw_bn_eqs, raw_bn_descr, raw_bn_descr2, lthy1) =
if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
else raise TEST lthy
- (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*)
- (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*)
+ val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr)
+ val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2)
+ val _ = tracing ("bclauses " ^ @{make_string} bclauses)
+ val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs)
+ val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs)
+ val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2)
+ val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2))
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
val {descr, sorts, ...} = dtinfo
@@ -391,7 +332,7 @@
val exhaust_thms = map #exhaust dtinfos;
(* definitions of raw permutations *)
- val ((perms, raw_perm_defs, raw_perm_simps), lthy2) =
+ val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
if get_STEPS lthy1 > 2
then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
else raise TEST lthy1
@@ -405,22 +346,22 @@
(* definition of raw fv_functions *)
val lthy3 = Theory_Target.init NONE thy;
- val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
val (fv, fvbn, fv_def, lthy3a) =
if get_STEPS lthy2 > 3
- then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3
+ then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) bn_funs) (map snd bn_eqs) descr sorts raw_bn_descr raw_bn_descr2 raw_bclauses lthy3
else raise TEST lthy3
+
(* definition of raw alphas *)
val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
if get_STEPS lthy > 4
- then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a
+ then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a
else raise TEST lthy3a
val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
- val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
+ val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
val bns = raw_bn_funs ~~ bn_nos;
@@ -433,8 +374,6 @@
val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) 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 all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
@@ -474,7 +413,7 @@
(fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
(fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
val fv_rsp = flat (map snd fv_rsp_pre);
- val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
+ val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
(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
@@ -488,7 +427,7 @@
const_rsp_tac) raw_consts lthy11a
val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
- val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
+ val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
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
@@ -497,7 +436,7 @@
val _ = warning "Lifting permutations";
val thy = Local_Theory.exit_global lthy12c;
val perm_names = map (fn x => "permute_" ^ x) qty_names
- val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
+ val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) 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);
@@ -717,108 +656,71 @@
(main_parser >> nominal_datatype2_cmd)
*}
-(*
-atom_decl name
+
+text {*
+ nominal_datatype2 does the following things in order:
-nominal_datatype lam =
- Var name
-| App lam lam
-| Lam x::name t::lam bind_set x in t
-| Let p::pt t::lam bind_set "bn p" in t
-and pt =
- P1 name
-| P2 pt pt
-binder
- bn::"pt \<Rightarrow> atom set"
-where
- "bn (P1 x) = {atom x}"
-| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
-
-find_theorems Var_raw
-
-
+Parser.thy/raw_nominal_decls
+ 1) define the raw datatype
+ 2) define the raw binding functions
-thm lam_pt.bn
-thm lam_pt.fv[simplified lam_pt.supp(1-2)]
-thm lam_pt.eq_iff
-thm lam_pt.induct
-thm lam_pt.perm
-
-nominal_datatype exp =
- EVar name
-| EUnit
-| EPair q1::exp q2::exp
-| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l
+Perm.thy/define_raw_perms
+ 3) define permutations of the raw datatype and show that the raw type is
+ in the pt typeclass
+
+Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
+ 4) define fv and fv_bn
+ 5) define alpha and alpha_bn
-and fnclause =
- K x::name p::pat f::exp bind_res "b_pat p" in f
-
-and fnclauses =
- S fnclause
-| ORs fnclause fnclauses
-
-and lrb =
- Clause fnclauses
-
-and lrbs =
- Single lrb
-| More lrb lrbs
+Perm.thy/distinct_rel
+ 6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...) (Proof by cases; simp)
-and pat =
- PVar name
-| PUnit
-| PPair pat pat
-
-binder
- b_lrbs :: "lrbs \<Rightarrow> atom list" and
- b_pat :: "pat \<Rightarrow> atom set" and
- b_fnclauses :: "fnclauses \<Rightarrow> atom list" and
- b_fnclause :: "fnclause \<Rightarrow> atom list" and
- b_lrb :: "lrb \<Rightarrow> atom list"
-
-where
- "b_lrbs (Single l) = b_lrb l"
-| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)"
-| "b_pat (PVar x) = {atom x}"
-| "b_pat (PUnit) = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)"
-| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp) = [atom x]"
-
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm
-
-nominal_datatype ty =
- Vr "name"
-| Fn "ty" "ty"
-and tys =
- Al xs::"name fset" t::"ty" bind_res xs in t
-
-thm ty_tys.fv[simplified ty_tys.supp]
-thm ty_tys.eq_iff
-
-*)
-
-(* some further tests *)
-
-(*
-nominal_datatype ty2 =
- Vr2 "name"
-| Fn2 "ty2" "ty2"
-
-nominal_datatype tys2 =
- All2 xs::"name fset" ty::"ty2" bind_res xs in ty
-
-nominal_datatype lam2 =
- Var2 "name"
-| App2 "lam2" "lam2 list"
-| Lam2 x::"name" t::"lam2" bind x in t
-*)
+Tacs.thy/build_rel_inj
+ 6) prove alpha_eq_iff (C1 x = C2 y \<leftrightarrow> P x y ...)
+ (left-to-right by intro rule, right-to-left by cases; simp)
+Equivp.thy/prove_eqvt
+ 7) prove bn_eqvt (common induction on the raw datatype)
+ 8) prove fv_eqvt (common induction on the raw datatype with help of above)
+Rsp.thy/build_alpha_eqvts
+ 9) prove alpha_eqvt and alpha_bn_eqvt
+ (common alpha-induction, unfolding alpha_gen, permute of #* and =)
+Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
+ 10) prove that alpha and alpha_bn are equivalence relations
+ (common induction and application of 'compose' lemmas)
+Lift.thy/define_quotient_types
+ 11) define quotient types
+Rsp.thy/build_fvbv_rsps
+ 12) prove bn respects (common induction and simp with alpha_gen)
+Rsp.thy/prove_const_rsp
+ 13) prove fv respects (common induction and simp with alpha_gen)
+ 14) prove permute respects (unfolds to alpha_eqvt)
+Rsp.thy/prove_alpha_bn_rsp
+ 15) prove alpha_bn respects
+ (alpha_induct then cases then sym and trans of the relations)
+Rsp.thy/prove_alpha_alphabn
+ 16) show that alpha implies alpha_bn (by unduction, needed in following step)
+Rsp.thy/prove_const_rsp
+ 17) prove respects for all datatype constructors
+ (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
+Perm.thy/quotient_lift_consts_export
+ 18) define lifted constructors, fv, bn, alpha_bn, permutations
+Perm.thy/define_lifted_perms
+ 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
+Lift.thy/lift_thm
+ 20) lift permutation simplifications
+ 21) lift induction
+ 22) lift fv
+ 23) lift bn
+ 24) lift eq_iff
+ 25) lift alpha_distincts
+ 26) lift fv and bn eqvts
+Equivp.thy/prove_supports
+ 27) prove that union of arguments supports constructors
+Equivp.thy/prove_fs
+ 28) show that the lifted type is in fs typeclass (* by q_induct, supports *)
+Equivp.thy/supp_eq
+ 29) prove supp = fv
+*}