18 

    19 text {* TEST *}

    20 

    21 

    22 ML {*

    23 (* adds a freshness condition to the assumptions *)

    24 fun mk_ecase_prems lthy c (params, prems, concl) bclauses =

    25   let

    26     val tys = map snd params

    27     val binders = get_all_binders bclauses

    28    

    29     fun prep_binder (opt, i) = 

    30       let

    31         val t = Bound (length tys - i - 1)

    32       in

    33         case opt of

    34           NONE => setify_ty lthy (nth tys i) t 

    35         | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   

    36       end 

    37 

    38     val prems' = 

    39       case binders of

    40         [] => prems                        (* case: no binders *)

    41       | _ => binders                       (* case: binders *) 

    42           |> map prep_binder

    43           |> fold_union_env tys

    44           |> (fn t => mk_fresh_star t c)

    45           |> (fn t => HOLogic.mk_Trueprop t :: prems)

    46   in

    47     mk_full_horn params prems' concl

    48   end  

    49 *}

    50 

    51 

    52 ML {*

    53 (* derives the freshness theorem that there exists a p, such that 

    54    (p o as) #* (c, t1,\<dots>, tn) *)

    55 fun fresh_thm ctxt c parms binders bn_finite_thms =

    56   let

    57     fun prep_binder (opt, i) = 

    58       case opt of

    59         NONE => setify ctxt (nth parms i) 

    60       | SOME bn => to_set (bn $ (nth parms i))  

    61 

    62     fun prep_binder2 (opt, i) = 

    63       case opt of

    64         NONE => atomify ctxt (nth parms i)

    65       | SOME bn => bn $ (nth parms i) 

    66 

    67     val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))

    68     val lhs = binders

    69       |> map prep_binder

    70       |> fold_union

    71       |> mk_perm (Bound 0)

    72 

    73     val goal = mk_fresh_star lhs rhs

    74       |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))

    75       |> HOLogic.mk_Trueprop   

    76  

    77     val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} 

    78       @ @{thms finite.intros finite_Un finite_set finite_fset}  

    79   in

    80     Goal.prove ctxt [] [] goal

    81       (K (HEADGOAL (rtac @{thm at_set_avoiding1}

    82           THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))

    83   end

    84 *} 

    85 

    86 ML {*

    87 fun abs_const bmode ty =

    88   let

    89     val (const_name, binder_ty, abs_ty) = 

    90       case bmode of

    91         Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})

    92       | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})

    93       | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})

    94   in

    95     Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))

    96   end

    97 

    98 fun mk_abs bmode trm1 trm2 =

    99   abs_const bmode (fastype_of trm2) $ trm1 $ trm2  

   100 

   101 fun is_abs_eq thm =

   102   let

   103     fun is_abs trm =

   104       case (head_of trm) of

   105         Const (@{const_name "Abs_set"}, _) => true

   106       | Const (@{const_name "Abs_lst"}, _) => true

   107       | Const (@{const_name "Abs_res"}, _) => true

   108       | _ => false

   109   in 

   110     thm |> prop_of 

   111         |> HOLogic.dest_Trueprop

   112         |> HOLogic.dest_eq

   113         |> fst

   114         |> is_abs

   115   end

   116 *}

   117 

   118 

   119 

   120 ML {*

   121 (* derives an abs_eq theorem of the form 

   122 

   123    Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 

   124    Exists q. [as].x = [q o as].(q o x)  for recursive binders

   125 *)

   126 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns

   127   (bclause as (BC (bmode, binders, bodies))) =

   128   case binders of

   129     [] => [] 

   130   | _ =>

   131       let

   132         val rec_flag = is_recursive_binder bclause

   133         val binder_trm = comb_binders ctxt bmode parms binders

   134         val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)

   135 

   136         val abs_lhs = mk_abs bmode binder_trm body_trm

   137         val abs_rhs = 

   138           if rec_flag

   139           then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)

   140           else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)

   141         

   142         val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)

   143         val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 

   144 

   145         val goal = HOLogic.mk_conj (abs_eq, peq)

   146           |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))

   147           |> HOLogic.mk_Trueprop  

   148  

   149         val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}

   150           @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset

   151           fresh_star_set} @ @{thms finite.intros finite_fset}

   152   

   153         val tac1 = 

   154           if rec_flag

   155           then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}

   156           else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}

   157         

   158         val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] 

   159      in

   160        [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))

   161          |> (if rec_flag

   162              then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []

   163              else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]

   164      end

   165 *}

   166 

   167 

   168 

   169 lemma setify:

   170   shows "xs = ys \<Longrightarrow> set xs = set ys" 

   171   by simp

   172 

   173 ML {*

   174 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 

   175   prems bclausess qexhaust_thm =

   176   let

   177     fun aux_tac prem bclauses =

   178       case (get_all_binders bclauses) of

   179         [] => EVERY' [rtac prem, atac]

   180       | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>  

   181           let

   182             val parms = map (term_of o snd) params

   183             val fthm = fresh_thm ctxt c parms binders bn_finite_thms 

   184   

   185             val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}

   186             val (([(_, fperm)], fprops), ctxt') = Obtain.result

   187               (K (EVERY1 [etac exE, 

   188                           full_simp_tac (HOL_basic_ss addsimps ss), 

   189                           REPEAT o (etac @{thm conjE})])) [fthm] ctxt 

   190   

   191             val abs_eq_thms = flat 

   192              (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)

   193 

   194             val ((_, eqs), ctxt'') = Obtain.result

   195               (K (EVERY1 

   196                    [ REPEAT o (etac @{thm exE}), 

   197                      REPEAT o (etac @{thm conjE}),

   198                      REPEAT o (dtac @{thm setify}),

   199                      full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' 

   200 

   201             val (abs_eqs, peqs) = split_filter is_abs_eq eqs

   202 

   203             val fprops' = 

   204               map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops

   205               @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops

   206 

   207             (* for freshness conditions *) 

   208             val tac1 = SOLVED' (EVERY'

   209               [ simp_tac (HOL_basic_ss addsimps peqs),

   210                 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),

   211                 conj_tac (DETERM o resolve_tac fprops') ]) 

   212 

   213             (* for equalities between constructors *)

   214             val tac2 = SOLVED' (EVERY' 

   215               [ rtac (@{thm ssubst} OF prems),

   216                 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),

   217                 rewrite_goal_tac (map safe_mk_equiv abs_eqs),

   218                 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) 

   219 

   220             (* proves goal "P" *)

   221             val side_thm = Goal.prove ctxt'' [] [] (term_of concl)

   222               (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))

   223               |> singleton (ProofContext.export ctxt'' ctxt)  

   224           in

   225             rtac side_thm 1 

   226           end) ctxt

   227   in

   228     EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]

   229   end

   230 *}

   231 

   232 ML {*

   233 fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns

   234   perm_bn_alphas =

   235   let

   236     val ((_, exhausts'), lthy') = Variable.import true exhausts lthy 

   237 

   238     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'

   239     val c = Free (c, TFree (a, @{sort fs}))

   240 

   241     val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)

   242       |> map prop_of

   243       |> map Logic.strip_horn

   244       |> split_list

   245 

   246     val ecases' = (map o map) strip_full_horn ecases

   247 

   248     val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss

   249    

   250     fun tac bclausess exhaust {prems, context} =

   251       case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 

   252         prems bclausess exhaust

   253 

   254     fun prove prems bclausess exhaust concl =

   255       Goal.prove lthy'' [] prems concl (tac bclausess exhaust)

   256   in

   257     map4 prove premss bclausesss exhausts' main_concls

   258     |> ProofContext.export lthy'' lthy

   259   end

   260 *}

   261