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 2011 12ce87b55f97
parent 2008 1bddffddc03f
child 2016 1715dfe9406c
equal deleted inserted replaced
2010:19fe16dd36c2 2011:12ce87b55f97 
   326 
   326 
   327 
   327 
   328 ML {*
 
   328 ML {*
 
   329 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 
   329 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 
   330 let
 
   330 let
 
   331 
       
   332   (* definition of the raw datatype and raw bn-functions *)
 
   331   (* definition of the raw datatype and raw bn-functions *)
 
   333   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
 
   332   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
 
   334     raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 
   333     raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 
   335 
   334 
   336   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
 
   335   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
 
   337   val {descr, sorts, ...} = dtinfo;
 
   336   val {descr, sorts, ...} = dtinfo;
 
   338   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
   337   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
 
   339   val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
 
       
   340   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
 
   338   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
 
   341 
   339 
   342   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
   340   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
   343   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
 
   341   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
 
   344   val inject = flat (map #inject dtinfos);
 
   342   val inject = flat (map #inject dtinfos);
 
   357   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
 
   355   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
 
   358   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
   356   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
   359   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   357   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   360   val thy = Local_Theory.exit_global lthy2;
 
   358   val thy = Local_Theory.exit_global lthy2;
 
   361   val thy_name = Context.theory_name thy
 
   359   val thy_name = Context.theory_name thy
 
       
   360 
   362   val lthy3 = Theory_Target.init NONE thy;
 
   361   val lthy3 = Theory_Target.init NONE thy;
 
   363   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   362   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   364 
   363 
       
   364   (* definition of raw fv_functions *)
 
   365   val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 
   365   val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 
       
   366   
       
   367   (* definition of raw alphas *)
 
   366   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
 
   368   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
 
   367     define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
 
   369     define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
 
   368   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
 
   370   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
 
       
   371   
   369   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 
   372   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 
   370   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
 
   373   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
 
   371   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
 
   374   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
 
   372   val bns = raw_bn_funs ~~ bn_nos;
 
   375   val bns = raw_bn_funs ~~ bn_nos;
 
   373   val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
 
   376   val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
 
   374     (rel_distinct ~~ alpha_ts_nobn));
 
   377     (rel_distinct ~~ alpha_ts_nobn));
 
   375   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 
   378   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 
   376     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 
   379     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 
       
   380   
       
   381   (* definition of raw_alpha_eq_iff  lemmas *)
 
   377   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
 
   382   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
 
       
   383   
       
   384   (* proving equivariance lemmas *)
 
   378   val _ = warning "Proving equivariance";
 
   385   val _ = warning "Proving equivariance";
 
   379   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   386   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   380   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 
   387   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 
   381   fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
 
   388   fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
 
   382   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
   389   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
       
   390 
       
   391   (* provind alpha equivalence *)
 
   383   val _ = warning "Proving equivalence";
 
   392   val _ = warning "Proving equivalence";
 
   384   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   393   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   385   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
 
   394   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
 
   386   val alpha_equivp =
 
   395   val alpha_equivp =
 
   387     build_equivps alpha_ts reflps alpha_induct
 
   396     build_equivps alpha_ts reflps alpha_induct
 
   423   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
 
   432   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
 
   424   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
 
   433   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
 
   425   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
 
   434   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
 
   426   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
 
   435   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
 
   427   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
 
   436   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
 
   428   val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
 
   437   val (qalpha_ts_bn, qalphabn_defs, lthy12c) = 
       
   438     quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
 
   429   val _ = warning "Lifting permutations";
 
   439   val _ = warning "Lifting permutations";
 
   430   val thy = Local_Theory.exit_global lthy12c;
 
   440   val thy = Local_Theory.exit_global lthy12c;
 
   431   val perm_names = map (fn x => "permute_" ^ x) qty_names
 
   441   val perm_names = map (fn x => "permute_" ^ x) qty_names
 
   432   val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
 
   442   val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
 
   433   val lthy13 = Theory_Target.init NONE thy';
 
   443   val lthy13 = Theory_Target.init NONE thy';
 
   439   fun note_suffix s th ctxt =
 
   449   fun note_suffix s th ctxt =
 
   440     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
 
   450     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
 
   441   fun note_simp_suffix s th ctxt =
 
   451   fun note_simp_suffix s th ctxt =
 
   442     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 
   452     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 
   443   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
 
   453   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
 
   444     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
 
   454     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), 
       
   455     [Rule_Cases.name constr_names q_induct]) lthy13;
 
   445   val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
 
   456   val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
 
   446   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
 
   457   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
 
   447   val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
 
   458   val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
 
   448   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
 
   459   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
 
   449   val q_fv = map (lift_thm qtys lthy15) fv_def;
 
   460   val q_fv = map (lift_thm qtys lthy15) fv_def;
 
   647 
   658 
   648 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
 
   659 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
 
   649   (main_parser >> nominal_datatype2_cmd)
 
   660   (main_parser >> nominal_datatype2_cmd)
 
   650 *}
 
   661 *}
 
   651 
   662 
   652 
       
   653 (*
 
       
   654 atom_decl name
 
   663 atom_decl name
 
   655 
   664 
   656 nominal_datatype lam =
 
   665 nominal_datatype lam =
 
   657   Var name
 
   666   Var name
 
   658 | App lam lam
 
   667 | App lam lam
 
   728 and tys =
 
   737 and tys =
 
   729   Al xs::"name fset" t::"ty" bind_res xs in t
 
   738   Al xs::"name fset" t::"ty" bind_res xs in t
 
   730 
   739 
   731 thm ty_tys.fv[simplified ty_tys.supp]
 
   740 thm ty_tys.fv[simplified ty_tys.supp]
 
   732 thm ty_tys.eq_iff
 
   741 thm ty_tys.eq_iff
 
   733 *)
 
   742 
   734 
   743 
   735 
   744 
   736 (* some further tests *)
 
   745 (* some further tests *)
 
   737 
   746 
   738 (*
 
   747 (*
nominal2