nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:082d9fd28f89
+:ebf253d80670
 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_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 *)
 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2
 val _ = warning "Definition of raw fv-functions";
 val lthy3 = Theory_Target.init NONE thy;
 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) =
 if get_STEPS lthy3a > 3
 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a
 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
 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
 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4
 else raise TEST lthy4
 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4)
 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)
+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
 (* proving alpha equivalence *)
 val _ = warning "Proving equivalence"
 val alpha_refl_thms =
-if get_STEPS lthy > 9
+if get_STEPS lthy > 10
-then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6
+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
 (* proving alpha implies alpha_bn *)
 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 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
-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))
 (* 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_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
 val qtys = map #qtyp qty_infos
 val qalpha_bns_descr =
 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
 ||>> qconst_defs qtys qbns_descr
 ||>> qconst_defs qtys qfvs_descr
 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
-(* HERE *)
+(* temporary theorem bindings *)
 val (_, lthy8') = lthy8
 |> 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)
+||>> 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 *)
 val _ = warning "Proving respects";
 val q_name = space_implode "_" qty_names;
 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 =
 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",

changeset 2388	ebf253d80670
parent 2387	082d9fd28f89
child 2389	0f24c961b5f6