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/Fv.thy
changeset 1669 9911824a5396
parent 1658 aacab5f67333
child 1670 ed89a26b7074
equal deleted inserted replaced
1666:a99ae705b811 1669:9911824a5396 
   134      Otherwise we return: argl = argr
 
   134      Otherwise we return: argl = argr
 
   135 
   135 
   136 *)
 
   136 *)
 
   137 
   137 
   138 ML {*
 
   138 ML {*
 
       
   139 datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
 
       
   140 *}
 
       
   141 
       
   142 ML {*
 
   139 fun is_atom thy typ =
 
   143 fun is_atom thy typ =
 
   140   Sign.of_sort thy (typ, @{sort at})
 
   144   Sign.of_sort thy (typ, @{sort at})
 
   141 
   145 
   142 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
 
   146 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
 
   143   | is_atom_set thy _ = false;
 
   147   | is_atom_set _ _ = false;
 
   144 
   148 
   145 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
 
   149 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
 
   146   | is_atom_fset thy _ = false;
 
   150   | is_atom_fset _ _ = false;
 
   147 *}
 
   151 *}
 
   148 
   152 
   149 
   153 
   150 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 
   154 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 
   151 ML {*
 
   155 ML {*
 
   324 end
 
   328 end
 
   325 *}
 
   329 *}
 
   326 
   330 
   327 
   331 
   328 ML {*
 
   332 ML {*
 
   329 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, is_rec)) =
 
   333 fun alpha_bn (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, _ (*is_rec*) )) =
 
   330 let
 
   334 let
 
   331   val {descr, sorts, ...} = dt_info;
 
   335   val {descr, sorts, ...} = dt_info;
 
   332   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
   336   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
   333   val pi = Free("pi", @{typ perm})
 
       
   334   fun alpha_bn_constr (cname, dts) args_in_bn =
 
   337   fun alpha_bn_constr (cname, dts) args_in_bn =
 
   335   let
 
   338   let
 
   336     val Ts = map (typ_of_dtyp descr sorts) dts;
 
   339     val Ts = map (typ_of_dtyp descr sorts) dts;
 
   337     val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
 
   340     val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
 
   338     val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
 
   341     val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
 
   340     val args2 = map Free (names2 ~~ Ts);
 
   343     val args2 = map Free (names2 ~~ Ts);
 
   341     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 
   344     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 
   342     val rhs = HOLogic.mk_Trueprop
 
   345     val rhs = HOLogic.mk_Trueprop
 
   343       (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
 
   346       (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
 
   344     fun lhs_arg ((dt, arg_no), (arg, arg2)) =
 
   347     fun lhs_arg ((dt, arg_no), (arg, arg2)) =
 
   345       let
 
   348       case AList.lookup (op=) args_in_bn arg_no of
 
   346         val argty = fastype_of arg;
 
   349         SOME NONE => @{term True}
 
   347         val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
 
   350       | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
 
   348       in
 
   351       | NONE =>
 
   349         case AList.lookup (op=) args_in_bn arg_no of
 
   352           if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
 
   350           SOME NONE => @{term True}
 
   353           else HOLogic.mk_eq (arg, arg2)
 
   351         | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
 
       
   352         | NONE =>
 
       
   353             if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
 
       
   354             else HOLogic.mk_eq (arg, arg2)
 
       
   355       end
 
       
   356     val arg_nos = 0 upto (length dts - 1)
 
   354     val arg_nos = 0 upto (length dts - 1)
 
   357     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
 
   355     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
 
   358     val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)
 
   356     val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)
 
   359   in
 
   357   in
 
   360     eq
 
   358     eq
 
   365   ((bn, alpha_bn_free), eqs)
 
   363   ((bn, alpha_bn_free), eqs)
 
   366 end
 
   364 end
 
   367 *}
 
   365 *}
 
   368 
   366 
   369 ML {*
 
   367 ML {*
 
   370 fun alpha_bns thy dt_info alpha_frees rel_bns bns_rec =
 
   368 fun alpha_bns dt_info alpha_frees rel_bns bns_rec =
 
   371 let
 
   369 let
 
   372   val {descr, sorts, ...} = dt_info;
 
   370   val {descr, sorts, ...} = dt_info;
 
   373   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
   371   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
   374   fun mk_alphabn_free (bn, ith, _) =
 
   372   fun mk_alphabn_free (bn, ith, _) =
 
   375     let
 
   373     let
 
   379     in
 
   377     in
 
   380       (alphabn_name, alphabn_free)
 
   378       (alphabn_name, alphabn_free)
 
   381     end;
 
   379     end;
 
   382   val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free rel_bns);
 
   380   val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free rel_bns);
 
   383   val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees;
 
   381   val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees;
 
   384   val pair = split_list (map (alpha_bn thy dt_info alpha_frees bn_alphabn)
 
   382   val pair = split_list (map (alpha_bn dt_info alpha_frees bn_alphabn)
 
   385     (rel_bns ~~ (alphabn_frees ~~ bns_rec)))
 
   383     (rel_bns ~~ (alphabn_frees ~~ bns_rec)))
 
   386 in
 
   384 in
 
   387   (alphabn_names, pair)
 
   385   (alphabn_names, pair)
 
   388 end
 
   386 end
 
   389 *}
 
   387 *}
 
   420   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
 
   418   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
 
   421   val alpha_frees = map Free (alpha_names ~~ alpha_types);
 
   419   val alpha_frees = map Free (alpha_names ~~ alpha_types);
 
   422   (* We assume that a bn is either recursive or not *)
 
   420   (* We assume that a bn is either recursive or not *)
 
   423   val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
 
   421   val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
 
   424   val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
 
   422   val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
 
   425     alpha_bns thy dt_info alpha_frees bns bns_rec
 
   423     alpha_bns dt_info alpha_frees bns bns_rec
 
   426   val alpha_bn_frees = map snd bn_alpha_bns;
 
   424   val alpha_bn_frees = map snd bn_alpha_bns;
 
   427   val alpha_bn_types = map fastype_of alpha_bn_frees;
 
   425   val alpha_bn_types = map fastype_of alpha_bn_frees;
 
   428   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
 
   426   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
 
   429     let
 
   427     let
 
   430       val Ts = map (typ_of_dtyp descr sorts) dts;
 
   428       val Ts = map (typ_of_dtyp descr sorts) dts;
 
   493             ([], [], [], []) =>
 
   491             ([], [], [], []) =>
 
   494               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
 
   492               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
 
   495               else (HOLogic.mk_eq (arg, arg2))
 
   493               else (HOLogic.mk_eq (arg, arg2))
 
   496           | (_, [], [], []) => @{term True}
 
   494           | (_, [], [], []) => @{term True}
 
   497           | ([], [], [], _) => @{term True}
 
   495           | ([], [], [], _) => @{term True}
 
   498           | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) =>
 
   496           | ([], ((((SOME (bn, is_rec)), _, _), _) :: _), [], []) =>
 
   499             if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
 
   497             if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
 
   500             if is_rec then
 
   498             if is_rec then
 
   501               let
 
   499               let
 
   502                 val (rbinds, rpis) = split_list rel_in_comp_binds
 
   500                 val (rbinds, rpis) = split_list rel_in_comp_binds
 
   503                 val bound_in_nos = map (fn (_, _, i) => i) rbinds
 
   501                 val bound_in_nos = map (fn (_, _, i) => i) rbinds
 
   504                 val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
 
   502                 val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
 
   505                 val bound_args = arg :: map (nth args) bound_in_nos;
 
   503                 val bound_args = arg :: map (nth args) bound_in_nos;
 
   506                 val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
 
   504                 val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
 
   507                 fun bound_in args (_, _, i) = nth args i;
 
       
   508                 val lhs_binds = fv_binds args rbinds
 
   505                 val lhs_binds = fv_binds args rbinds
 
   509                 val lhs_arg = foldr1 HOLogic.mk_prod bound_args
 
   506                 val lhs_arg = foldr1 HOLogic.mk_prod bound_args
 
   510                 val lhs = mk_pair (lhs_binds, lhs_arg);
 
   507                 val lhs = mk_pair (lhs_binds, lhs_arg);
 
   511                 val rhs_binds = fv_binds args2 rbinds;
 
   508                 val rhs_binds = fv_binds args2 rbinds;
 
   512                 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
 
   509                 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
 
   576       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
 
   573       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
 
   577      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
 
   574      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
 
   578      (alpha_types @ alpha_bn_types)) []
 
   575      (alpha_types @ alpha_bn_types)) []
 
   579      (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
 
   576      (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
 
   580   val ordered_fvs = fv_frees @ fvbns;
 
   577   val ordered_fvs = fv_frees @ fvbns;
 
   581   val exported_fvs = map (Morphism.term (ProofContext.export_morphism lthy''' lthy)) ordered_fvs;
 
       
   582   val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 
   578   val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 
   583 in
 
   579 in
 
   584   (((all_fvs, ordered_fvs), alphas), lthy''')
 
   580   (((all_fvs, ordered_fvs), alphas), lthy''')
 
   585 end
 
   581 end
 
   586 *}
 
   582 *}
 
   619   val tys = map (domain_type o fastype_of) alpha_ts;
 
   615   val tys = map (domain_type o fastype_of) alpha_ts;
 
   620   val names = Datatype_Prop.make_tnames tys;
 
   616   val names = Datatype_Prop.make_tnames tys;
 
   621   val args = map Free (names ~~ tys);
 
   617   val args = map Free (names ~~ tys);
 
   622   fun find_alphas ty x =
 
   618   fun find_alphas ty x =
 
   623     domain_type (fastype_of x) = ty;
 
   619     domain_type (fastype_of x) = ty;
 
   624   fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg;
 
       
   625   fun refl_eq_arg (ty, arg) =
 
   620   fun refl_eq_arg (ty, arg) =
 
   626     let
 
   621     let
 
   627       val rel_alphas = filter (find_alphas ty) alphas;
 
   622       val rel_alphas = filter (find_alphas ty) alphas;
 
   628     in
 
   623     in
 
   629       map (fn x => x $ arg $ arg) rel_alphas
 
   624       map (fn x => x $ arg $ arg) rel_alphas
 
   634   (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
 
   629   (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
 
   635 end
 
   630 end
 
   636 *}
 
   631 *}
 
   637 
   632 
   638 ML {*
 
   633 ML {*
 
   639 fun reflp_tac induct eq_iff ctxt =
 
   634 fun reflp_tac induct eq_iff =
 
   640   rtac induct THEN_ALL_NEW
 
   635   rtac induct THEN_ALL_NEW
 
   641   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
 
   636   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
 
   642   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   637   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   643   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   638   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   644      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   639      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   647 
   642 
   648 ML {*
 
   643 ML {*
 
   649 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
 
   644 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
 
   650 let
 
   645 let
 
   651   val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
 
   646   val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
 
   652   val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1);
 
   647   val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
 
   653 in
 
   648 in
 
   654   HOLogic.conj_elims refl_conj
 
   649   HOLogic.conj_elims refl_conj
 
   655 end
 
   650 end
 
   656 *}
 
   651 *}
 
   657 
   652
nominal2