1 theory Lambda

     2 imports "../Nominal2" 

     3 begin

     4 

     5 

     6 atom_decl name

     7 

     8 nominal_datatype lam =

     9   Var "name"

    10 | App "lam" "lam"

    11 | Lam x::"name" l::"lam"  bind x in l

    12 

    13 thm lam.distinct

    14 thm lam.induct

    15 thm lam.exhaust lam.strong_exhaust

    16 thm lam.fv_defs

    17 thm lam.bn_defs

    18 thm lam.perm_simps

    19 thm lam.eq_iff

    20 thm lam.fv_bn_eqvt

    21 thm lam.size_eqvt

    22 

    23 ML {*

    24 fun mk_cminus p = Thm.capply @{cterm "uminus::perm \<Rightarrow> perm"} p 

    25 

    26 fun minus_permute_intro_tac p = 

    27   rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})

    28 

    29 fun minus_permute_elim p thm = 

    30   thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})

    31 *}

    32 

    33 ML {*

    34 fun real_head_of (@{term Trueprop} $ t) = real_head_of t

    35   | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t

    36   | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t

    37   | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t

    38   | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t

    39   | real_head_of t = head_of t  

    40 *}

    41 

    42 ML {* 

    43 fun mk_vc_compat (avoid, avoid_trm) prems concl_args params =

    44   let

    45     fun aux arg = arg

    46       |> mk_fresh_star avoid_trm 

    47       |> HOLogic.mk_Trueprop

    48       |> (curry Logic.list_implies) prems

    49       |> (curry list_all_free) params

    50   in 

    51     if null avoid then [] else map aux concl_args

    52   end

    53 *}

    54 

    55 ML {*

    56 fun map_term prop f trm =

    57   if prop trm 

    58   then f trm

    59   else case trm of

    60     (t1 $ t2) => map_term prop f t1 $ map_term prop f t2

    61   | Abs (x, T, t) => Abs (x, T, map_term prop f t)

    62   | _ => trm

    63 *}

    64 

    65 ML {*

    66 fun add_p_c p (c, c_ty) trm =

    67   let

    68     val (P, args) = strip_comb trm

    69     val (P_name, P_ty) = dest_Free P

    70     val (ty_args, bool) = strip_type P_ty

    71     val args' = map (mk_perm p) args

    72   in

    73     list_comb (Free (P_name, (c_ty :: ty_args) ---> bool),  c :: args')

    74     |> (fn t => HOLogic.all_const c_ty $ lambda c t )

    75     |> (fn t => HOLogic.all_const @{typ perm} $  lambda p t)

    76   end

    77 *}

    78 

    79 ML {*

    80 fun induct_forall_const T = Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool})

    81 fun mk_induct_forall (a, T) t =  induct_forall_const T $ Abs (a, T, t)

    82 *}

    83 

    84 ML {*

    85 fun add_c_prop qnt Ps (c, c_name, c_ty) trm =

    86   let

    87     fun add t = 

    88       let

    89         val (P, args) = strip_comb t

    90         val (P_name, P_ty) = dest_Free P

    91         val (ty_args, bool) = strip_type P_ty

    92         val args' = args

    93           |> qnt ? map (incr_boundvars 1)

    94       in

    95         list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args')

    96         |> qnt ? mk_induct_forall (c_name, c_ty)

    97       end

    98   in

    99     map_term (member (op =) Ps o head_of) add trm

   100   end

   101 *}

   102 

   103 ML {*

   104 fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) =

   105   let

   106     val prems' = prems

   107       |> map (incr_boundvars 1) 

   108       |> map (add_c_prop true Ps (Bound 0, c_name, c_ty))

   109 

   110     val avoid_trm' = avoid_trm

   111       |> (curry list_abs_free) (params @ [(c_name, c_ty)])

   112       |> strip_abs_body

   113       |> (fn t => mk_fresh_star_ty c_ty t (Bound 0))

   114       |> HOLogic.mk_Trueprop

   115 

   116     val prems'' = 

   117       if null avoid 

   118       then prems' 

   119       else avoid_trm' :: prems'

   120 

   121     val concl' = concl

   122       |> incr_boundvars 1 

   123       |> add_c_prop false Ps (Bound 0, c_name, c_ty)  

   124   in

   125     mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'

   126   end

   127 *}

   128 

   129 

   130 ML {*

   131 fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2)

   132   | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2)

   133   | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2)

   134   | same_name _ = false

   135 *}

   136 

   137 ML {*

   138 (* local abbreviations *)

   139 fun eqvt_stac ctxt = Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel} []  

   140 fun eqvt_srule ctxt = Nominal_Permeq.eqvt_strict_rule ctxt @{thms permute_minus_cancel} []  

   141 *}

   142 

   143 ML {*

   144 val all_elims = 

   145   let

   146      fun spec' ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}

   147   in

   148     fold (fn ct => fn th => th RS spec' ct)

   149   end

   150 *}

   151 

   152 ML {*

   153 fun helper_tac flag prm p ctxt =

   154   Subgoal.SUBPROOF (fn {context, prems, ...} =>

   155     let

   156       val prems' = prems

   157         |> map (minus_permute_elim p)

   158         |> map (eqvt_srule context)

   159      

   160       val prm' = (prems' MRS prm)

   161         |> flag ? (all_elims [p])

   162         |> flag ? (simplify (HOL_basic_ss addsimps @{thms permute_minus_cancel}))

   163     in

   164       simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def })) 1

   165     end) ctxt

   166 *}

   167 

   168 ML {*

   169 fun non_binder_tac prem intr_cvars Ps ctxt = 

   170   Subgoal.SUBPROOF (fn {context, params, prems, ...} =>

   171     let

   172       val thy = ProofContext.theory_of context

   173       val (prms, p, _) = split_last2 (map snd params)

   174       val prm_tys = map (fastype_of o term_of) prms

   175       val cperms = map (cterm_of thy o perm_const) prm_tys

   176       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 

   177       val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem

   178 

   179       (* for inductive-premises*)

   180       fun tac1 prm = helper_tac true prm p context

   181 

   182       (* for non-inductive premises *)   

   183       fun tac2 prm =  

   184         EVERY' [ minus_permute_intro_tac p, 

   185                  eqvt_stac context, 

   186                  helper_tac false prm p context ]

   187 

   188       fun select prm (t, i) =

   189         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i

   190     in

   191       EVERY1 [rtac prem', RANGE (map (SUBGOAL o select) prems) ]

   192     end) ctxt

   193 *}

   194 

   195 ML {*

   196 fun binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trms ctxt = 

   197   Subgoal.FOCUS (fn {context, params, ...} =>

   198     let

   199       val thy = ProofContext.theory_of context

   200       val (prms, p, _) = split_last2 (map snd params)

   201       val prm_tys = map (fastype_of o term_of) prms

   202       val cperms = map (cterm_of thy o perm_const) prm_tys

   203       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 

   204       val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem

   205     in

   206       Skip_Proof.cheat_tac thy

   207       (* EVERY1 [rtac prem'] *)  

   208     end) ctxt

   209 *}

   210 

   211 ML {*

   212 fun case_tac ctxt fresh_thms Ps avoid avoid_trm intr_cvars prem =

   213   let

   214     val tac1 = non_binder_tac prem intr_cvars Ps ctxt

   215     val tac2 = binder_tac prem intr_cvars Ps fresh_thms avoid avoid_trm ctxt

   216   in 

   217     EVERY' [ rtac @{thm allI}, rtac @{thm allI}, eqvt_stac ctxt,

   218              if null avoid then tac1 else tac2 ]

   219   end

   220 *}

   221 

   222 ML {*

   223 fun tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars {prems, context} =

   224   let

   225     val cases_tac = map4 (case_tac context fresh_thms Ps) avoids avoid_trms intr_cvars prems

   226   in 

   227     EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]

   228   end

   229 *}

   230 

   231 ML {*

   232 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (\<And>c. Q ==> P (0::perm) c)" by simp}

   233 *}

   234 

   235 ML {*

   236 fun prove_strong_inductive rule_names avoids raw_induct intrs ctxt =

   237   let

   238     val thy = ProofContext.theory_of ctxt

   239     val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt

   240 

   241     val (ind_prems, ind_concl) = raw_induct'

   242       |> prop_of

   243       |> Logic.strip_horn

   244       |>> map strip_full_horn

   245     val params = map (fn (x, _, _) => x) ind_prems

   246     val param_trms = (map o map) Free params  

   247 

   248     val intr_vars_tys = map (fn t => rev (Term.add_vars (prop_of t) [])) intrs

   249     val intr_vars = (map o map) fst intr_vars_tys

   250     val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms

   251     val intr_cvars = (map o map) (cterm_of thy o Var) intr_vars_tys

   252 

   253     val (intr_prems, intr_concls) = intrs

   254       |> map prop_of

   255       |> map2 subst_Vars intr_vars_substs

   256       |> map Logic.strip_horn

   257       |> split_list

   258 

   259     val intr_concls_args = map (snd o strip_comb o HOLogic.dest_Trueprop) intr_concls 

   260       

   261     val avoid_trms = avoids

   262       |> (map o map) (setify ctxt') 

   263       |> map fold_union

   264 

   265     val vc_compat_goals = 

   266       map4 mk_vc_compat (avoids ~~ avoid_trms) intr_prems intr_concls_args params

   267 

   268     val ([c_name, a, p], ctxt'') = Variable.variant_fixes ["c", "'a", "p"] ctxt'

   269     val c_ty = TFree (a, @{sort fs})

   270     val c = Free (c_name, c_ty)

   271     val p = Free (p, @{typ perm})

   272 

   273     val (preconds, ind_concls) = ind_concl

   274       |> HOLogic.dest_Trueprop

   275       |> HOLogic.dest_conj 

   276       |> map HOLogic.dest_imp

   277       |> split_list

   278 

   279     val Ps = map (fst o strip_comb) ind_concls

   280 

   281     val ind_concl' = ind_concls

   282       |> map (add_p_c p (c, c_ty))

   283       |> (curry (op ~~)) preconds  

   284       |> map HOLogic.mk_imp

   285       |> fold_conj

   286       |> HOLogic.mk_Trueprop

   287 

   288     val ind_prems' = ind_prems

   289       |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms)   

   290 

   291     fun after_qed ctxt_outside fresh_thms ctxt = 

   292       let

   293         val thms = Goal.prove ctxt [] ind_prems' ind_concl' 

   294           (tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars) 

   295           |> singleton (ProofContext.export ctxt ctxt_outside)

   296           |> Datatype_Aux.split_conj_thm

   297           |> map (fn thm => thm RS normalise)

   298           |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) 

   299           |> map (Drule.rotate_prems (length ind_prems'))

   300           |> map zero_var_indexes

   301 

   302         val _ = tracing ("RESULTS\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) thms))

   303       in

   304         ctxt

   305       end 

   306   in

   307     Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt''

   308   end

   309 *}

   310 

   311 ML {*

   312 fun prove_strong_inductive_cmd (pred_name, avoids) ctxt =

   313   let

   314     val thy = ProofContext.theory_of ctxt;

   315     val ({names, ...}, {raw_induct, intrs, ...}) =

   316       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name);

   317 

   318     val rule_names = 

   319       hd names

   320       |> the o Induct.lookup_inductP ctxt

   321       |> fst o Rule_Cases.get

   322       |> map fst

   323 

   324     val _ = (case duplicates (op = o pairself fst) avoids of

   325         [] => ()

   326       | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)))

   327 

   328     val _ = (case subtract (op =) rule_names (map fst avoids) of

   329         [] => ()

   330       | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs))

   331 

   332     val avoids_ordered = order_default (op =) [] rule_names avoids

   333       

   334     fun read_avoids avoid_trms intr =

   335       let

   336         (* fixme hack *)

   337         val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt

   338         val trms = map (term_of o snd) ctrms

   339         val ctxt'' = fold Variable.declare_term trms ctxt' 

   340       in

   341         map (Syntax.read_term ctxt'') avoid_trms 

   342       end 

   343 

   344     val avoid_trms = map2 read_avoids avoids_ordered intrs

   345   in

   346     prove_strong_inductive rule_names avoid_trms raw_induct intrs ctxt

   347   end

   348 *}

   349 

   350 ML {*

   351 (* outer syntax *)

   352 local

   353   structure P = Parse;

   354   structure S = Scan

   355   

   356   val _ = Keyword.keyword "avoids"

   357 

   358   val single_avoid_parser = 

   359     P.name -- (P.$$$ ":" |-- P.and_list1 P.term)

   360 

   361   val avoids_parser = 

   362     S.optional (P.$$$ "avoids" |-- P.enum1 "|" single_avoid_parser) []

   363 

   364   val main_parser = P.xname -- avoids_parser

   365 in

   366   val _ =

   367   Outer_Syntax.local_theory_to_proof "nominal_inductive"

   368     "prove strong induction theorem for inductive predicate involving nominal datatypes"

   369       Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd)

   370 end

   371 *}

   372 

   373 inductive

   374   Acc :: "('a::pt \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"

   375 where

   376   AccI: "(\<And>y. R y x \<Longrightarrow> Acc R y) \<Longrightarrow> Acc R x"

   377 

   378 (*

   379 equivariance Acc

   380 *)

   381 

   382 lemma Acc_eqvt [eqvt]:

   383   fixes p::"perm"

   384   assumes a: "Acc R x"

   385   shows "Acc (p \<bullet> R) (p \<bullet> x)"

   386 using a

   387 apply(induct)

   388 apply(rule AccI)

   389 apply(rotate_tac 1)

   390 apply(drule_tac x="-p \<bullet> y" in meta_spec)

   391 apply(simp)

   392 apply(drule meta_mp)

   393 apply(rule_tac p="p" in permute_boolE)

   394 apply(perm_simp add: permute_minus_cancel)

   395 apply(assumption)

   396 apply(assumption)

   397 done

   398  

   399 

   400 nominal_inductive Acc .

   401 

   402 section {* Typing *}

   403 

   404 nominal_datatype ty =

   405   TVar string

   406 | TFun ty ty ("_ \<rightarrow> _") 

   407 

   408 lemma ty_fresh:

   409   fixes x::"name"

   410   and   T::"ty"

   411   shows "atom x \<sharp> T"

   412 apply (nominal_induct T rule: ty.strong_induct)

   413 apply (simp_all add: ty.fresh pure_fresh)

   414 done

   415 

   416 

   417 

   418 inductive

   419   valid :: "(name \<times> ty) list \<Rightarrow> bool"

   420 where

   421   "valid []"

   422 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"

   423 

   424 inductive

   425   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 

   426 where

   427     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

   428   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"

   429   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"

   430 

   431 thm typing.intros

   432 thm typing.induct

   433 

   434 

   435 

   436 equivariance valid

   437 equivariance typing

   438 

   439 

   440 nominal_inductive typing

   441   avoids t_Lam: "x"

   442   apply -

   443   apply(simp_all add: fresh_star_def ty_fresh lam.fresh)?

   444   done

   445 

   446 

   447 

   448 lemma

   449   fixes c::"'a::fs"

   450   assumes a: "\<Gamma> \<turnstile> t : T" 

   451   and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"

   452   and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> 

   453            \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"

   454   and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>{atom x} \<sharp>* c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> 

   455            \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"

   456   shows "P c \<Gamma> t T"

   457 proof -

   458   from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"

   459   proof (induct)

   460     case (t_Var \<Gamma> x T p c)

   461     then show ?case

   462       apply -

   463       apply(perm_strict_simp)

   464       thm a1

   465       apply(rule a1)

   466       apply(drule_tac p="p" in permute_boolI)

   467       apply(perm_strict_simp add: permute_minus_cancel)

   468       apply(assumption)

   469       apply(rotate_tac 1)

   470       apply(drule_tac p="p" in permute_boolI)

   471       apply(perm_strict_simp add: permute_minus_cancel)

   472       apply(assumption)

   473       done

   474   next

   475     case (t_App \<Gamma> t1 T1 T2 t2 p c)

   476     then show ?case

   477       apply -

   478       apply(perm_strict_simp)

   479       apply(rule a2)

   480       apply(drule_tac p="p" in permute_boolI)

   481       apply(perm_strict_simp add: permute_minus_cancel)

   482       apply(assumption)

   483       apply(assumption)

   484       apply(rotate_tac 2)

   485       apply(drule_tac p="p" in permute_boolI)

   486       apply(perm_strict_simp add: permute_minus_cancel)

   487       apply(assumption)

   488       apply(assumption)

   489       done

   490   next

   491     case (t_Lam x \<Gamma> T1 t T2 p c)

   492     then show ?case

   493       apply -

   494       apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 

   495         supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")

   496       apply(erule exE)

   497       apply(rule_tac t="p \<bullet> \<Gamma>" and  s="(q + p) \<bullet> \<Gamma>" in subst)

   498       apply(simp only: permute_plus)

   499       apply(rule supp_perm_eq)

   500       apply(simp add: supp_Pair fresh_star_Un)

   501       apply(rule_tac t="p \<bullet> Lam x t" and  s="(q + p) \<bullet> Lam x t" in subst)

   502       apply(simp only: permute_plus)

   503       apply(rule supp_perm_eq)

   504       apply(simp add: supp_Pair fresh_star_Un)

   505       apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)

   506       apply(simp only: permute_plus)

   507       apply(rule supp_perm_eq)

   508       apply(simp add: supp_Pair fresh_star_Un)

   509       apply(simp (no_asm) only: eqvts)

   510       apply(rule a3)

   511       apply(simp only: eqvts permute_plus)

   512       apply(rule_tac p="- (q + p)" in permute_boolE)

   513       apply(perm_strict_simp add: permute_minus_cancel)

   514       apply(assumption)

   515        apply(rule_tac p="- (q + p)" in permute_boolE)

   516       apply(perm_strict_simp add: permute_minus_cancel)

   517       apply(assumption)

   518       apply(perm_strict_simp)

   519       apply(simp only:)

   520       apply(rule at_set_avoiding2)

   521       apply(simp add: finite_supp)

   522       apply(simp add: finite_supp)

   523       apply(simp add: finite_supp)

   524       apply(rule_tac p="-p" in permute_boolE)

   525       apply(perm_strict_simp add: permute_minus_cancel)

   526 	--"supplied by the user"

   527       apply(simp add: fresh_star_Pair)

   528       sorry

   529   qed

   530   then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .

   531   then show "P c \<Gamma> t T" by simp

   532 qed

   533 

   534 *)

   535 

   536 

   537 end

   538 

   539 

   540