--- a/Nominal/NewParser.thy Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/NewParser.thy Fri Jul 30 00:40:32 2010 +0100
@@ -305,24 +305,31 @@
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
val {descr, sorts, ...} = dtinfo
- val all_raw_tys = map (fn (_, (n, _, _)) => n) descr
+ val all_raw_tys = all_dtyps descr sorts
+ val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr
val all_raw_constrs =
flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
- val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_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 rel_dtinfos = List.take (dtinfos, (length dts));
val raw_constrs_distinct = (map #distinct rel_dtinfos);
- val induct_thm = #induct dtinfo;
+ val raw_induct_thm = #induct dtinfo;
+ val raw_induct_thms = #inducts dtinfo;
val exhaust_thms = map #exhaust dtinfos;
+ val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) 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 descr sorts induct_thm (length dts)) lthy0
+ then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0
else raise TEST lthy0
(* noting the raw permutations as eqvt theorems *)
@@ -338,7 +345,7 @@
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
+ then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
else raise TEST lthy3
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) =
@@ -367,7 +374,7 @@
then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
else raise TEST lthy4
- (* proving equivariance lemmas for bns, fvs and alpha *)
+ (* proving equivariance lemmas for bns, fvs, size and alpha *)
val _ = warning "Proving equivariance";
val bn_eqvt =
if get_STEPS lthy > 6
@@ -381,13 +388,19 @@
val fv_eqvt =
if get_STEPS lthy > 7
then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps)
- (Local_Theory.restore lthy_tmp)
+ (Local_Theory.restore lthy_tmp)
+ else raise TEST lthy4
+
+ val size_eqvt =
+ if get_STEPS lthy > 8
+ then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps)
+ (Local_Theory.restore lthy_tmp)
else raise TEST lthy4
val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
val (alpha_eqvt, lthy6) =
- if get_STEPS lthy > 8
+ if get_STEPS lthy > 9
then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
else raise TEST lthy4
@@ -395,23 +408,23 @@
val _ = warning "Proving equivalence"
val alpha_refl_thms =
- if get_STEPS lthy > 9
- then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6
+ if get_STEPS lthy > 10
+ then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6
else raise TEST lthy6
val alpha_sym_thms =
- if get_STEPS lthy > 10
+ if get_STEPS lthy > 11
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 > 11
+ if get_STEPS lthy > 12
then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms)
alpha_intros alpha_induct alpha_cases lthy6
else raise TEST lthy6
val alpha_equivp_thms =
- if get_STEPS lthy > 12
+ if get_STEPS lthy > 13
then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6
else raise TEST lthy6
@@ -419,16 +432,14 @@
val _ = warning "Proving alpha implies bn"
val alpha_bn_imp_thms =
- if get_STEPS lthy > 13
+ if get_STEPS lthy > 14
then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6
else raise TEST lthy6
(* auxiliary lemmas for respectfulness proofs *)
- (* HERE *)
-
- val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns
- alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
- val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test))
+ val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs
+ raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+
(* defining the quotient type *)
val _ = warning "Declaring the quotient types"
@@ -438,7 +449,7 @@
val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
val (qty_infos, lthy7) =
- if get_STEPS lthy > 14
+ if get_STEPS lthy > 15
then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
else raise TEST lthy6
@@ -463,7 +474,7 @@
map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms
val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) =
- if get_STEPS lthy > 15
+ if get_STEPS lthy > 16
then
lthy7
|> qconst_defs qtys qconstrs_descr
@@ -479,7 +490,7 @@
val qfv_bns = map #qconst qfv_bns_info
val qalpha_bns = map #qconst qalpha_bns_info
- (* HERE *)
+ (* temporary theorem bindings *)
val (_, lthy8') = lthy8
|> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts)
@@ -489,9 +500,11 @@
||>> 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)
+ ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
+ ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), size_eqvt)
val _ =
- if get_STEPS lthy > 16
+ if get_STEPS lthy > 17
then true else raise TEST lthy8'
(* old stuff *)
@@ -558,7 +571,7 @@
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) qconstrs;
- val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
+ val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm);
fun note_suffix s th ctxt =
snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
fun note_simp_suffix s th ctxt =