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/Parser.thy
changeset 1650 4b949985cf57
parent 1623 b63e85d36715
child 1651 f731e9aff866
equal deleted inserted replaced
1649:ba837d3ed37f 1650:4b949985cf57 
   285   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
   285   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
   286 end
 
   286 end
 
   287 *}
 
   287 *}
 
   288 
   288 
   289 ML {* val cheat_equivp = Unsynchronized.ref false *}
 
   289 ML {* val cheat_equivp = Unsynchronized.ref false *}
 
   290 ML {* val cheat_bn_eqvt = Unsynchronized.ref false *}
 
       
   291 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 
       
   292 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 
   290 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 
   293 ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
 
   291 ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
 
   294 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 
   292 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 
   295 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
 
   293 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
 
   296 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
   294 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
   312   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
   310   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
   313   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
 
   311   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
 
   314   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   312   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   315 
   313 
   316   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
 
   314   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
 
   317   val descr = #descr dtinfo;
 
   315   val {descr, sorts, ...} = dtinfo;
 
   318   val sorts = #sorts dtinfo;
 
   316   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
       
   317   val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
 
   319   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
 
   318   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
 
   320   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
   319   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
   321   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
 
   320   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
 
   322   val rel_dtinfos = List.take (dtinfos, (length dts));
 
   321   val rel_dtinfos = List.take (dtinfos, (length dts));
 
   323   val inject = flat (map #inject dtinfos);
 
   322   val inject = flat (map #inject dtinfos);
 
   343     (rel_distinct ~~ alpha_ts_nobn));
 
   342     (rel_distinct ~~ alpha_ts_nobn));
 
   344   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 
   343   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 
   345     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 
   344     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 
   346   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
 
   345   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
 
   347   val _ = tracing "Proving equivariance";
 
   346   val _ = tracing "Proving equivariance";
 
   348   fun build_bv_eqvt simps inducts (t, n) ctxt =
 
   347   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   349     build_eqvts Binding.empty [t]
 
   348   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5
 
   350       (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
 
       
   351        else build_eqvts_tac (nth inducts n) simps ctxt
 
       
   352       ) ctxt
 
       
   353   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
       
   354   val fv_eqvt_tac =
 
       
   355     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
 
       
   356     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5
 
       
   357   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5;
 
       
   358   val (fv_bn_eqvts, lthy6a) =
 
       
   359     if fv_ts_bn = [] then ([], lthy6) else
 
       
   360     fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts)
 
       
   361       (fv_ts_bn ~~ bn_nos) lthy6;
 
       
   362   val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
 
       
   363   fun alpha_eqvt_tac' _ =
 
   349   fun alpha_eqvt_tac' _ =
 
   364     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
   350     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
   365     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1
 
   351     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1
 
   366   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
 
   352   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
   367   val _ = tracing "Proving equivalence";
 
   353   val _ = tracing "Proving equivalence";
 
   368   val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
 
   354   val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
 
   369   val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   355   val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   370   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a;
 
   356   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
 
   371   val alpha_equivp =
 
   357   val alpha_equivp =
 
   372     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
 
   358     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
 
   373     else build_equivps alpha_ts reflps alpha_induct
 
   359     else build_equivps alpha_ts reflps alpha_induct
 
   374       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
 
   360       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
 
   375   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   361   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   376   val qty_names = map Name.of_binding qty_binds;
 
   362   val qty_names = map Name.of_binding qty_binds;
 
   377   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   363   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   378   val lthy7 = define_quotient_type
 
   364   val lthy7 = define_quotient_type
 
   379     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
 
   365     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
 
   380     (ALLGOALS (resolve_tac alpha_equivp)) lthy6a;
 
   366     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
 
   381   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   367   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   382   val raw_consts =
 
   368   val raw_consts =
 
   383     flat (map (fn (i, (_, _, l)) =>
 
   369     flat (map (fn (i, (_, _, l)) =>
 
   384       map (fn (cname, dts) =>
 
   370       map (fn (cname, dts) =>
 
   385         Const (cname, map (typ_of_dtyp descr sorts) dts --->
 
   371         Const (cname, map (typ_of_dtyp descr sorts) dts --->
 
   453   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
 
   439   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
 
   454   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
 
   440   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
 
   455   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
 
   441   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
 
   456   val q_dis = map (lift_thm lthy18) rel_dists;
 
   442   val q_dis = map (lift_thm lthy18) rel_dists;
 
   457   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
 
   443   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
 
   458   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
 
   444   val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt);
 
   459   val (_, lthy20) = Local_Theory.note ((Binding.empty,
 
   445   val (_, lthy20) = Local_Theory.note ((Binding.empty,
 
   460     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 
   446     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 
   461   val _ = tracing "Finite Support";
 
   447   val _ = tracing "Finite Support";
 
   462   val supports = map (prove_supports lthy20 q_perm) consts;
 
   448   val supports = map (prove_supports lthy20 q_perm) consts;
 
   463   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
 
   449   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
nominal2