Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/NewParser.thy
changeset 2119 238062c4c9f2
parent 2118 0e52851acac4
parent 2115 9b109ef7bf47
child 2122 24ca435ead14
equal deleted inserted replaced
2118:0e52851acac4 2119:238062c4c9f2 
   276 in
 
   276 in
 
   277   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
   277   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
   278 end
 
   278 end
 
   279 *}
 
   279 *}
 
   280 
   280 
   281 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 
       
   282 ML {* val cheat_equivp = Unsynchronized.ref false *}
 
   281 ML {* val cheat_equivp = Unsynchronized.ref false *}
 
   283 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 
   282 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 
   284 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
   283 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
   285 ML {* val cheat_supp_eq = Unsynchronized.ref false *}
 
   284 ML {* val cheat_supp_eq = Unsynchronized.ref false *}
 
   286 
   285 
   434 
   433 
   435   (* proving equivariance lemmas *)
 
   434   (* proving equivariance lemmas *)
 
   436   val _ = warning "Proving equivariance";
 
   435   val _ = warning "Proving equivariance";
 
   437   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   436   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   438   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 
   437   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 
   439   fun alpha_eqvt_tac' _ =
 
   438   val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
   440     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
       
   441     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
 
       
   442   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
       
   443 
   439 
   444   (* proving alpha equivalence *)
 
   440   (* proving alpha equivalence *)
 
   445   val _ = warning "Proving equivalence";
 
   441   val _ = warning "Proving equivalence";
 
   446   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   442   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   447   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
 
   443   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
 
   448   val alpha_equivp =
 
   444   val alpha_equivp =
 
   449     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
 
   445     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
 
   450     else build_equivps alpha_ts reflps alpha_induct
 
   446     else build_equivps alpha_ts reflps alpha_induct
 
   451       inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
 
   447       inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a;
 
   452   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   448   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   453   val qty_names = map Name.of_binding qty_binds;
 
   449   val qty_names = map Name.of_binding qty_binds;
 
   454   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   450   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   455   val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
 
   451   val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a;
 
   456   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   452   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   457   val raw_consts =
 
   453   val raw_consts =
 
   458     flat (map (fn (i, (_, _, l)) =>
 
   454     flat (map (fn (i, (_, _, l)) =>
 
   459       map (fn (cname, dts) =>
 
   455       map (fn (cname, dts) =>
 
   460         Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
 
   456         Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
nominal2