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 1408 b452e11e409f
parent 1407 beeaa85c9897
child 1409 25b02cc185e2
equal deleted inserted replaced
1407:beeaa85c9897 1408:b452e11e409f 
   268   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
   268   Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
 
   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 
   274 
   274 ML {*
 
   275 ML {*
 
   275 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 
   276 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 
   276 let
 
   277 let
 
   277   val thy = ProofContext.theory_of lthy
 
   278   val thy = ProofContext.theory_of lthy
 
   315   val alpha_intros = #intrs alpha;
 
   316   val alpha_intros = #intrs alpha;
 
   316   val alpha_cases_loc = #elims alpha
 
   317   val alpha_cases_loc = #elims alpha
 
   317   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
 
   318   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
 
   318   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
 
   319   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
 
   319   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 
   320   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 
       
   321   fun alpha_eqvt_tac' _ =
 
       
   322     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   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;
 
   320 in
 
   326 in
 
   321 if !restricted_nominal = 0 then
 
   327 if !restricted_nominal = 0 then
 
   322   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 
   328   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 
   323 else
 
   329 else
 
   324 let
 
   330 let
 
   325   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
   331   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 
   326   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
 
   332   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
 
   327     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
 
   333     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
 
   328   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)
 
   329   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;
 
   330   fun alpha_eqvt_tac' _ = alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy6 1
 
       
   331   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms alpha_eqvt_tac' lthy6;
 
       
   332   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
 
       
   333   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
 
   336   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
 
   334   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
 
   335     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;
 
   336   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 
   339   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
 
   337   val qty_binds = map (fn (_, b, _, _) => b) dts;
 
   340   val qty_binds = map (fn (_, b, _, _) => b) dts;
nominal2