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 1414 d3b86738e848
parent 1412 137cad9c1ce9
child 1416 947e5f772a9c
equal deleted inserted replaced
1413:0310a21821a7 1414:d3b86738e848 
   301   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
 
   301   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
 
   302     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
 
   302     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
 
   303   val raw_binds_flat = map (map flat) raw_binds;
 
   303   val raw_binds_flat = map (map flat) raw_binds;
 
   304   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
 
   304   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
 
   305   val alpha_ts_loc = #preds alpha
 
   305   val alpha_ts_loc = #preds alpha
 
       
   306   val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
 
   306   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
 
   307   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
 
   307   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
 
   308   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
 
   308   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
 
   309   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
 
       
   310   val alpha_ts_nobn = List.take (alpha_ts, length perms)
 
   309   val alpha_induct_loc = #induct alpha
 
   311   val alpha_induct_loc = #induct alpha
 
   310   val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
 
   312   val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
 
   311   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
 
   313   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
 
   312   val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc;
 
   314   val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc;
 
   313   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 
   315   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 
   320   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
 
   322   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
 
   321   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 
   323   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 
   322   fun alpha_eqvt_tac' _ =
 
   324   fun alpha_eqvt_tac' _ =
 
   323     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
   325     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
   324     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
 
   326     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
 
   325   val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
 
   327   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
 
   326   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
 
   328   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
 
   327   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
   329   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
   328   val fv_eqvt_tac =
 
   330   val fv_eqvt_tac =
 
   329     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
 
   331     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
 
   330     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
 
   332     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
 
   331   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
 
   333   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
 
   332   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
 
   334   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
 
   333   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
 
   335   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
 
   334   val alpha_equivp_loc = map (equivp_hack lthy6) (List.take (alpha_ts_loc, length perms))
 
   336   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
 
   335 (*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
 
   337 (*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
 
   336     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
 
   338     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
 
   337   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 
   339   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 
   338   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   340   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   339   val qty_names = map Name.of_binding qty_binds;
 
   341   val qty_names = map Name.of_binding qty_binds;
 
   340   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   342   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   341 in
 
       
   342 if !restricted_nominal = 0 then
 
       
   343   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
 
       
   344 else
 
       
   345 let
 
       
   346   val lthy7 = define_quotient_type
 
   343   val lthy7 = define_quotient_type
 
   347     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts))
 
   344     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
 
   348     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
 
   345     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
 
   349   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   346   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   350   val raw_consts =
 
   347   val raw_consts =
 
   351     flat (map (fn (i, (_, _, l)) =>
 
   348     flat (map (fn (i, (_, _, l)) =>
 
   352       map (fn (cname, dts) =>
 
   349       map (fn (cname, dts) =>
 
   353         Const (cname, map (typ_of_dtyp descr sorts) dts --->
 
   350         Const (cname, map (typ_of_dtyp descr sorts) dts --->
 
   354           typ_of_dtyp descr sorts (DtRec i))) l) descr);
 
   351           typ_of_dtyp descr sorts (DtRec i))) l) descr);
 
   355   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
 
   352   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
 
   356   val (consts, const_defs) = split_list consts_defs;
 
   353   val (consts, const_defs) = split_list consts_defs;
 
   357 in
 
   354 in
 
   358 if !restricted_nominal = 1 then
 
   355 if !restricted_nominal = 0 then
 
   359   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
 
   356   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
 
   360 else
 
   357 else
 
   361 let
 
   358 let
 
   362   val (bns_rsp_pre, lthy9) = fold_map (
 
   359   val (bns_rsp_pre, lthy9) = fold_map (
 
   363     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
 
   360     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
 
   399     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 
   396     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 
   400 in
 
   397 in
 
   401   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 
   398   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 
   402 end
 
   399 end
 
   403 end
 
   400 end
 
   404 end
 
       
   405 *}
 
   401 *}
 
   406 
   402 
   407 ML {* 
   403 ML {* 
   408 (* parsing the datatypes and declaring *)
 
   404 (* parsing the datatypes and declaring *)
 
   409 (* constructors in the local theory    *)
 
   405 (* constructors in the local theory    *)
nominal2