diff -r 107c06267f33 -r c6d30d5f5ba1 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sun Aug 15 11:03:13 2010 +0800 +++ b/Nominal/NewParser.thy Sun Aug 15 14:00:28 2010 +0800 @@ -312,20 +312,19 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo - val all_raw_constrs = + val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) - val all_raw_tys = all_dtyps descr sorts - val all_raw_ty_names = map (fst o dest_Type) all_raw_tys + val raw_tys = all_dtyps descr sorts + val raw_full_ty_names = map (fst o dest_Type) raw_tys - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names - val inject_thms = flat (map #inject dtinfos) - val distinct_thms = flat (map #distinct dtinfos) - val constr_thms = inject_thms @ distinct_thms - - val raw_induct_thm = #induct dtinfo; - val raw_induct_thms = #inducts dtinfo; - val exhaust_thms = map #exhaust dtinfos; - val raw_size_trms = map size_const all_raw_tys + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names + + val raw_inject_thms = flat (map #inject dtinfos) + val raw_distinct_thms = flat (map #distinct dtinfos) + val raw_induct_thm = #induct dtinfo + val raw_induct_thms = #inducts dtinfo + val raw_exhaust_thms = map #exhaust dtinfos + val raw_size_trms = map size_const raw_tys val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |> `(fn thms => (length thms) div 2) |> uncurry drop @@ -335,7 +334,7 @@ val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = if get_STEPS lthy0 > 1 then Local_Theory.theory_result - (define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0 + (define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm) lthy0 else raise TEST lthy0 val lthy2a = Named_Target.reinit lthy2 lthy2 @@ -346,12 +345,13 @@ val _ = warning "Definition of raw fv-functions"; val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = if get_STEPS lthy3 > 2 - then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 + then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs + (raw_inject_thms @ raw_distinct_thms) lthy3 else raise TEST lthy3 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = if get_STEPS lthy3a > 3 - then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a + then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a else raise TEST lthy3a (* definition of raw alphas *) @@ -365,14 +365,14 @@ (* definition of alpha-distinct lemmas *) val _ = warning "Distinct theorems"; val alpha_distincts = - mk_alpha_distincts lthy4 alpha_cases distinct_thms alpha_trms all_raw_tys + mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys (* definition of alpha_eq_iff lemmas *) (* they have a funny shape for the simplifier *) val _ = warning "Eq-iff theorems"; val (alpha_eq_iff_simps, alpha_eq_iff) = if get_STEPS lthy > 5 - then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases + then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases else raise TEST lthy4 (* proving equivariance lemmas for bns, fvs, size and alpha *) @@ -421,7 +421,7 @@ val alpha_trans_thms = if get_STEPS lthy > 12 - then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) + then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_induct alpha_cases lthy6 else raise TEST lthy6 @@ -447,7 +447,7 @@ (raw_size_thms @ raw_size_eqvt) lthy6 |> map mk_funs_rsp - val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros + val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt @@ -462,21 +462,22 @@ (* defining the quotient type *) val _ = warning "Declaring the quotient types" val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts - val qty_binds = map (fn (_, bind, _, _) => bind) dts - val qty_names = map Name.of_binding qty_binds; - + val (qty_infos, lthy7) = if get_STEPS lthy > 16 - then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a + then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a else raise TEST lthy6a val qtys = map #qtyp qty_infos - + val qty_full_names = map (fst o dest_Type) qtys + val qty_names = map Long_Name.base_name qty_full_names + + (* defining of quotient term-constructors, binding functions, free vars functions *) val _ = warning "Defining the quotient constants" 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 + |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs val qbns_descr = map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns @@ -493,20 +494,34 @@ val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs + val qsize_descr = + map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms + val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = if get_STEPS lthy > 17 then lthy7 - |> qconst_defs qtys qconstrs_descr - ||>> qconst_defs qtys qbns_descr - ||>> qconst_defs qtys qfvs_descr - ||>> qconst_defs qtys qfv_bns_descr - ||>> qconst_defs qtys qalpha_bns_descr + |> define_qconsts qtys qconstrs_descr + ||>> define_qconsts qtys qbns_descr + ||>> define_qconsts qtys qfvs_descr + ||>> define_qconsts qtys qfv_bns_descr + ||>> define_qconsts qtys qalpha_bns_descr else raise TEST lthy7 - (*val _ = Local_Theory.theory_result - (qperm_defs qtys qty_full_names qperm_descr raw_perm_laws) lthy8*) + (* definition of the quotient permfunctions and pt-class *) + val lthy9 = + if get_STEPS lthy > 18 + then Local_Theory.theory + (define_qperms qtys qty_full_names qperm_descr raw_perm_laws) lthy8 + else raise TEST lthy8 + + val lthy9' = + if get_STEPS lthy > 19 + then Local_Theory.theory + (define_qsizes qtys qty_full_names qsize_descr) lthy9 + else raise TEST lthy9 + val lthy9a = Named_Target.reinit lthy9' lthy9' val qconstrs = map #qconst qconstrs_info val qbns = map #qconst qbns_info @@ -517,7 +532,7 @@ (* temporary theorem bindings *) - val (_, lthy8') = lthy8 + val (_, lthy9') = lthy9a |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) @@ -527,12 +542,12 @@ ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) val _ = - if get_STEPS lthy > 18 - then true else raise TEST lthy8' + if get_STEPS lthy > 20 + then true else raise TEST lthy9' (* old stuff *) - val thy = ProofContext.theory_of lthy8' + val thy = ProofContext.theory_of lthy9' val thy_name = Context.theory_name thy val qty_full_names = map (Long_Name.qualify thy_name) qty_names @@ -561,28 +576,28 @@ (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_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms 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_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms 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_bn_trms lthy11 fun const_rsp_tac _ = 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) all_raw_constrs lthy11a + const_rsp_tac) 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_info, lthy12a) = qconst_defs qtys dd lthy12; + val (qfv_info, lthy12a) = define_qconsts 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_bns - val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a; + val (qbn_info, lthy12b) = define_qconsts 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_info, lthy12c) = qconst_defs qtys dd lthy12b; + val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b; val qalpha_bn_trms = map #qconst qalpha_info val qalphabn_defs = map #def qalpha_info @@ -591,7 +606,7 @@ 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 (* use Local_Theory.theory_result *) - val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy; + val thy' = define_qperms qtys qty_full_names dd raw_perm_laws thy; val lthy13 = Named_Target.init "" thy'; val q_name = space_implode "_" qty_names;