diff -r a908ea36054f -r 4c5881455923 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri Jul 02 15:34:46 2010 +0100 +++ b/Nominal/NewParser.thy Wed Jul 07 09:34:00 2010 +0100 @@ -336,7 +336,7 @@ val _ = warning "Definition of raw fv-functions"; val lthy3 = Theory_Target.init NONE thy; - val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = + val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = if get_STEPS lthy3 > 2 then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 else raise TEST lthy3 @@ -370,7 +370,7 @@ val _ = warning "Proving equivariance"; val bn_eqvt = if get_STEPS lthy > 6 - then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 + then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 else raise TEST lthy4 (* noting the bn_eqvt lemmas in a temprorary theory *) @@ -437,25 +437,38 @@ val qtys = map #qtyp qty_infos (* defining of quotient term-constructors, binding functions, free vars functions *) - val qconstr_descr = + val _ = warning "Defining the quotient constnats" + val qconstrs_descr = flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs val qbns_descr = - map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs + map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns val qfvs_descr = - map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs + map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs + val qfv_bns_descr = + map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns - val (qs, lthy8) = + (* TODO: probably also needs alpha_bn *) + val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = if get_STEPS lthy > 15 - then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7 + then + lthy7 + |> qconst_defs qtys qconstrs_descr + ||>> qconst_defs qtys qbns_descr + ||>> qconst_defs qtys qfvs_descr + ||>> qconst_defs qtys qfv_bns_descr else raise TEST lthy7 - val _ = tracing ("raw fvs " ^ commas (map @{make_string} raw_fvs)) - val _ = tracing ("raw fv_bns " ^ commas (map @{make_string} raw_fv_bns)) + val qconstrs = map #qconst qconstrs_info + val qbns = map #qconst qbns_info + val qfvs = map #qconst qfvs_info + val qfv_bns = map #qconst qfv_bns_info + (* respectfulness proofs *) + (* HERE *) val _ = @@ -464,18 +477,10 @@ (* old stuff *) - val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); - val raw_consts = - flat (map (fn (i, (_, _, l)) => - 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 dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts - val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7; val _ = warning "Proving respects"; val bn_nos = map (fn (_, i, _) => i) raw_bn_info; - val bns = raw_bn_funs ~~ bn_nos; + val bns = raw_bns ~~ bn_nos; val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; val (bns_rsp_pre, lthy9) = fold_map ( @@ -504,27 +509,36 @@ let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - const_rsp_tac) raw_consts lthy11a + const_rsp_tac) all_raw_constrs lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; + val (qfv_info, lthy12a) = qconst_defs qtys dd lthy12; + val qfv_ts = map #qconst qfv_info + val qfv_defs = map #def qfv_info 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 dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs - val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns + val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a; + val qbn_ts = map #qconst qbn_info + val qbn_defs = map #def qbn_info val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms - val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b; + val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b; + val qalpha_bn_trms = map #qconst qalpha_info + val qalphabn_defs = map #def qalpha_info + val _ = warning "Lifting permutations"; val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs - val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy; + (* use Local_Theory.theory_result *) + val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy; val lthy13 = Theory_Target.init NONE thy'; + val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = warning "Lifting induction"; - val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; + val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); @@ -556,7 +570,7 @@ val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = warning "Supports"; - val supports = map (prove_supports lthy20 q_perm) consts; + val supports = map (prove_supports lthy20 q_perm) qconstrs; val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); val thy3 = Local_Theory.exit_global lthy20; val _ = warning "Instantiating FS";