# HG changeset patch # User Cezary Kaliszyk # Date 1272628679 -7200 # Node ID 4df3441aa0b4d660f4c158913d2580949c1bc536 # Parent f03bfddc5aea2a04c3a24ee503e43e4ee4c73330 more parser/new parser synchronization. diff -r f03bfddc5aea -r 4df3441aa0b4 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri Apr 30 10:48:48 2010 +0200 +++ b/Nominal/NewParser.thy Fri Apr 30 13:57:59 2010 +0200 @@ -267,6 +267,15 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; + val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; + val inject = flat (map #inject dtinfos); + val distincts = flat (map #distinct dtinfos); + val rel_dtinfos = List.take (dtinfos, (length dts)); + val rel_distinct = map #distinct rel_dtinfos; + val induct = #induct dtinfo; + val exhausts = map #exhaust dtinfos; + val ((raw_perm_def, raw_perm_simps, perms), lthy2) = Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; @@ -277,11 +286,13 @@ val thy = Local_Theory.exit_global lthy2; val lthy3 = Theory_Target.init NONE thy; - val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; - val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) = - define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4; + val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; + val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = + define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a; + val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts + in - ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5) + ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) end *} @@ -468,7 +479,7 @@ | "bn (P2 p1 p2) = bn p1 \ bn p2" thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps -thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros +thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros[no_vars] nominal_datatype exp = EVar name diff -r f03bfddc5aea -r 4df3441aa0b4 Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Apr 30 10:48:48 2010 +0200 +++ b/Nominal/Parser.thy Fri Apr 30 13:57:59 2010 +0200 @@ -387,8 +387,10 @@ val ((raw_perm_def, raw_perm_simps, perms), lthy3) = Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; val raw_binds_flat = map (map flat) raw_binds; - val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = + val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; + val (fv, fvbn) = chop (length perms) fv_ts; + val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct; val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); @@ -402,14 +404,13 @@ val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 val _ = tracing "Proving equivariance"; val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 - val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) ordered_fv_ts lthy5 + val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 fun alpha_eqvt_tac' _ = if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; val _ = tracing "Proving equivalence"; - val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; - val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; + val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn @@ -430,7 +431,7 @@ val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; val _ = map tracing (map PolyML.makestring bns_rsp_pre') val (bns_rsp_pre, lthy9) = fold_map ( - fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => + 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); fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy @@ -438,7 +439,7 @@ val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; val (fv_rsp_pre, lthy10) = fold_map (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] - (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) ordered_fv_ts lthy9; + (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; val fv_rsp = flat (map snd fv_rsp_pre); val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; @@ -452,8 +453,8 @@ in constr_rsp_tac alpha_eq_iff (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 - val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12; + 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 perms) 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;