nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:aecebd5ed424
+:72ad4e766acf
 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or
 appends of elements; in case of recursive calls it retruns also the applied
 bn function *)
 ML {*
-fun strip_bn_fun t =
+fun strip_bn_fun lthy args t =
-case t of
+let
-Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+fun aux t =
-| Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+case t of
-| Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
-(i, NONE) :: strip_bn_fun y
+| Const (@{const_name append}, _) $ l $ r => aux l @ aux r
-| Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+| Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
-(i, NONE) :: strip_bn_fun y
+(find_index (equal x) args, NONE) :: aux y
-| Const (@{const_name bot}, _) => []
+| Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
-| Const (@{const_name Nil}, _) => []
+(find_index (equal x) args, NONE) :: aux y
-| (f as Free _) $ Bound i => [(i, SOME f)]
+| Const (@{const_name bot}, _) => []
-| _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
+| 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 {*
 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_descr lthy dt_names dts eqs =
 let
 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 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)))
 end
 fun order dts i ts =
 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
 (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_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_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
+val raw_bn_descr =
-fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
+prep_bn_descr lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs2)
-val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr;
+in
-in
+(raw_dt_full_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr, 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, lthy1)
 end
 *}
 lemma equivp_hack: "equivp x"
 sorry
 setup STEPS_setup
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
-(* definition of the raw datatypes and raw bn-functions *)
+(* definition of the raw datatypes *)
-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) =
+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
 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr
 (* definition of raw fv_functions *)
 val lthy3 = Theory_Target.init NONE thy;
 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
 (* definition of raw alphas *)
 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
 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;
-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)
 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 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;
 (* 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;
 (* proving alpha equivalence *)
 val _ = warning "Proving equivalence";
 map (fn (cname, dts) =>
 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
 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;
 val bns_rsp = flat (map snd bns_rsp_pre);
 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 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;
 val _ = warning "Lifting permutations";
 val thy = Local_Theory.exit_global lthy12c;
 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
 val q_perm = map (lift_thm qtys lthy14) raw_perm_defs;
 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);*)
 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp
 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
 |> map (map (fn (_, antys, _, bns) => (map fst antys, bns)))
 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
 fun prep_mode "bind"     = Lst

changeset 2294	72ad4e766acf
parent 2293	aecebd5ed424
child 2295	8aff3f3ce47f