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 1411 6b9833936281
parent 1410 5d421b327f79
child 1412 137cad9c1ce9
equal deleted inserted replaced
1410:5d421b327f79 1411:6b9833936281 
   269 end
 
   269 end
 
   270 *}
 
   270 *}
 
   271 
   271 
   272 ML {* val restricted_nominal=ref 0 *}
 
   272 ML {* val restricted_nominal=ref 0 *}
 
   273 ML {* val cheat_alpha_eqvt = ref true *}
 
   273 ML {* val cheat_alpha_eqvt = ref true *}
 
       
   274 ML {* val cheat_fv_eqvt = ref true *}
 
   274 
   275 
   275 ML {*
 
   276 ML {*
 
   276 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 
   277 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 
   277 let
 
   278 let
 
   278   val thy = ProofContext.theory_of lthy
 
   279   val thy = ProofContext.theory_of lthy
 
   322     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
   323     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
 
   323     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
 
   324     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
 
   324   val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
 
   325   val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
 
   325   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
 
   326   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
 
   326   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
   327   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
   327 in
 
   328   val fv_eqvt_tac =
 
   328 if !restricted_nominal = 0 then
 
   329     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
 
   329   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
 
   330     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
 
   330 else
 
   331   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
 
   331 let
 
       
   332   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc
 
       
   333     (build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5) lthy5;
 
       
   334   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
 
   332   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
 
   335   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
 
   333   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
 
       
   334 in
 
       
   335 if !restricted_nominal = 0 then
 
       
   336   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
 
       
   337 else
 
       
   338 let
 
   336   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
 
   339   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
 
   337   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
 
   340   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
 
   338     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
 
   341     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
 
   339   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 
   342   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 
   340   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   343   val qty_binds = map (fn (_, b, _, _) => b) dts;
nominal2