nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:107c06267f33
+:c6d30d5f5ba1
 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 else raise TEST lthy
 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 raw_tys = all_dtyps descr sorts
-val all_raw_ty_names = map (fst o dest_Type) all_raw_tys
+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 dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names
-val inject_thms = flat (map #inject dtinfos)
-val distinct_thms = flat (map #distinct dtinfos)
+val raw_inject_thms = flat (map #inject dtinfos)
-val constr_thms = inject_thms @ distinct_thms
+val raw_distinct_thms = flat (map #distinct dtinfos)
+val raw_induct_thm = #induct dtinfo
-val raw_induct_thm = #induct dtinfo;
+val raw_induct_thms = #inducts dtinfo
-val raw_induct_thms = #inducts dtinfo;
+val raw_exhaust_thms = map #exhaust dtinfos
-val exhaust_thms = map #exhaust dtinfos;
+val raw_size_trms = map size_const raw_tys
-val raw_size_trms = map size_const all_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
 (* definitions of raw permutations *)
 val _ = warning "Definition of raw permutations";
 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
 (* noting the raw permutations as eqvt theorems *)
 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
 (* definition of raw fv_functions *)
 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 *)
 val _ = warning "Definition of alphas";
 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
 val alpha_tys = map (domain_type o fastype_of) alpha_trms
 (* 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 *)
 val _ = warning "Proving equivariance";
 val bn_eqvt =
 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6
 else raise TEST lthy6
 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
 val alpha_equivp_thms =
 if get_STEPS lthy > 13
 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct
 (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
 (* noting the quot_respects lemmas *)
 else raise TEST lthy6
 (* 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
 val qfvs_descr =
 val qalpha_bns_descr =
 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 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
+|> define_qconsts qtys qconstrs_descr
-||>> qconst_defs qtys qbns_descr
+||>> define_qconsts qtys qbns_descr
-||>> qconst_defs qtys qfvs_descr
+||>> define_qconsts qtys qfvs_descr
-||>> qconst_defs qtys qfv_bns_descr
+||>> define_qconsts qtys qfv_bns_descr
-||>> qconst_defs qtys qalpha_bns_descr
+||>> define_qconsts qtys qalpha_bns_descr
 else raise TEST lthy7
-(*val _ = Local_Theory.theory_result
+(* definition of the quotient permfunctions and pt-class *)
-(qperm_defs qtys qty_full_names qperm_descr raw_perm_laws) lthy8*)
+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
 val qfvs = map #qconst qfvs_info
 val qfv_bns = map #qconst qfv_bns_info
 val qalpha_bns = map #qconst qalpha_bns_info
 (* 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)
 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs)
 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps)
 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws)
 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
 val _ =
-if get_STEPS lthy > 18
+if get_STEPS lthy > 20
-then true else raise TEST lthy8'
+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
 val _ = warning "Proving respects";
 val fv_rsp = flat (map snd fv_rsp_pre);
 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
 (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
 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
 (* 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;
 fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
 val _ = warning "Lifting induction";

changeset 2400	c6d30d5f5ba1
parent 2399	107c06267f33
child 2401	7645e18e8b19