Nominal/Ex/Lambda.thy
changeset 1805 f187f20f0a79
parent 1800 78fdc6b36a1c
child 1810 894930834ca8
equal deleted inserted replaced
1804:81b171e2d6d5 1805:f187f20f0a79
     8   Var "name"
     8   Var "name"
     9 | App "lam" "lam"
     9 | App "lam" "lam"
    10 | Lam x::"name" l::"lam"  bind x in l
    10 | Lam x::"name" l::"lam"  bind x in l
    11 
    11 
    12 lemmas supp_fn' = lam.fv[simplified lam.supp]
    12 lemmas supp_fn' = lam.fv[simplified lam.supp]
       
    13 
       
    14 declare lam.perm[eqvt]
    13 
    15 
    14 section {* Strong Induction Principles*}
    16 section {* Strong Induction Principles*}
    15 
    17 
    16 (* 
    18 (* 
    17   Old way of establishing strong induction
    19   Old way of establishing strong induction
    24   and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
    26   and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
    25   shows "P c lam"
    27   shows "P c lam"
    26 proof -
    28 proof -
    27   have "\<And>p. P c (p \<bullet> lam)"
    29   have "\<And>p. P c (p \<bullet> lam)"
    28     apply(induct lam arbitrary: c rule: lam.induct)
    30     apply(induct lam arbitrary: c rule: lam.induct)
    29     apply(simp only: lam.perm)
    31     apply(perm_simp)
    30     apply(rule a1)
    32     apply(rule a1)
    31     apply(simp only: lam.perm)
    33     apply(perm_simp)
    32     apply(rule a2)
    34     apply(rule a2)
    33     apply(assumption)
    35     apply(assumption)
    34     apply(assumption)
    36     apply(assumption)
    35     apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
    37     apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
    36     defer
    38     defer
    70   and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
    72   and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
    71   shows "P c lam"
    73   shows "P c lam"
    72 proof -
    74 proof -
    73   have "\<And>p. P c (p \<bullet> lam)"
    75   have "\<And>p. P c (p \<bullet> lam)"
    74     apply(induct lam arbitrary: c rule: lam.induct)
    76     apply(induct lam arbitrary: c rule: lam.induct)
    75     apply(simp only: lam.perm)
    77     apply(perm_simp)
    76     apply(rule a1)
    78     apply(rule a1)
    77     apply(simp only: lam.perm)
    79     apply(perm_simp)
    78     apply(rule a2)
    80     apply(rule a2)
    79     apply(assumption)
    81     apply(assumption)
    80     apply(assumption)
    82     apply(assumption)
    81     apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
    83     apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
    82     apply(erule exE)
    84     apply(erule exE)
    83     apply(rule_tac t="p \<bullet> Lam name lam" and 
    85     apply(rule_tac t="p \<bullet> Lam name lam" and 
    84                    s="q \<bullet> p \<bullet> Lam name lam" in subst)
    86                    s="q \<bullet> p \<bullet> Lam name lam" in subst)
    85     defer
    87     defer
    86     apply(simp add: lam.perm)
    88     apply(simp)
    87     apply(rule a3)
    89     apply(rule a3)
    88     apply(simp add: eqvts fresh_star_def)
    90     apply(simp add: eqvts fresh_star_def)
    89     apply(drule_tac x="q + p" in meta_spec)
    91     apply(drule_tac x="q + p" in meta_spec)
    90     apply(simp)
    92     apply(simp)
    91     apply(rule at_set_avoiding2)
    93     apply(rule at_set_avoiding2)
    92     apply(simp add: finite_supp)
    94     apply(simp add: finite_supp)
    93     apply(simp add: finite_supp)
    95     apply(simp add: finite_supp)
    94     apply(simp add: finite_supp)
    96     apply(simp add: finite_supp)
    95     apply(simp only: lam.perm atom_eqvt)
    97     apply(perm_simp)
    96     apply(simp add: fresh_star_def fresh_def supp_fn')
    98     apply(simp add: fresh_star_def fresh_def supp_fn')
    97     apply(rule supp_perm_eq)
    99     apply(rule supp_perm_eq)
    98     apply(simp)
   100     apply(simp)
    99     done
   101     done
   100   then have "P c (0 \<bullet> lam)" by blast
   102   then have "P c (0 \<bullet> lam)" by blast
   101   then show "P c lam" by simp
   103   then show "P c lam" by simp
   102 qed
   104 qed
       
   105 
       
   106 section {* Typing *}
       
   107 
       
   108 nominal_datatype ty =
       
   109   TVar string
       
   110 | TFun ty ty ("_ \<rightarrow> _")
       
   111 
       
   112 inductive
       
   113   valid :: "(name \<times> ty) list \<Rightarrow> bool"
       
   114 where
       
   115   "valid []"
       
   116 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
       
   117 
       
   118 ML {*
       
   119 fun my_tac ctxt intros =  
       
   120  Nominal_Permeq.eqvt_strict_tac ctxt [] []
       
   121  THEN' resolve_tac intros 
       
   122  THEN_ALL_NEW 
       
   123    (atac ORELSE'
       
   124     EVERY'
       
   125       [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}),
       
   126         Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
       
   127         atac ])
       
   128 *}
       
   129 
       
   130 
       
   131 lemma
       
   132   assumes a: "valid Gamma" 
       
   133   shows "valid (p \<bullet> Gamma)"
       
   134 using a
       
   135 apply(induct)
       
   136 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
       
   137 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
       
   138 done
       
   139 
       
   140 declare permute_lam_raw.simps[eqvt]
       
   141 
       
   142 thm alpha_gen_real_eqvt[no_vars]
       
   143 
       
   144 lemma temporary:
       
   145   shows "(p \<bullet> (bs, x) \<approx>gen R f q (cs, y)) = (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
       
   146 apply(simp only: permute_bool_def)
       
   147 apply(rule iffI)
       
   148 apply(rule alpha_gen_real_eqvt)
       
   149 apply(assumption)
       
   150 apply(drule_tac p="-p" in alpha_gen_real_eqvt(1))
       
   151 apply(simp)
       
   152 done
       
   153 
       
   154 lemma temporary_raw:
       
   155   shows "(p \<bullet> alpha_gen) \<equiv> alpha_gen"
       
   156 sorry
       
   157 
       
   158 declare temporary_raw[eqvt_raw]
       
   159 
       
   160 lemma
       
   161   assumes a: "alpha_lam_raw t1 t2"
       
   162   shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)"
       
   163 using a
       
   164 apply(induct)
       
   165 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
       
   166 apply(perm_strict_simp)
       
   167 apply(rule alpha_lam_raw.intros)
       
   168 apply(simp)
       
   169 apply(perm_strict_simp)
       
   170 apply(rule alpha_lam_raw.intros)
       
   171 apply(simp add: alphas)
       
   172 apply(rule_tac p="- p" in permute_boolE)
       
   173 apply(perm_simp permute_minus_cancel(2))
       
   174 oops
       
   175 
       
   176 
   103 
   177 
   104 section {* size function *}
   178 section {* size function *}
   105 
   179 
   106 lemma size_eqvt_raw:
   180 lemma size_eqvt_raw:
   107   fixes t::"lam_raw"
   181   fixes t::"lam_raw"