Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Lambda.thy
changeset 1952 27cdc0a3a763
parent 1950 7de54c9f81ac
child 1954 23480003f9c5
equal deleted inserted replaced
1951:a0c7290a4e27 1952:27cdc0a3a763 
   124 
   124 
   125 inductive
 
   125 inductive
 
   126   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
   126   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
   127 where
 
   127 where
 
   128     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 
   128     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 
   129   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
 
   129   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
 
   130   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
   130   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
   131 
       
   132 inductive
 
       
   133   typing' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<Turnstile> _ : _" [60,60,60] 60) 
       
   134 where
 
       
   135     t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T"
 
       
   136   | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2"
 
       
   137   | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2"
 
       
   138 
       
   139 inductive
 
       
   140   typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60) 
       
   141 where
 
       
   142     t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T"
 
       
   143   | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2"
 
       
   144   | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2"
 
       
   145 
       
   146 inductive
 
       
   147   typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60)
 
       
   148 and  valid' :: "(name\<times>ty) list \<Rightarrow> bool"
 
       
   149 where
 
       
   150     v1[intro]: "valid' []"
 
       
   151   | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)"
 
       
   152   | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T"
 
       
   153   | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"
 
       
   154   | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2"
 
       
   155 
   131 
   156 equivariance valid
 
   132 equivariance valid
 
   157 equivariance typing
 
   133 equivariance typing
 
   158 equivariance typing'
 
       
   159 equivariance typing2' 
       
   160 equivariance typing''
 
       
   161 
   134 
   162 thm valid.eqvt
 
   135 thm valid.eqvt
 
   163 thm typing.eqvt
 
   136 thm typing.eqvt
 
   164 thm eqvts
 
   137 thm eqvts
 
   165 thm eqvts_raw
 
   138 thm eqvts_raw
 
       
   139 
       
   140 thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
 
       
   141 
       
   142 lemma
 
       
   143   fixes c::"'a::fs"
 
       
   144   assumes a: "\<Gamma> \<turnstile> t : T" 
       
   145   and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
 
       
   146   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> 
       
   147            \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"
 
       
   148   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> 
       
   149            \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"
 
       
   150   shows "P c \<Gamma> t T"
 
       
   151 proof -
 
       
   152   from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"
 
       
   153   proof (induct)
 
       
   154     case (t_Var \<Gamma> x T p c)
 
       
   155     then show ?case
 
       
   156       apply -
 
       
   157       apply(perm_strict_simp)
 
       
   158       apply(rule a1)
 
       
   159       apply(rule_tac p="-p" in permute_boolE)
 
       
   160       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   161       apply(assumption)
 
       
   162       apply(rule_tac p="-p" in permute_boolE)
 
       
   163       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   164       apply(assumption)
 
       
   165       done
 
       
   166   next
 
       
   167     case (t_App \<Gamma> t1 T1 T2 t2 p c)
 
       
   168     then show ?case
 
       
   169       apply -
 
       
   170       apply(perm_strict_simp)
 
       
   171       apply(rule_tac ?T1.0="p \<bullet> T1" in a2)
 
       
   172       apply(rule_tac p="-p" in permute_boolE)
 
       
   173       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   174       apply(assumption)
 
       
   175       apply(assumption)
 
       
   176       apply(rule_tac p="-p" in permute_boolE)
 
       
   177       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   178       apply(assumption)
 
       
   179       apply(assumption)
 
       
   180       done
 
       
   181   next
 
       
   182     case (t_Lam x \<Gamma> T1 t T2 p c)
 
       
   183     then show ?case
 
       
   184       apply -
 
       
   185       apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 
       
   186         supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
 
       
   187       apply(erule exE)
 
       
   188       apply(rule_tac t="p \<bullet> \<Gamma>" and  s="q \<bullet> p \<bullet> \<Gamma>" in subst)
 
       
   189       apply(rule supp_perm_eq)
 
       
   190       apply(simp add: supp_Pair fresh_star_union)
 
       
   191       apply(rule_tac t="p \<bullet> Lam x t" and  s="q \<bullet> p \<bullet> Lam x t" in subst)
 
       
   192       apply(rule supp_perm_eq)
 
       
   193       apply(simp add: supp_Pair fresh_star_union)
 
       
   194       apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="q \<bullet> p \<bullet> (T1 \<rightarrow> T2)" in subst)
 
       
   195       apply(rule supp_perm_eq)
 
       
   196       apply(simp add: supp_Pair fresh_star_union)
 
       
   197       apply(simp add: eqvts)
 
       
   198       apply(rule a3)
 
       
   199       apply(simp add: fresh_star_def)
 
       
   200       apply(rule_tac p="-q" in permute_boolE)
 
       
   201       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   202       apply(rule_tac p="-p" in permute_boolE)
 
       
   203       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   204       apply(assumption)
 
       
   205       apply(rule_tac p="-q" in permute_boolE)
 
       
   206       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   207       apply(rule_tac p="-p" in permute_boolE)
 
       
   208       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   209       apply(assumption)
 
       
   210       apply(drule_tac x="d" in meta_spec)
 
       
   211       apply(drule_tac x="q + p" in meta_spec)
 
       
   212       apply(simp)
 
       
   213       apply(rule at_set_avoiding2)
 
       
   214       apply(simp add: finite_supp)
 
       
   215       apply(simp add: finite_supp)
 
       
   216       apply(simp add: finite_supp)
 
       
   217       apply(rule_tac p="-p" in permute_boolE)
 
       
   218       apply(perm_strict_simp add: permute_minus_cancel)
 
       
   219 	(* supplied by the user *)
 
       
   220       apply(simp add: fresh_star_prod)
 
       
   221       apply(simp add: fresh_star_def)
 
       
   222 
       
   223 
       
   224       done
 
       
   225 (* HERE *)      
       
   226 
       
   227 
       
   228 
       
   229 
       
   230 
   166 
   231 
   167 
   232 
   168 inductive
 
   233 inductive
 
   169   tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"  
   234   tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"  
   170   for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
 
   235   for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
 
   187    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
   252    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
   188 
   253 
   189 declare permute_lam_raw.simps[eqvt]
 
   254 declare permute_lam_raw.simps[eqvt]
 
   190 declare alpha_gen_eqvt[eqvt]
 
   255 declare alpha_gen_eqvt[eqvt]
 
   191 equivariance alpha_lam_raw'
 
   256 equivariance alpha_lam_raw'
 
       
   257 
   192 thm eqvts_raw
 
   258 thm eqvts_raw
 
   193 
       
   194 
       
   195 
       
   196 (* HERE *)
 
       
   197 
       
   198 lemma
 
       
   199   assumes a: "alpha_lam_raw' t1 t2"
 
       
   200   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
 
       
   201 using a
 
       
   202 apply(induct)
 
       
   203 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
       
   204   @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*})
 
       
   205 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
       
   206   @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*})
 
       
   207 (*
 
       
   208 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
       
   209   @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*})
 
       
   210 *)
 
       
   211 oops
 
       
   212 
   259 
   213 section {* size function *}
 
   260 section {* size function *}
 
   214 
   261 
   215 lemma size_eqvt_raw:
 
   262 lemma size_eqvt_raw:
 
   216   fixes t::"lam_raw"
 
   263   fixes t::"lam_raw"
 
   365 apply(subst if_not_P)
 
   412 apply(subst if_not_P)
 
   366 apply(auto)
 
   413 apply(auto)
 
   367 done
 
   414 done
 
   368 *)
 
   415 *)
 
   369 
   416 
       
   417 
       
   418 ML {*
 
       
   419 
       
   420 fun prove_strong_ind (pred_name, avoids) ctxt = 
       
   421   Proof.theorem NONE (K I) [] ctxt
 
       
   422 
       
   423 local structure P = OuterParse and K = OuterKeyword in
 
       
   424 
       
   425 val _ =
 
       
   426   OuterSyntax.local_theory_to_proof "nominal_inductive"
 
       
   427     "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
 
       
   428       (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
 
       
   429         (P.$$$ ":" |-- P.and_list1 P.term))) []) >>  prove_strong_ind)
 
       
   430 
       
   431 end;
 
       
   432 
       
   433 *}
 
       
   434 
       
   435 (*
 
       
   436 nominal_inductive typing
 
       
   437 *)
 
       
   438 
       
   439 
   370 end
 
   440 end
 
   371 
   441 
   372 
   442 
   373 
   443
nominal2