--- a/Nominal/Nominal2.thy Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Nominal2.thy Mon Dec 06 14:24:17 2010 +0000
@@ -146,13 +146,9 @@
ML {*
(** definition of the raw binding functions **)
-(* TODO: needs cleaning *)
-fun find [] _ = error ("cannot find element")
- | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
-
-fun prep_bn_info lthy dt_names dts eqs =
+fun prep_bn_info lthy dt_names dts bn_funs eqs =
let
- fun aux eq =
+ fun process_eq eq =
let
val (lhs, rhs) = eq
|> HOLogic.dest_Trueprop
@@ -162,32 +158,32 @@
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 cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))
val rhs_elements = strip_bn_fun lthy cnstr_args rhs
in
- (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
+ ((bn_fun, dt_index), (cnstr_name, rhs_elements))
end
- fun order dts i ts =
+ (* order according to constructor names *)
+ fun cntrs_order ((bn, dt_index), data) =
let
- val dt = nth dts i
- val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
- val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
+ val dt = nth dts dt_index
+ val cts = (fn (_, _, _, x) => x) dt
+ val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts
in
- map (find ts') cts
+ (bn, (bn, dt_index, order (op=) ct_names data))
end
+
+in
+ eqs
+ |> map process_eq
+ |> AList.group (op=) (* eqs grouped according to bn_functions *)
+ |> map cntrs_order (* inner data ordered according to constructors *)
+ |> order (op=) bn_funs (* ordered according to bn_functions *)
+end
+*}
- val unordered = AList.group (op=) (map aux eqs)
- val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered
- val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered'
- val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
-
- (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*)
- (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
- (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
-in
- ordered'
-end
-
+ML {*
fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
if null raw_bn_funs
then ([], [], [], [], lthy)
@@ -203,7 +199,7 @@
val raw_bn_eqs = the simps
val raw_bn_info =
- prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+ prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
in
(fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
end
@@ -269,6 +265,8 @@
then define_raw_dts dts bn_funs bn_eqs bclauses lthy
else raise TEST lthy
+ val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs))
+
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
val {descr, sorts, ...} = dtinfo
@@ -311,6 +309,12 @@
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
else raise TEST lthy3
+ (*
+ val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns))
+ val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info))
+ val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info))
+ *)
+
(* defining the permute_bn functions *)
val (raw_perm_bns, raw_perm_bn_simps, lthy3b) =
if get_STEPS lthy3a > 2
@@ -489,6 +493,14 @@
val qalpha_bns_descr =
map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms
+ (*
+ val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info))
+ val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs))
+ val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns))
+ val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns))
+ val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms))
+ *)
+
val qperm_descr =
map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
@@ -499,7 +511,7 @@
map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
- val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) =
+ val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)=
if get_STEPS lthy > 24
then
lthy7
@@ -527,6 +539,7 @@
val qfvs = map #qconst qfvs_info
val qfv_bns = map #qconst qfv_bns_info
val qalpha_bns = map #qconst qalpha_bns_info
+ val qperm_bns = map #qconst qperm_bns_info
(* lifting of the theorems *)
val _ = warning "Lifting of Theorems"
@@ -586,12 +599,6 @@
qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
else []
- (* proving that the qbn result is finite *)
- val qbn_finite_thms =
- if get_STEPS lthy > 33
- then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
- else []
-
(* postprocessing of eq and fv theorems *)
val qeq_iffs' = qeq_iffs
@@ -612,6 +619,18 @@
|> map (fn thm => thm RS transform_thm)
|> map (simplify (HOL_basic_ss addsimps transform_thms))
+ (* proving that the qbn result is finite *)
+ val qbn_finite_thms =
+ if get_STEPS lthy > 33
+ then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
+ else []
+
+ (* proving that perm_bns preserve alpha *)
+ val qperm_bn_alpha_thms = @{thms TrueI}
+ (* if get_STEPS lthy > 33
+ then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC
+ else []*)
+
(* noting the theorems *)
@@ -639,6 +658,7 @@
||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
+ ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
in
(0, lthy9')
end handle TEST ctxt => (0, ctxt)