diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Nominal2.thy --- 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)