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 2050 8bd75f2fd7b0
parent 2048 20be95dce643
child 2076 6cb1a4639521
equal deleted inserted replaced
2049:38bbccdf9ff9 2050:8bd75f2fd7b0 
   157 in
 
   157 in
 
   158   map (map (map rawify_bclause)) bclauses
 
   158   map (map (map rawify_bclause)) bclauses
 
   159 end
 
   159 end
 
   160 *}
 
   160 *}
 
   161 
   161 
   162 text {* What does the prep_bn code do? Cezary's Function? *}
 
   162 (* strip_bn_fun takes a bn function defined by the user as a union or
 
   163 
   163    append of elements and returns those elements together with bn functions
 
       
   164    applied *)
 
   164 ML {*
 
   165 ML {*
 
   165 fun strip_bn_fun t =
 
   166 fun strip_bn_fun t =
 
   166   case t of
 
   167   case t of
 
   167     Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
 
   168     Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
 
   168   | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
 
   169   | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
 
   256   ||>> pair raw_bclauses
 
   257   ||>> pair raw_bclauses
 
   257   ||>> pair raw_bns
 
   258   ||>> pair raw_bns
 
   258 end
 
   259 end
 
   259 *}
 
   260 *}
 
   260 
   261 
       
   262 lemma equivp_hack: "equivp x"
 
       
   263 sorry
 
       
   264 ML {*
 
       
   265 fun equivp_hack ctxt rel =
 
       
   266 let
 
       
   267   val thy = ProofContext.theory_of ctxt
 
       
   268   val ty = domain_type (fastype_of rel)
 
       
   269   val cty = ctyp_of thy ty
 
       
   270   val ct = cterm_of thy rel
 
       
   271 in
 
       
   272   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
       
   273 end
 
       
   274 *}
 
       
   275 
       
   276 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 
       
   277 ML {* val cheat_equivp = Unsynchronized.ref false *}
 
       
   278 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 
       
   279 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
       
   280 ML {* val cheat_supp_eq = Unsynchronized.ref false *}
 
       
   281 
       
   282 ML {*
 
       
   283 fun remove_loop t =
 
       
   284   let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end
 
       
   285   handle TERM _ => @{thm eqTrueI} OF [t]
 
       
   286 *}
 
   261 
   287 
   262 text {* 
   288 text {* 
   263   nominal_datatype2 does the following things in order:
 
   289   nominal_datatype2 does the following things in order:
 
   264 
   290 
   265 Parser.thy/raw_nominal_decls
 
   291 Parser.thy/raw_nominal_decls
 
   322  28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
 
   348  28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
 
   323 Equivp.thy/supp_eq
 
   349 Equivp.thy/supp_eq
 
   324  29) prove supp = fv
 
   350  29) prove supp = fv
 
   325 *}
 
   351 *}
 
   326 
   352 
       
   353 ML {*
 
       
   354 (* for testing porposes - to exit the procedure early *)
 
       
   355 exception TEST of Proof.context
 
       
   356 
       
   357 val STEPS = 10
 
       
   358 *}
 
   327 
   359 
   328 ML {*
 
   360 ML {*
 
   329 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 
   361 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 
   330 let
 
   362 let
 
   331   (* definition of the raw datatype and raw bn-functions *)
 
   363   (* definition of the raw datatype and raw bn-functions *)
 
   332   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
 
   364   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
 
   333     raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 
   365     if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 
       
   366     else raise TEST lthy
 
   334 
   367 
   335   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
 
   368   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
 
   336   val {descr, sorts, ...} = dtinfo;
 
   369   val {descr, sorts, ...} = dtinfo;
 
   337   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
 
   370   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
 
   338   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
 
   371   val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
 
   339 
       
   340   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
   372   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
       
   373 
   341   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
 
   374   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
 
   342   val inject = flat (map #inject dtinfos);
 
   375   
   343   val distincts = flat (map #distinct dtinfos);
 
   376   (* what is the difference between raw_dt_names and all_full_tnames ? *)
 
   344   val rel_dtinfos = List.take (dtinfos, (length dts));
 
   377   (* what is the purpose of dtinfo and dtinfos ? *)
 
   345   val rel_distinct = map #distinct rel_dtinfos;
 
   378   val _ = tracing ("raw_dt_names " ^ commas raw_dt_names)
 
   346   val induct = #induct dtinfo;
 
   379   val _ = tracing ("all_full_tnames " ^ commas all_full_tnames)
 
   347   val exhausts = map #exhaust dtinfos;
 
   380 
       
   381   val inject_thms = flat (map #inject dtinfos);
 
       
   382   val distinct_thms = flat (map #distinct dtinfos);
 
       
   383   val rel_dtinfos = List.take (dtinfos, (length dts)); 
       
   384   val rel_distinct = map #distinct rel_dtinfos;  (* thm list list *)
 
       
   385   val induct_thm = #induct dtinfo;
 
       
   386   val exhaust_thms = map #exhaust dtinfos;
 
   348 
   387 
   349   (* definitions of raw permutations *)
 
   388   (* definitions of raw permutations *)
 
   350   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
 
   389   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
 
   351     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
 
   390     if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
 
       
   391     else raise TEST lthy1
 
   352 
   392 
   353   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
 
   393   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
 
   354   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
 
   394   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
 
   355   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
 
   395   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
 
   356   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
   396   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
   360 
   400 
   361   val lthy3 = Theory_Target.init NONE thy;
 
   401   val lthy3 = Theory_Target.init NONE thy;
 
   362   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   402   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   363 
   403 
   364   (* definition of raw fv_functions *)
 
   404   (* definition of raw fv_functions *)
 
   365   val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 
   405   val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
 
   366   
   406   val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls)
 
       
   407   val ((fv, fvbn), fv_def, lthy3a) = 
       
   408     if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
 
       
   409     else raise TEST lthy3
 
       
   410   
       
   411 
   367   (* definition of raw alphas *)
 
   412   (* definition of raw alphas *)
 
   368   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
 
   413   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
 
   369     define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
 
   414     if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
 
       
   415     else raise TEST lthy3a
 
       
   416   
   370   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
 
   417   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
 
   371   
   418   
   372   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 
   419   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
 
   373   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
 
   420   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
 
   374   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
 
   421   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
 
   377     (rel_distinct ~~ alpha_ts_nobn));
 
   424     (rel_distinct ~~ alpha_ts_nobn));
 
   378   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 
   425   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 
   379     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 
   426     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
 
   380   
   427   
   381   (* definition of raw_alpha_eq_iff  lemmas *)
 
   428   (* definition of raw_alpha_eq_iff  lemmas *)
 
   382   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
 
   429   val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
 
   383   
   430   val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
 
       
   431   val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
 
       
   432 
   384   (* proving equivariance lemmas *)
 
   433   (* proving equivariance lemmas *)
 
   385   val _ = warning "Proving equivariance";
 
   434   val _ = warning "Proving equivariance";
 
   386   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   435   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
 
   387   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 
   436   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 
   388   fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
 
   437   fun alpha_eqvt_tac' _ =
 
       
   438     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
       
   439     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
 
   389   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
   440   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
   390 
   441 
   391   (* provind alpha equivalence *)
 
   442   (* proving alpha equivalence *)
 
   392   val _ = warning "Proving equivalence";
 
   443   val _ = warning "Proving equivalence";
 
   393   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   444   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
 
   394   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
 
   445   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
 
   395   val alpha_equivp =
 
   446   val alpha_equivp =
 
   396     build_equivps alpha_ts reflps alpha_induct
 
   447     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
 
   397       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
 
   448     else build_equivps alpha_ts reflps alpha_induct
 
       
   449       inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
 
   398   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   450   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   399   val qty_names = map Name.of_binding qty_binds;
 
   451   val qty_names = map Name.of_binding qty_binds;
 
   400   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   452   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 
   401   val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
 
   453   val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
 
   402   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   454   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 
   403   val raw_consts =
 
   455   val raw_consts =
 
   404     flat (map (fn (i, (_, _, l)) =>
 
   456     flat (map (fn (i, (_, _, l)) =>
 
   405       map (fn (cname, dts) =>
 
   457       map (fn (cname, dts) =>
 
   406         Const (cname, map (typ_of_dtyp descr sorts) dts --->
 
   458         Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
 
   407           typ_of_dtyp descr sorts (DtRec i))) l) descr);
 
   459           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
 
   408   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
 
   460   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
 
   409   val _ = warning "Proving respects";
 
   461   val _ = warning "Proving respects";
 
   410   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
 
   462   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
 
   411   val (bns_rsp_pre, lthy9) = fold_map (
 
   463   val (bns_rsp_pre, lthy9) = fold_map (
 
   412     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
 
   464     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
 
   413        resolve_tac bns_rsp_pre' 1)) bns lthy8;
 
   465        resolve_tac bns_rsp_pre' 1)) bns lthy8;
 
   414   val bns_rsp = flat (map snd bns_rsp_pre);
 
   466   val bns_rsp = flat (map snd bns_rsp_pre);
 
   415   (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
 
   467 
   416   fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
 
   468   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
 
       
   469     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
 
   417   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
 
   470   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
 
   418   val (fv_rsp_pre, lthy10) = fold_map
 
   471   val (fv_rsp_pre, lthy10) = fold_map
 
   419     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
 
   472     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
 
   420     (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
 
   473     (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
 
   421   val fv_rsp = flat (map snd fv_rsp_pre);
 
   474   val fv_rsp = flat (map snd fv_rsp_pre);
 
   422   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
 
   475   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
 
   423     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
 
   476     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
 
       
   477   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
 
       
   478     else
 
       
   479       let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
 
   424   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
 
   480   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
 
   425         (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
 
   481     alpha_bn_rsp_tac) alpha_ts_bn lthy11
 
   426   fun const_rsp_tac _ =
 
   482   fun const_rsp_tac _ =
 
   427     let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
 
   483     let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
 
   428       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
 
   484       in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
 
   429   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
 
   485   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
 
   430     const_rsp_tac) raw_consts lthy11a
 
   486     const_rsp_tac) raw_consts lthy11a
 
   431     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
 
   487     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
 
   432   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
 
   488   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
 
   433   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
 
   489   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
 
   443   val lthy13 = Theory_Target.init NONE thy';
 
   499   val lthy13 = Theory_Target.init NONE thy';
 
   444   val q_name = space_implode "_" qty_names;
 
   500   val q_name = space_implode "_" qty_names;
 
   445   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
 
   501   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
 
   446   val _ = warning "Lifting induction";
 
   502   val _ = warning "Lifting induction";
 
   447   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
 
   503   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
 
   448   val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
 
   504   val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
 
   449   fun note_suffix s th ctxt =
 
   505   fun note_suffix s th ctxt =
 
   450     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
 
   506     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
 
   451   fun note_simp_suffix s th ctxt =
 
   507   fun note_simp_suffix s th ctxt =
 
   452     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 
   508     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 
   453   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
 
   509   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
 
   461   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
 
   517   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
 
   462   val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
 
   518   val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
 
   463   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
 
   519   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
 
   464   val _ = warning "Lifting eq-iff";
 
   520   val _ = warning "Lifting eq-iff";
 
   465   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
 
   521   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
 
   466   val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
 
   522   val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
 
   467   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
 
   523   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
 
   468   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
 
   524   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
 
   469   val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
 
   525   val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
 
   470   val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
 
   526   val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
 
   471   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
 
   527   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
 
   485   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
 
   541   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
 
   486   val lthy22 = Class.prove_instantiation_instance tac lthy21
 
   542   val lthy22 = Class.prove_instantiation_instance tac lthy21
 
   487   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
 
   543   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
 
   488   val (names, supp_eq_t) = supp_eq fv_alpha_all;
 
   544   val (names, supp_eq_t) = supp_eq fv_alpha_all;
 
   489   val _ = warning "Support Equations";
 
   545   val _ = warning "Support Equations";
 
   490   val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
 
   546   fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
 
       
   547     supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
 
       
   548   val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
 
       
   549     let val _ = warning ("Support eqs failed") in [] end;
 
   491   val lthy23 = note_suffix "supp" q_supp lthy22;
 
   550   val lthy23 = note_suffix "supp" q_supp lthy22;
 
   492 in
 
   551 in
 
   493   (0, lthy23)
 
   552   (0, lthy23)
 
   494 end
 
   553 end handle TEST ctxt => (0, ctxt)
 
   495 *}
 
   554 *}
 
   496 
   555 
   497 section {* Preparing and parsing of the specification *}
 
   556 section {* Preparing and parsing of the specification *}
 
   498 
   557 
   499 ML {* 
   558 ML {* 
   658 
   717 
   659 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
 
   718 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
 
   660   (main_parser >> nominal_datatype2_cmd)
 
   719   (main_parser >> nominal_datatype2_cmd)
 
   661 *}
 
   720 *}
 
   662 
   721 
       
   722 (*
 
   663 atom_decl name
 
   723 atom_decl name
 
   664 
   724 
   665 nominal_datatype lam =
 
   725 nominal_datatype lam =
 
   666   Var name
 
   726   Var name
 
   667 | App lam lam
 
   727 | App lam lam
 
   674  bn::"pt \<Rightarrow> atom set"
 
   734  bn::"pt \<Rightarrow> atom set"
 
   675 where
 
   735 where
 
   676   "bn (P1 x) = {atom x}"
 
   736   "bn (P1 x) = {atom x}"
 
   677 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
   737 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
   678 
   738 
       
   739 find_theorems Var_raw
 
       
   740 
       
   741 
       
   742 
   679 thm lam_pt.bn
 
   743 thm lam_pt.bn
 
   680 thm lam_pt.fv[simplified lam_pt.supp(1-2)]
 
   744 thm lam_pt.fv[simplified lam_pt.supp(1-2)]
 
   681 thm lam_pt.eq_iff
 
   745 thm lam_pt.eq_iff
 
   682 thm lam_pt.induct
 
   746 thm lam_pt.induct
 
   683 thm lam_pt.perm
 
   747 thm lam_pt.perm
 
   738   Al xs::"name fset" t::"ty" bind_res xs in t
 
   802   Al xs::"name fset" t::"ty" bind_res xs in t
 
   739 
   803 
   740 thm ty_tys.fv[simplified ty_tys.supp]
 
   804 thm ty_tys.fv[simplified ty_tys.supp]
 
   741 thm ty_tys.eq_iff
 
   805 thm ty_tys.eq_iff
 
   742 
   806 
   743 
   807 *)
 
   744 
   808 
   745 (* some further tests *)
 
   809 (* some further tests *)
 
   746 
   810 
   747 (*
 
   811 (*
 
   748 nominal_datatype ty2 =
 
   812 nominal_datatype ty2 =
nominal2