1 theory Fv

     2 imports "Nominal2_Atoms" "Abs"

     3 begin

     4 

     5 (* Bindings are given as a list which has a length being equal

     6    to the length of the number of constructors.

     7 

     8    Each element is a list whose length is equal to the number

     9    of arguents.

    10 

    11    Every element specifies bindings of this argument given as

    12    a tuple: function, bound argument.

    13 

    14   Eg:

    15 nominal_datatype

    16 

    17    C1

    18  | C2 x y z bind x in z

    19  | C3 x y z bind f x in z bind g y in z

    20 

    21 yields:

    22 [

    23  [],

    24  [[], [], [(NONE, 0)]],

    25  [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]

    26 

    27 A SOME binding has to have a function returning an atom set,

    28 and a NONE binding has to be on an argument that is an atom

    29 or an atom set.

    30 

    31 How the procedure works:

    32   For each of the defined datatypes,

    33   For each of the constructors,

    34   It creates a union of free variables for each argument.

    35 

    36   For an argument the free variables are the variables minus

    37   bound variables.

    38 

    39   The variables are:

    40     For an atom, a singleton set with the atom itself.

    41     For an atom set, the atom set itself.

    42     For a recursive argument, the appropriate fv function applied to it.

    43     (* TODO: This one is not implemented *)

    44     For other arguments it should be an appropriate fv function stored

    45       in the database.

    46   The bound variables are a union of results of all bindings that

    47   involve the given argument. For a paricular binding the result is:

    48     For a function applied to an argument this function with the argument.

    49     For an atom, a singleton set with the atom itself.

    50     For an atom set, the atom set itself.

    51     For a recursive argument, the appropriate fv function applied to it.

    52     (* TODO: This one is not implemented *)

    53     For other arguments it should be an appropriate fv function stored

    54       in the database.

    55 *)

    56 

    57 ML {*

    58   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);

    59   (* TODO: It is the same as one in 'nominal_atoms' *)

    60   fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});

    61   val noatoms = @{term "{} :: atom set"};

    62   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];

    63   fun mk_union sets =

    64     fold (fn a => fn b =>

    65       if a = noatoms then b else

    66       if b = noatoms then a else

    67       HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms;

    68   fun mk_diff a b =

    69     if b = noatoms then a else

    70     if b = a then noatoms else

    71     HOLogic.mk_binop @{const_name minus} (a, b);

    72   fun mk_atoms t =

    73     let

    74       val ty = fastype_of t;

    75       val atom_ty = HOLogic.dest_setT ty --> @{typ atom};

    76       val img_ty = atom_ty --> ty --> @{typ "atom set"};

    77     in

    78       (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)

    79     end;

    80   (* Copy from Term *)

    81   fun is_funtype (Type ("fun", [_, _])) = true

    82     | is_funtype _ = false;

    83   (* Similar to one in USyntax *)

    84   fun mk_pair (fst, snd) =

    85     let val ty1 = fastype_of fst

    86       val ty2 = fastype_of snd

    87       val c = HOLogic.pair_const ty1 ty2

    88     in c $ fst $ snd

    89     end;

    90 

    91 *}

    92 

    93 (* TODO: Notice datatypes without bindings and replace alpha with equality *)

    94 ML {*

    95 (* Currently needs just one full_tname to access Datatype *)

    96 fun define_fv_alpha full_tname bindsall lthy =

    97 let

    98   val thy = ProofContext.theory_of lthy;

    99   val {descr, ...} = Datatype.the_info thy full_tname;

   100   val sorts = []; (* TODO *)

   101   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

   102   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>

   103     "fv_" ^ name_of_typ (nth_dtyp i)) descr);

   104   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;

   105   val fv_frees = map Free (fv_names ~~ fv_types);

   106   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>

   107     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);

   108   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;

   109   val alpha_frees = map Free (alpha_names ~~ alpha_types);

   110   fun fv_alpha_constr i (cname, dts) bindcs =

   111     let

   112       val Ts = map (typ_of_dtyp descr sorts) dts;

   113       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);

   114       val args = map Free (names ~~ Ts);

   115       val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);

   116       val args2 = map Free (names2 ~~ Ts);

   117       val c = Const (cname, Ts ---> (nth_dtyp i));

   118       val fv_c = nth fv_frees i;

   119       val alpha = nth alpha_frees i;

   120       fun fv_bind args (NONE, i) =

   121             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else

   122             (* TODO we assume that all can be 'atomized' *)

   123             if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else

   124             mk_single_atom (nth args i)

   125         | fv_bind args (SOME f, i) = f $ (nth args i);

   126       fun fv_arg ((dt, x), bindxs) =

   127         let

   128           val arg =

   129             if is_rec_type dt then nth fv_frees (body_index dt) $ x else

   130             (* TODO: we just assume everything can be 'atomized' *)

   131             if (is_funtype o fastype_of) x then mk_atoms x else

   132             HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]

   133           val sub = mk_union (map (fv_bind args) bindxs)

   134         in

   135           mk_diff arg sub

   136         end;

   137       val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq

   138         (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))

   139       val alpha_rhs =

   140         HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));

   141       fun alpha_arg ((dt, bindxs), (arg, arg2)) =

   142         if bindxs = [] then (

   143           if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)

   144           else (HOLogic.mk_eq (arg, arg2)))

   145         else

   146           if is_rec_type dt then let

   147             (* THE HARD CASE *)

   148             val lhs_binds = mk_union (map (fv_bind args) bindxs);

   149             val lhs = mk_pair (lhs_binds, arg);

   150             val rhs_binds = mk_union (map (fv_bind args2) bindxs);

   151             val rhs = mk_pair (rhs_binds, arg2);

   152             val alpha = nth alpha_frees (body_index dt);

   153             val fv = nth fv_frees (body_index dt);

   154             val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;

   155             val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre

   156           in

   157             HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)

   158           (* TODO Add some test that is makes sense *)

   159           end else @{term "True"}

   160       val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))

   161       val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)

   162     in

   163       (fv_eq, alpha_eq)

   164     end;

   165   fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;

   166   val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))

   167   val add_binds = map (fn x => (Attrib.empty_binding, x))

   168   val (fvs, lthy') = (Primrec.add_primrec

   169     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)

   170   val (alphas, lthy'') = (Inductive.add_inductive_i

   171      {quiet_mode = false, verbose = true, alt_name = Binding.empty,

   172       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}

   173      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []

   174      (add_binds alpha_eqs) [] lthy')

   175 in

   176   ((fvs, alphas), lthy'')

   177 end

   178 *}

   179 

   180 (* tests

   181 atom_decl name

   182 

   183 datatype ty =

   184   Var "name set"

   185 

   186 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}

   187 

   188 local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}

   189 print_theorems

   190 

   191 

   192 datatype rtrm1 =

   193   rVr1 "name"

   194 | rAp1 "rtrm1" "rtrm1"

   195 | rLm1 "name" "rtrm1"        --"name is bound in trm1"

   196 | rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"

   197 and bp =

   198   BUnit

   199 | BVr "name"

   200 | BPr "bp" "bp"

   201 

   202 (* to be given by the user *)

   203 

   204 primrec 

   205   bv1

   206 where

   207   "bv1 (BUnit) = {}"

   208 | "bv1 (BVr x) = {atom x}"

   209 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"

   210 

   211 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}

   212 

   213 local_setup {* define_fv_alpha "Fv.rtrm1"

   214   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],

   215    [[], [[]], [[], []]]] *}

   216 print_theorems

   217 *)

   218 

   219 

   220 ML {*

   221 fun alpha_inj_tac dist_inj intrs elims =

   222   SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'

   223   (rtac @{thm iffI} THEN' RANGE [

   224      (eresolve_tac elims THEN_ALL_NEW

   225        asm_full_simp_tac (HOL_ss addsimps dist_inj)

   226      ),

   227      asm_full_simp_tac (HOL_ss addsimps intrs)])

   228 *}

   229 

   230 ML {*

   231 fun build_alpha_inj_gl thm =

   232   let

   233     val prop = prop_of thm;

   234     val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);

   235     val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);

   236     fun list_conj l = foldr1 HOLogic.mk_conj l;

   237   in

   238     if hyps = [] then concl

   239     else HOLogic.mk_eq (concl, list_conj hyps)

   240   end;

   241 *}

   242 

   243 ML {*

   244 fun build_alpha_inj intrs dist_inj elims ctxt =

   245 let

   246   val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;

   247   val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;

   248   fun tac _ = alpha_inj_tac dist_inj intrs elims 1;

   249   val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;

   250 in

   251   Variable.export ctxt' ctxt thms

   252 end

   253 *}

   254 

   255 ML {*

   256 fun build_alpha_refl_gl alphas (x, y, z) =

   257 let

   258   fun build_alpha alpha =

   259     let

   260       val ty = domain_type (fastype_of alpha);

   261       val var = Free(x, ty);

   262       val var2 = Free(y, ty);

   263       val var3 = Free(z, ty);

   264       val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);

   265       val transp = HOLogic.mk_imp (alpha $ var $ var2,

   266         HOLogic.mk_all (z, ty,

   267           HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))

   268     in

   269       ((alpha $ var $ var), (symp, transp))

   270     end;

   271   val (refl_eqs, eqs) = split_list (map build_alpha alphas)

   272   val (sym_eqs, trans_eqs) = split_list eqs

   273   fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l

   274 in

   275   (conj refl_eqs, (conj sym_eqs, conj trans_eqs))

   276 end

   277 *}

   278 

   279 ML {*

   280 fun reflp_tac induct inj =

   281   rtac induct THEN_ALL_NEW

   282   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW

   283   TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   284   (rtac @{thm exI[of _ "0 :: perm"]} THEN'

   285    asm_full_simp_tac (HOL_ss addsimps

   286      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))

   287 *}

   288 

   289 ML {*

   290 fun symp_tac induct inj eqvt =

   291   ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW

   292   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW

   293   TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   294   (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)

   295 *}

   296 

   297 ML {*

   298 fun imp_elim_tac case_rules =

   299   Subgoal.FOCUS (fn {concl, context, ...} =>

   300     case term_of concl of

   301       _ $ (_ $ asm $ _) =>

   302         let

   303           fun filter_fn case_rule = (

   304             case Logic.strip_assums_hyp (prop_of case_rule) of

   305               ((_ $ asmc) :: _) =>

   306                 let

   307                   val thy = ProofContext.theory_of context

   308                 in

   309                   Pattern.matches thy (asmc, asm)

   310                 end

   311             | _ => false)

   312           val matching_rules = filter filter_fn case_rules

   313         in

   314          (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1

   315         end

   316     | _ => no_tac

   317   )

   318 *}

   319 

   320 ML {*

   321 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =

   322   ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW

   323   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW

   324   (

   325     asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN'

   326     TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   327     (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt])

   328   )

   329 *}

   330 

   331 lemma transp_aux:

   332   "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"

   333   unfolding transp_def

   334   by blast

   335 

   336 ML {*

   337 fun equivp_tac reflps symps transps =

   338   simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})

   339   THEN' rtac conjI THEN' rtac allI THEN'

   340   resolve_tac reflps THEN'

   341   rtac conjI THEN' rtac allI THEN' rtac allI THEN'

   342   resolve_tac symps THEN'

   343   rtac @{thm transp_aux} THEN' resolve_tac transps

   344 *}

   345 

   346 ML {*

   347 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =

   348 let

   349   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;

   350   val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)

   351   fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1;

   352   fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;

   353   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;

   354   val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';

   355   val symt = Goal.prove ctxt' [] [] symg symp_tac';

   356   val transt = Goal.prove ctxt' [] [] transg transp_tac';

   357   val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]

   358   val reflts = HOLogic.conj_elims refltg

   359   val symts = HOLogic.conj_elims symtg

   360   val transts = HOLogic.conj_elims transtg

   361   fun equivp alpha =

   362     let

   363       val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})

   364       val goal = @{term Trueprop} $ (equivp $ alpha)

   365       fun tac _ = equivp_tac reflts symts transts 1

   366     in

   367       Goal.prove ctxt [] [] goal tac

   368     end

   369 in

   370   map equivp alphas

   371 end

   372 *}

   373 

   374 (*

   375 Tests:

   376 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}

   377 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})

   378 

   379 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}

   380 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})

   381 

   382 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}

   383 by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})

   384 

   385 lemma alpha1_equivp:

   386   "equivp alpha_rtrm1"

   387   "equivp alpha_bp"

   388 apply (tactic {*

   389   (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})

   390   THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'

   391   resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})

   392   THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'

   393   resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}

   394   THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})

   395 )

   396 1 *})

   397 done*)

   398 

   399 end