# HG changeset patch # User Christian Urban # Date 1274532707 -3600 # Node ID 72ad4e766acfa818fa19a926dac605eb89fd4083 # Parent aecebd5ed424ac397d1dd3308a9b9e207c29269b properly exported bn_descr diff -r aecebd5ed424 -r 72ad4e766acf Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri May 21 11:40:18 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Sat May 22 13:51:47 2010 +0100 @@ -7,6 +7,7 @@ ML {* print_depth 50 *} declare [[STEPS = 4]] + nominal_datatype trm = Var "name" | App "trm" "trm" diff -r aecebd5ed424 -r 72ad4e766acf Nominal/NewAlpha.thy --- a/Nominal/NewAlpha.thy Fri May 21 11:40:18 2010 +0100 +++ b/Nominal/NewAlpha.thy Sat May 22 13:51:47 2010 +0100 @@ -127,7 +127,7 @@ let fun mk_alphabn_free (bn, ith, _) = let - val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); + val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn))); val ty = nth_dtyp dt_descr sorts ith; val alphabn_type = ty --> ty --> @{typ bool}; val alphabn_free = Free(alphabn_name, alphabn_type); diff -r aecebd5ed424 -r 72ad4e766acf Nominal/NewParser.thy --- 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 diff -r aecebd5ed424 -r 72ad4e766acf Nominal/nominal_dt_rawfuns.ML --- 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