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 1422 a26cb19375e8
parent 1420 e655ea5f0b5f
child 1428 4029105011ca
equal deleted inserted replaced
1421:95324fb345e5 1422:a26cb19375e8 
   251   ||>> pair raw_binds
 
   251   ||>> pair raw_binds
 
   252   ||>> pair raw_bns
 
   252   ||>> pair raw_bns
 
   253 end
 
   253 end
 
   254 *}
 
   254 *}
 
   255 
   255 
   256 ML {* add_primrec_wrapper *}
 
   256 ML {*
 
       
   257 fun un_raw name = unprefix "_raw" name handle Fail _ => name
 
       
   258 fun add_under names = hd names :: (map (prefix "_") (tl names))
 
       
   259 fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))
 
       
   260 val un_raw_names = rename_vars un_raws
 
       
   261 fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
 
       
   262 *}
 
   257 
   263 
   258 lemma equivp_hack: "equivp x"
 
   264 lemma equivp_hack: "equivp x"
 
   259 sorry
 
   265 sorry
 
   260 ML {*
 
   266 ML {*
 
   261 fun equivp_hack ctxt rel =
 
   267 fun equivp_hack ctxt rel =
 
   379   val thy = Local_Theory.exit_global lthy12c;
 
   385   val thy = Local_Theory.exit_global lthy12c;
 
   380   val perm_names = map (fn x => "permute_" ^ x) qty_names
 
   386   val perm_names = map (fn x => "permute_" ^ x) qty_names
 
   381   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
 
   387   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
 
   382   val lthy13 = Theory_Target.init NONE thy';
 
   388   val lthy13 = Theory_Target.init NONE thy';
 
   383   val q_name = space_implode "_" qty_names;
 
   389   val q_name = space_implode "_" qty_names;
 
   384   val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
 
   390   val q_induct = lift_thm lthy13 induct;
 
   385   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
 
   391   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
 
   386   val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def;
 
   392   val q_perm = map (lift_thm lthy14) raw_perm_def;
 
   387   val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
 
   393   val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
 
   388   val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def;
 
   394   val q_fv = map (lift_thm lthy15) fv_def;
 
   389   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
 
   395   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
 
   390   val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
 
   396   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
 
   391   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
 
   397   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
 
   392   val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
 
   398   val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
 
   393   val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
 
   399   val q_inj_pre = map (lift_thm lthy17) inj_unfolded;
 
   394   val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
 
   400   val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
 
   395   val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
 
   401   val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
 
   396   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
 
   402   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
 
   397     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
 
   403     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
 
   398   val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
 
   404   val q_dis = map (lift_thm lthy18) rel_dists;
 
   399   val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
 
   405   val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
 
   400   val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt;
 
   406   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
 
   401   val (_, lthy20) = Local_Theory.note ((Binding.empty,
 
   407   val (_, lthy20) = Local_Theory.note ((Binding.empty,
 
   402     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 
   408     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 
   403 in
 
   409 in
 
   404   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 
   410   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 
   405 end
 
   411 end
 
   406 *}
 
   412 *}
 
       
   413 
   407 
   414 
   408 ML {* 
   415 ML {* 
   409 (* parsing the datatypes and declaring *)
 
   416 (* parsing the datatypes and declaring *)
 
   410 (* constructors in the local theory    *)
 
   417 (* constructors in the local theory    *)
 
   411 fun prepare_dts dt_strs lthy = 
   418 fun prepare_dts dt_strs lthy =
nominal2