--- a/Nominal/NewParser.thy Fri May 21 11:40:18 2010 +0100
+++ b/Nominal/NewParser.thy Sat May 22 13:51:47 2010 +0100
@@ -165,18 +165,23 @@
appends of elements; in case of recursive calls it retruns also the applied
bn function *)
ML {*
-fun strip_bn_fun t =
- case t of
- 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}, _) => []
- | Const (@{const_name Nil}, _) => []
- | (f as Free _) $ Bound i => [(i, SOME f)]
- | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
+fun strip_bn_fun lthy args t =
+let
+ fun aux t =
+ case t of
+ Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
+ | Const (@{const_name append}, _) $ l $ r => aux l @ aux r
+ | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+ (find_index (equal x) args, NONE) :: aux y
+ | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+ (find_index (equal x) args, NONE) :: aux y
+ | Const (@{const_name bot}, _) => []
+ | Const (@{const_name Nil}, _) => []
+ | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]
+ | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))
+in
+ aux t
+end
*}
ML {*
@@ -190,15 +195,14 @@
fun aux eq =
let
val (lhs, rhs) = eq
- |> strip_qnt_body "all"
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq
val (bn_fun, [cnstr]) = strip_comb lhs
- val (_, ty) = dest_Free bn_fun
+ val (_, ty) = dest_Const bn_fun
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 = strip_bn_fun rhs
+ val (cnstr_head, cnstr_args) = strip_comb cnstr
+ val rhs_elements = strip_bn_fun lthy cnstr_args rhs
val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
in
(dt_index, (bn_fun, (cnstr_head, included)))
@@ -250,18 +254,18 @@
(bn_fun_strs ~~ bn_fun_strs')
val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
+ val raw_dt_names' = map (Long_Name.qualify thy_name) raw_dt_names
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_env binds
- val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
+ val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
+ (*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_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
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 raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr;
+ val raw_bn_descr =
+ prep_bn_descr lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs2)
in
- (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy1)
+ (raw_dt_full_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr, lthy2)
end
*}
@@ -305,19 +309,11 @@
ML {*
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_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_funs, raw_bn_eqs, raw_bn_descr, raw_bn_descr2, lthy1) =
+ (* definition of the raw datatypes *)
+ val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_descr, lthy1) =
if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
else raise TEST lthy
- val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr)
- val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2)
- val _ = tracing ("raw_bclauses " ^ @{make_string} raw_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
val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr
@@ -349,7 +345,7 @@
val (fv, fvbn, fv_def, lthy3a) =
if get_STEPS lthy2 > 3
- then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) raw_bn_funs2) (map snd raw_bn_eqs2) descr sorts raw_bn_descr2 raw_bn_descr2 raw_bclauses lthy3
+ then define_raw_fvs descr sorts raw_bn_funs raw_bn_descr raw_bclauses lthy3
else raise TEST lthy3
@@ -362,9 +358,9 @@
val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
- val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
+ 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;
+ val bns = [] (*raw_bn_funs*) ~~ bn_nos;
val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
(rel_distinct ~~ alpha_ts_nobn));
val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
@@ -376,7 +372,7 @@
(* 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
+ val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4
val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5
val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
@@ -400,7 +396,7 @@
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;
+ val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct [] (*raw_bn_eqs*) (map fst bns) lthy8;
val (bns_rsp_pre, lthy9) = fold_map (
fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
resolve_tac bns_rsp_pre' 1)) bns lthy8;
@@ -429,7 +425,7 @@
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 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 (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, qalphabn_defs, lthy12c) =
quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
@@ -456,7 +452,7 @@
val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
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 qtys 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 _ = warning "Lifting eq-iff";
(*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
@@ -575,7 +571,7 @@
fun prep_binder env bn_str =
case (Syntax.read_term lthy bn_str) of
Free (x, _) => (NONE, index_lookup env x)
- | Const (a, T) $ Free (x, _) => (SOME (Free (Long_Name.base_name a, T)), index_lookup env x)
+ | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
| _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
fun prep_body env bn_str = index_lookup env bn_str
--- a/Nominal/nominal_dt_rawfuns.ML Fri May 21 11:40:18 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML Sat May 22 13:51:47 2010 +0100
@@ -18,10 +18,9 @@
val listify: Proof.context -> term -> term
val define_raw_fvs:
- string list -> term list ->
Datatype_Aux.descr ->
(string * sort) list ->
- (term * int * (int * term option) list list) list ->
+ term list ->
(term * int * (int * term option) list list) list ->
bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
end
@@ -123,7 +122,6 @@
NONE => mk_supp arg
| SOME fv => fv $ arg
end
-handle Option => error "fv_map lookup "
fun mk_fv_binder lthy fv_bn_map args (bn_option, i) =
let
@@ -133,7 +131,6 @@
NONE => (setify lthy arg, @{term "{}::atom set"})
| SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
end
-handle Option => error "fv_bn_map lookup "
fun mk_fv_bn_body fv_map fv_bn_map bn_args args i =
let
@@ -147,7 +144,6 @@
| SOME (NONE) => @{term "{}::atom set"}
| SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
end
-handle Option => error "fv_map/fv_bn_map lookup "
fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
let
@@ -197,41 +193,28 @@
map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
end
-fun define_raw_fvs t1 t2 dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
+fun define_raw_fvs dt_descr sorts bn_trms bn_funs2 bclausesss lthy =
let
- val _ = tracing ("bn-functions to be defined\n " ^ commas t1)
- val _ = tracing ("bn-equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) t2))
-
val fv_names = prefix_dt_names dt_descr sorts "fv_"
val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
val fv_frees = map Free (fv_names ~~ fv_tys);
val fv_map = fv_arg_tys ~~ fv_frees
- val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)
- val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)
- val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2
- val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2
+ val bn_tys2 = map (fn (_, i, _) => i) bn_funs2
+ val fv_bn_names2 = map (fn bn => "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bn_trms
val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
- val fv_bn_map2 = bns ~~ fv_bn_frees2
- val fv_bn_map3 = bns2 ~~ fv_bn_frees2
-
- val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2)
- val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3)
+ val fv_bn_map = bn_trms ~~ fv_bn_frees2
val constrs_info = all_dtyp_constrs_types dt_descr sorts
- val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map3)) constrs_info bclausesss
- val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2
+ val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss
+ val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_funs2
- val _ = tracing ("functions to be defined\n " ^ @{make_string} (t1 @ fv_names @ fv_bn_names2))
- val _ = tracing ("equations\n " ^
- cat_lines (map (Syntax.string_of_term lthy) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2)))
-
- val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (t1 @ fv_names @ fv_bn_names2)
- val all_fv_eqs = map (pair Attrib.empty_binding) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2)
+ val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)
+ val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)
fun pat_completeness_auto lthy =
Pat_Completeness.pat_completeness_tac lthy 1