diff -r 9ca7b249760e -r aead2aad845c Nominal/NewParser.thy --- a/Nominal/NewParser.thy Mon May 24 20:50:15 2010 +0100 +++ b/Nominal/NewParser.thy Mon May 24 21:11:33 2010 +0100 @@ -349,21 +349,19 @@ else raise TEST lthy3 (* definition of raw alphas *) - val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = + val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = if get_STEPS lthy > 4 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a else raise TEST lthy3a - val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) 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_nos = map (dtyp_no_of_typ dts_names) bn_tys; + 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 = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts)); val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) - ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) + ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts)) (* definition of raw_alpha_eq_iff lemmas *) val alpha_eq_iff = @@ -373,15 +371,27 @@ val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; - (* proving equivariance lemmas *) + (* proving equivariance lemmas for bns, fvs and alpha *) 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 (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 - val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; + val (bv_eqvt, lthy5) = + if get_STEPS lthy > 6 + then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 + else raise TEST lthy4 + + val (fv_eqvt, lthy6) = + if get_STEPS lthy > 7 + then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 + else raise TEST lthy5 + + val (alpha_eqvt, lthy6a) = + if get_STEPS lthy > 8 + then Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6 + else raise TEST lthy6 + (* proving alpha equivalence *) val _ = warning "Proving equivalence"; - val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts_nobn, alpha_ts_bn) bn_nos; + val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts, alpha_bn_ts) bn_nos; val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts @@ -390,7 +400,7 @@ val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names - val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a; + val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts alpha_equivp lthy6a; 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)) => @@ -399,7 +409,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; @@ -416,11 +426,11 @@ (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else - let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; + let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_bn_ts lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - alpha_bn_rsp_tac) alpha_ts_bn lthy11 + alpha_bn_rsp_tac) alpha_bn_ts lthy11 fun const_rsp_tac _ = - let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a + let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_bn_ts lthy11a in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ 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 @@ -428,10 +438,10 @@ val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) 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 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 (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_bn_ts + val (qalpha_bn_ts, qalphabn_defs, lthy12c) = + quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_ts) lthy12b; val _ = warning "Lifting permutations"; val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names @@ -455,7 +465,7 @@ val lthy15 = note_simp_suffix "perm" q_perm lthy14a; val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; 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);*) @@ -479,7 +489,7 @@ val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) val lthy22 = Class.prove_instantiation_instance tac lthy21 - val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; + val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts, qalpha_bn_ts) bn_nos; val (names, supp_eq_t) = supp_eq fv_alpha_all; val _ = warning "Support Equations"; fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else