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 3192 14c7d7e29c44
parent 3191 0440bc1a2438
child 3197 25d11b449e92
equal deleted inserted replaced
3191:0440bc1a2438 3192:14c7d7e29c44 
    92                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
 
    92                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
 
    93 apply(simp add: eqvt_def is_eta_nf_graph_def)
 
    93 apply(simp add: eqvt_def is_eta_nf_graph_def)
 
    94 apply(rule TrueI)
 
    94 apply(rule TrueI)
 
    95 apply(rule_tac y="x" in lam.exhaust)
 
    95 apply(rule_tac y="x" in lam.exhaust)
 
    96 apply(auto)[3]
 
    96 apply(auto)[3]
 
       
    97 using [[simproc del: alpha_lst]]
 
    97 apply(simp_all)
 
    98 apply(simp_all)
 
    98 apply(erule_tac c="()" in Abs_lst1_fcb2')
 
    99 apply(erule_tac c="()" in Abs_lst1_fcb2')
 
    99 apply(simp_all add: pure_fresh fresh_star_def)[3]
 
   100 apply(simp_all add: pure_fresh fresh_star_def)[3]
 
   100 apply(simp add: eqvt_at_def conj_eqvt)
 
   101 apply(simp add: eqvt_at_def conj_eqvt)
 
   101 apply(simp add: eqvt_at_def conj_eqvt)
 
   102 apply(simp add: eqvt_at_def conj_eqvt)
 
   122 apply(simp add: eqvt_def var_pos_graph_def)
 
   123 apply(simp add: eqvt_def var_pos_graph_def)
 
   123 apply(rule TrueI)
 
   124 apply(rule TrueI)
 
   124 apply(case_tac x)
 
   125 apply(case_tac x)
 
   125 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
 
   126 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
 
   126 apply(auto simp add: fresh_star_def)[3]
 
   127 apply(auto simp add: fresh_star_def)[3]
 
       
   128 using [[simproc del: alpha_lst]]
 
   127 apply(simp_all)
 
   129 apply(simp_all)
 
   128 apply(erule conjE)+
 
   130 apply(erule conjE)+
 
   129 apply(erule_tac Abs_lst1_fcb2)
 
   131 apply(erule_tac Abs_lst1_fcb2)
 
   130 apply(simp add: pure_fresh)
 
   132 apply(simp add: pure_fresh)
 
   131 apply(simp add: fresh_star_def)
 
   133 apply(simp add: fresh_star_def)
 
   167   apply(simp add: eqvt_def subst'_graph_def)
 
   169   apply(simp add: eqvt_def subst'_graph_def)
 
   168   apply(rule TrueI)
 
   170   apply(rule TrueI)
 
   169   apply(case_tac x)
 
   171   apply(case_tac x)
 
   170   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
 
   172   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
 
   171   apply(auto simp add: fresh_star_def)[3]
 
   173   apply(auto simp add: fresh_star_def)[3]
 
       
   174   using [[simproc del: alpha_lst]]
 
   172   apply(simp_all)
 
   175   apply(simp_all)
 
   173   apply(erule conjE)+
 
   176   apply(erule conjE)+
 
   174   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
 
   177   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
 
   175   apply(simp_all add: Abs_fresh_iff)
 
   178   apply(simp_all add: Abs_fresh_iff)
 
   176   apply(simp add: fresh_star_def fresh_Pair)
 
   179   apply(simp add: fresh_star_def fresh_Pair)
 
   200   unfolding eqvt_def
 
   203   unfolding eqvt_def
 
   201   unfolding frees_lst_graph_def
 
   204   unfolding frees_lst_graph_def
 
   202 apply(simp)
 
   205 apply(simp)
 
   203 apply(rule TrueI)
 
   206 apply(rule TrueI)
 
   204 apply(rule_tac y="x" in lam.exhaust)
 
   207 apply(rule_tac y="x" in lam.exhaust)
 
       
   208 using [[simproc del: alpha_lst]]
 
   205 apply(auto)
 
   209 apply(auto)
 
   206 apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   210 apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   207 apply(simp add: supp_removeAll fresh_def)
 
   211 apply(simp add: supp_removeAll fresh_def)
 
   208 apply(simp add: fresh_star_def fresh_Unit)
 
   212 apply(simp add: fresh_star_def fresh_Unit)
 
   209 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 
   213 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 
   227   apply(simp add: eqvt_def frees_set_graph_def)
 
   231   apply(simp add: eqvt_def frees_set_graph_def)
 
   228   apply(erule frees_set_graph.induct)
 
   232   apply(erule frees_set_graph.induct)
 
   229   apply(auto)[9]
 
   233   apply(auto)[9]
 
   230   apply(rule_tac y="x" in lam.exhaust)
 
   234   apply(rule_tac y="x" in lam.exhaust)
 
   231   apply(auto)[3]
 
   235   apply(auto)[3]
 
       
   236   using [[simproc del: alpha_lst]]
 
   232   apply(simp)
 
   237   apply(simp)
 
   233   apply(erule_tac c="()" in Abs_lst1_fcb2)
 
   238   apply(erule_tac c="()" in Abs_lst1_fcb2)
 
   234   apply(simp add: fresh_minus_atom_set)
 
   239   apply(simp add: fresh_minus_atom_set)
 
   235   apply(simp add: fresh_star_def fresh_Unit)
 
   240   apply(simp add: fresh_star_def fresh_Unit)
 
   236   apply(simp add: Diff_eqvt eqvt_at_def)
 
   241   apply(simp add: Diff_eqvt eqvt_at_def)
 
   252 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 
   257 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 
   253 | "height (Lam [x].t) = height t + 1"
 
   258 | "height (Lam [x].t) = height t + 1"
 
   254   apply(simp add: eqvt_def height_graph_def)
 
   259   apply(simp add: eqvt_def height_graph_def)
 
   255   apply(rule TrueI)
 
   260   apply(rule TrueI)
 
   256   apply(rule_tac y="x" in lam.exhaust)
 
   261   apply(rule_tac y="x" in lam.exhaust)
 
       
   262   using [[simproc del: alpha_lst]]
 
   257   apply(auto)
 
   263   apply(auto)
 
   258   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   264   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   259   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
 
   265   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
 
   260   done
 
   266   done
 
   261 
   267 
   274 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 
   280 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 
   275 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
 
   281 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
 
   276   unfolding eqvt_def subst_graph_def
 
   282   unfolding eqvt_def subst_graph_def
 
   277   apply(simp)
 
   283   apply(simp)
 
   278   apply(rule TrueI)
 
   284   apply(rule TrueI)
 
       
   285   using [[simproc del: alpha_lst]]
 
   279   apply(auto)
 
   286   apply(auto)
 
   280   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 
   287   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 
   281   apply(blast)+
 
   288   apply(blast)+
 
       
   289   using [[simproc del: alpha_lst]]
 
   282   apply(simp_all add: fresh_star_def fresh_Pair_elim)
 
   290   apply(simp_all add: fresh_star_def fresh_Pair_elim)
 
   283   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
 
   291   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
 
   284   apply(simp_all add: Abs_fresh_iff)
 
   292   apply(simp_all add: Abs_fresh_iff)
 
   285   apply(simp add: fresh_star_def fresh_Pair)
 
   293   apply(simp add: fresh_star_def fresh_Pair)
 
   286   apply(simp only: eqvt_at_def)
 
   294   apply(simp only: eqvt_at_def)
 
   304      (auto simp add: fresh_at_base)
 
   312      (auto simp add: fresh_at_base)
 
   305 
   313 
   306 text {* same lemma but with subst.induction *}
 
   314 text {* same lemma but with subst.induction *}
 
   307 lemma forget2:
 
   315 lemma forget2:
 
   308   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
 
   316   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
 
   309   by (induct t x s rule: subst.induct)
 
   317   apply(induct t x s rule: subst.induct)
 
   310      (auto simp add:  fresh_at_base fresh_Pair)
 
   318   using [[simproc del: alpha_lst]]
 
       
   319   apply(auto simp add:  flip_fresh_fresh fresh_Pair fresh_at_base)
 
       
   320   done
 
   311 
   321 
   312 lemma fresh_fact:
 
   322 lemma fresh_fact:
 
   313   fixes z::"name"
 
   323   fixes z::"name"
 
   314   assumes a: "atom z \<sharp> s"
 
   324   assumes a: "atom z \<sharp> s"
 
   315       and b: "z = y \<or> atom z \<sharp> t"
 
   325       and b: "z = y \<or> atom z \<sharp> t"
 
   465   apply (simp add: fresh_star_def ln.fresh)
 
   475   apply (simp add: fresh_star_def ln.fresh)
 
   466   apply (simp add: ln.fresh fresh_star_def)
 
   476   apply (simp add: ln.fresh fresh_star_def)
 
   467   apply(auto)[1]
 
   477   apply(auto)[1]
 
   468   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   478   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   469   apply (auto simp add: fresh_star_def)[3]
 
   479   apply (auto simp add: fresh_star_def)[3]
 
       
   480   using [[simproc del: alpha_lst]]
 
   470   apply(simp_all)
 
   481   apply(simp_all)
 
   471   apply(erule conjE)+
 
   482   apply(erule conjE)+
 
   472   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
 
   483   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
 
   473   apply (simp add: fresh_star_def)
 
   484   apply (simp add: fresh_star_def)
 
   474   apply (simp add: fresh_star_def)
 
   485   apply (simp add: fresh_star_def)
 
   496   apply(rule TrueI)
 
   507   apply(rule TrueI)
 
   497   apply(rule_tac y="x" in lam.exhaust)
 
   508   apply(rule_tac y="x" in lam.exhaust)
 
   498   apply(auto)[3]
 
   509   apply(auto)[3]
 
   499   apply(all_trivials)
 
   510   apply(all_trivials)
 
   500   apply(simp)
 
   511   apply(simp)
 
       
   512   using [[simproc del: alpha_lst]]
 
   501   apply(simp)
 
   513   apply(simp)
 
   502   apply(erule_tac c="()" in Abs_lst1_fcb2')
 
   514   apply(erule_tac c="()" in Abs_lst1_fcb2')
 
   503   apply(simp add: pure_fresh)
 
   515   apply(simp add: pure_fresh)
 
   504   apply(simp add: fresh_star_def pure_fresh)
 
   516   apply(simp add: fresh_star_def pure_fresh)
 
   505   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   517   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   524   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   536   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   525   apply(auto simp add: fresh_star_def)[3]
 
   537   apply(auto simp add: fresh_star_def)[3]
 
   526   apply(all_trivials)
 
   538   apply(all_trivials)
 
   527   apply(simp)
 
   539   apply(simp)
 
   528   apply(simp)
 
   540   apply(simp)
 
       
   541   using [[simproc del: alpha_lst]]
 
   529   apply(simp)
 
   542   apply(simp)
 
   530   apply(erule conjE)
 
   543   apply(erule conjE)
 
   531   apply(erule Abs_lst1_fcb2')
 
   544   apply(erule Abs_lst1_fcb2')
 
   532   apply(simp add: pure_fresh fresh_star_def)
 
   545   apply(simp add: pure_fresh fresh_star_def)
 
   533   apply(simp add: fresh_star_def)
 
   546   apply(simp add: fresh_star_def)
 
   580   apply(simp)
 
   593   apply(simp)
 
   581   apply(rule TrueI)
 
   594   apply(rule TrueI)
 
   582   apply (case_tac x)
 
   595   apply (case_tac x)
 
   583   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   596   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   584   apply (auto simp add: fresh_star_def fresh_at_list)[3]
 
   597   apply (auto simp add: fresh_star_def fresh_at_list)[3]
 
       
   598   using [[simproc del: alpha_lst]]
 
   585   apply(simp_all)
 
   599   apply(simp_all)
 
   586   apply(elim conjE)
 
   600   apply(elim conjE)
 
   587   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
 
   601   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
 
   588   apply (simp add: pure_fresh)
 
   602   apply (simp add: pure_fresh)
 
   589   apply(simp add: fresh_star_def fresh_at_list)
 
   603   apply(simp add: fresh_star_def fresh_at_list)
 
   639 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
 
   653 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
 
   640   apply(simp add: eval_apply_subst_graph_def eqvt_def)
 
   654   apply(simp add: eval_apply_subst_graph_def eqvt_def)
 
   641   apply(rule TrueI)
 
   655   apply(rule TrueI)
 
   642   apply (case_tac x)
 
   656   apply (case_tac x)
 
   643   apply (case_tac a rule: lam.exhaust)
 
   657   apply (case_tac a rule: lam.exhaust)
 
       
   658   using [[simproc del: alpha_lst]]
 
   644   apply simp_all[3]
 
   659   apply simp_all[3]
 
   645   apply blast
 
   660   apply blast
 
   646   apply (case_tac b)
 
   661   apply (case_tac b)
 
   647   apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
 
   662   apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
 
   648   apply simp_all[3]
 
   663   apply simp_all[3]
 
   649   apply blast
 
   664   apply blast
 
   650   apply blast
 
   665   apply blast
 
   651   apply (simp add: Abs1_eq_iff fresh_star_def)
 
   666   apply (simp add: Abs1_eq_iff fresh_star_def)
 
       
   667   using [[simproc del: alpha_lst]]
 
   652   apply(simp_all)
 
   668   apply(simp_all)
 
   653   apply(erule_tac c="()" in Abs_lst1_fcb2)
 
   669   apply(erule_tac c="()" in Abs_lst1_fcb2)
 
   654   apply (simp add: Abs_fresh_iff)
 
   670   apply (simp add: Abs_fresh_iff)
 
   655   apply(simp add: fresh_star_def fresh_Unit)
 
   671   apply(simp add: fresh_star_def fresh_Unit)
 
   656   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   672   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   690 unfolding eqvt_def q_graph_def
 
   706 unfolding eqvt_def q_graph_def
 
   691 apply (simp)
 
   707 apply (simp)
 
   692 apply (rule TrueI)
 
   708 apply (rule TrueI)
 
   693 apply (case_tac x)
 
   709 apply (case_tac x)
 
   694 apply (rule_tac y="a" in lam.exhaust)
 
   710 apply (rule_tac y="a" in lam.exhaust)
 
       
   711 using [[simproc del: alpha_lst]]
 
   695 apply simp_all
 
   712 apply simp_all
 
   696 apply blast
 
   713 apply blast
 
   697 apply blast
 
   714 apply blast
 
   698 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
 
   715 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
 
   699 apply blast
 
   716 apply blast
 
   716 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 
   733 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 
   717 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
 
   734 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
 
   718   apply (simp add: eqvt_def map_term_graph_def)
 
   735   apply (simp add: eqvt_def map_term_graph_def)
 
   719   apply(rule TrueI)
 
   736   apply(rule TrueI)
 
   720   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
 
   737   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
 
       
   738   using [[simproc del: alpha_lst]]
 
   721   apply auto
 
   739   apply auto
 
   722   apply (erule Abs_lst1_fcb)
 
   740   apply (erule Abs_lst1_fcb)
 
   723   apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
 
   741   apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
 
   724   apply (simp add: eqvt_def permute_fun_app_eq)
 
   742   apply (simp add: eqvt_def permute_fun_app_eq)
 
   725   done
 
   743   done
 
   888   apply(rule_tac y="b" in lam.exhaust)
 
   906   apply(rule_tac y="b" in lam.exhaust)
 
   889   apply(auto)[3]
 
   907   apply(auto)[3]
 
   890   apply(rule_tac y="b" in lam.exhaust)
 
   908   apply(rule_tac y="b" in lam.exhaust)
 
   891   apply(auto)[3]
 
   909   apply(auto)[3]
 
   892   apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)
 
   910   apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)
 
       
   911   using [[simproc del: alpha_lst]]
 
   893   apply(auto)[3]
 
   912   apply(auto)[3]
 
   894   apply(drule_tac x="name" in meta_spec)
 
   913   apply(drule_tac x="name" in meta_spec)
 
   895   apply(drule_tac x="name" in meta_spec)
 
   914   apply(drule_tac x="name" in meta_spec)
 
   896   apply(drule_tac x="lam" in meta_spec)
 
   915   apply(drule_tac x="lam" in meta_spec)
 
   897   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
 
   916   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
 
       
   917   using [[simproc del: alpha_lst]]
 
   898   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
 
   918   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
 
   899   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
 
   919   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
 
       
   920   using [[simproc del: alpha_lst]]
 
   900   apply simp_all
 
   921   apply simp_all
 
   901   apply (simp add: abs_same_binder)
 
   922   apply (simp add: abs_same_binder)
 
   902   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   923   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   903   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)
 
   924   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)
 
   904   done
 
   925   done
nominal2