--- a/Nominal/NewAlpha.thy Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-theory NewAlpha
-imports "Abs" "Perm"
-begin
-
-ML {*
-fun mk_prod_fv (t1, t2) =
-let
- val ty1 = fastype_of t1
- val ty2 = fastype_of t2
- val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
-in
- Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
-end
-*}
-
-ML {*
-fun mk_prod_alpha (t1, t2) =
-let
- val ty1 = fastype_of t1
- val ty2 = fastype_of t2
- val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
- val resT = [prodT, prodT] ---> @{typ "bool"}
-in
- Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
-end
-*}
-
-ML {*
-fun mk_binders lthy bmode args bodies =
-let
- fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
- | bind_set _ args (SOME bn, i) = bn $ (nth args i)
- fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
- | bind_lst _ args (SOME bn, i) = bn $ (nth args i)
-
- val (connect_fn, bind_fn) =
- case bmode of
- Lst => (mk_append, bind_lst)
- | Set => (mk_union, bind_set)
- | Res => (mk_union, bind_set)
-in
- foldl1 connect_fn (map (bind_fn lthy args) bodies)
-end
-*}
-
-ML {*
-fun mk_alpha_prem bmode fv alpha args args' binders binders' =
-let
- val (alpha_name, binder_ty) =
- case bmode of
- Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
- | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
- | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
- val ty = fastype_of args
- val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
- val alpha_ty = [ty, ty] ---> @{typ "bool"}
- val fv_ty = ty --> @{typ "atom set"}
-in
- HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
- Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
- $ HOLogic.mk_prod (binders, args) $ alpha $ fv $ (Bound 0) $ HOLogic.mk_prod (binders', args'))
-end
-*}
-
-ML {*
-fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
- case binder of
- (NONE, i) => []
- | (SOME bn, i) =>
- if member (op=) bodies i
- then []
- else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
-*}
-
-ML {*
-fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
-let
- fun mk_frees i =
- let
- val arg = nth args i
- val arg' = nth args' i
- val ty = fastype_of arg
- in
- if nth is_rec i
- then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
- else HOLogic.mk_eq (arg, arg')
- end
- fun mk_alpha_fv i =
- let
- val ty = fastype_of (nth args i)
- in
- case AList.lookup (op=) alpha_map ty of
- NONE => (HOLogic.eq_const ty, supp_const ty)
- | SOME (alpha, fv) => (alpha, fv)
- end
-
-in
- case bclause of
- BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
- | BC (bmode, binders, bodies) =>
- let
- val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
- val comp_fv = foldl1 mk_prod_fv fvs
- val comp_alpha = foldl1 mk_prod_alpha alphas
- val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
- val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
- val comp_binders = mk_binders lthy bmode args binders
- val comp_binders' = mk_binders lthy bmode args' binders
- val alpha_prem =
- mk_alpha_prem bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
- val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
- in
- map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
- end
-end
-*}
-
-ML {*
-fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
-let
- val arg_names = Datatype_Prop.make_tnames arg_tys
- val arg_names' = Name.variant_list arg_names arg_names
- val args = map Free (arg_names ~~ arg_tys)
- val args' = map Free (arg_names' ~~ arg_tys)
- val alpha = fst (the (AList.lookup (op=) alpha_map ty))
- val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
- val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
-in
- Library.foldr Logic.mk_implies (flat prems, concl)
-end
-*}
-
-ML {*
-fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
-let
- fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i =
- let
- val arg = nth args i
- val arg' = nth args' i
- val ty = fastype_of arg
- in
- case AList.lookup (op=) bn_args i of
- NONE => (case (AList.lookup (op=) alpha_map ty) of
- NONE => [HOLogic.mk_eq (arg, arg')]
- | SOME (alpha, _) => [alpha $ arg $ arg'])
- | SOME (NONE) => []
- | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']
- end
-in
- case bclause of
- BC (_, [], bodies) =>
- map HOLogic.mk_Trueprop
- (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
- | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
-end
-*}
-
-ML {*
-fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
-let
- val arg_names = Datatype_Prop.make_tnames arg_tys
- val arg_names' = Name.variant_list arg_names arg_names
- val args = map Free (arg_names ~~ arg_tys)
- val args' = map Free (arg_names' ~~ arg_tys)
- val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
- val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
- val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
-in
- Library.foldr Logic.mk_implies (flat prems, concl)
-end
-*}
-
-ML {*
-fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
-let
- val nth_constrs_info = nth constrs_info bn_n
- val nth_bclausess = nth bclausesss bn_n
-in
- map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
-end
-*}
-
-ML {*
-fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =
-let
- val alpha_names = prefix_dt_names descr sorts "alpha_"
- val alpha_arg_tys = all_dtyps descr sorts
- val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
- val alpha_frees = map Free (alpha_names ~~ alpha_tys)
- val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
-
- val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
- val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
- val alpha_bn_names = map (prefix "alpha_") bn_names
- val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
- val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
- val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
- val alpha_bn_map = bns ~~ alpha_bn_frees
-
- val constrs_info = all_dtyp_constrs_types descr sorts
-
- val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss
- val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
-
- val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
- (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)
- val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
-
- val (alphas, lthy') = Inductive.add_inductive_i
- {quiet_mode = true, verbose = false, alt_name = Binding.empty,
- coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
- all_alpha_names [] all_alpha_intros [] lthy
-
- val alpha_trms_loc = #preds alphas;
- val alpha_induct_loc = #raw_induct alphas;
- val alpha_intros_loc = #intrs alphas;
- val alpha_cases_loc = #elims alphas;
- val phi = ProofContext.export_morphism lthy' lthy;
-
- val alpha_trms = map (Morphism.term phi) alpha_trms_loc;
- val alpha_induct = Morphism.thm phi alpha_induct_loc;
- val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
- val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
-in
- (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
-end
-*}
-
-end