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 3181 ca162f0a7957
parent 3174 8f51702e1f2e
child 3183 313e6f2cdd89
equal deleted inserted replaced
3180:7b5db6c23753 3181:ca162f0a7957 
   297 thm subst.eqvt
 
   297 thm subst.eqvt
 
   298 
   298 
   299 lemma forget:
 
   299 lemma forget:
 
   300   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
 
   300   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
 
   301   by (nominal_induct t avoiding: x s rule: lam.strong_induct)
 
   301   by (nominal_induct t avoiding: x s rule: lam.strong_induct)
 
   302      (auto simp add: lam.fresh fresh_at_base)
 
   302      (auto simp add: fresh_at_base)
 
   303 
   303 
   304 text {* same lemma but with subst.induction *}
 
   304 text {* same lemma but with subst.induction *}
 
   305 lemma forget2:
 
   305 lemma forget2:
 
   306   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
 
   306   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
 
   307   by (induct t x s rule: subst.induct)
 
   307   by (induct t x s rule: subst.induct)
 
   308      (auto simp add: lam.fresh fresh_at_base fresh_Pair)
 
   308      (auto simp add:  fresh_at_base fresh_Pair)
 
   309 
   309 
   310 lemma fresh_fact:
 
   310 lemma fresh_fact:
 
   311   fixes z::"name"
 
   311   fixes z::"name"
 
   312   assumes a: "atom z \<sharp> s"
 
   312   assumes a: "atom z \<sharp> s"
 
   313       and b: "z = y \<or> atom z \<sharp> t"
 
   313       and b: "z = y \<or> atom z \<sharp> t"
 
   314   shows "atom z \<sharp> t[y ::= s]"
 
   314   shows "atom z \<sharp> t[y ::= s]"
 
   315   using a b
 
   315   using a b
 
   316   by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
 
   316   by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
 
   317       (auto simp add: lam.fresh fresh_at_base)
 
   317       (auto simp add:  fresh_at_base)
 
   318 
   318 
   319 lemma substitution_lemma:  
   319 lemma substitution_lemma:  
   320   assumes a: "x \<noteq> y" "atom x \<sharp> u"
 
   320   assumes a: "x \<noteq> y" "atom x \<sharp> u"
 
   321   shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"
 
   321   shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"
 
   322 using a 
   322 using a 
   326 lemma subst_rename: 
   326 lemma subst_rename: 
   327   assumes a: "atom y \<sharp> t"
 
   327   assumes a: "atom y \<sharp> t"
 
   328   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
 
   328   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
 
   329 using a 
   329 using a 
   330 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
 
   330 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
 
   331 apply (auto simp add: lam.fresh fresh_at_base)
 
   331 apply (auto simp add:  fresh_at_base)
 
   332 done
 
   332 done
 
   333 
   333 
   334 lemma height_ge_one:
 
   334 lemma height_ge_one:
 
   335   shows "1 \<le> (height e)"
 
   335   shows "1 \<le> (height e)"
 
   336 by (induct e rule: lam.induct) (simp_all)
 
   336 by (induct e rule: lam.induct) (simp_all)
 
   366 
   366 
   367 equivariance beta
 
   367 equivariance beta
 
   368 
   368 
   369 nominal_inductive beta
 
   369 nominal_inductive beta
 
   370   avoids b4: "x"
 
   370   avoids b4: "x"
 
   371   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
 
   371   by (simp_all add: fresh_star_def fresh_Pair  fresh_fact)
 
   372 
   372 
   373 text {* One-Reduction *}
 
   373 text {* One-Reduction *}
 
   374 
   374 
   375 inductive 
   375 inductive 
   376   One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)
 
   376   One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)
 
   383 equivariance One
 
   383 equivariance One
 
   384 
   384 
   385 nominal_inductive One 
   385 nominal_inductive One 
   386   avoids o3: "x"
 
   386   avoids o3: "x"
 
   387       |  o4: "x"
 
   387       |  o4: "x"
 
   388   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
 
   388   by (simp_all add: fresh_star_def fresh_Pair  fresh_fact)
 
   389 
   389 
   390 lemma One_refl:
 
   390 lemma One_refl:
 
   391   shows "t \<longrightarrow>1 t"
 
   391   shows "t \<longrightarrow>1 t"
 
   392 by (nominal_induct t rule: lam.strong_induct) (auto)
 
   392 by (nominal_induct t rule: lam.strong_induct) (auto)
 
   393 
   393 
   608   shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"
 
   608   shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"
 
   609   by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)
 
   609   by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)
 
   610 
   610 
   611 lemma var_fresh_subst:
 
   611 lemma var_fresh_subst:
 
   612   "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
 
   612   "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
 
   613   by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base)
 
   613   by (induct t x s rule: subst.induct) (auto simp add: lam.supp  fresh_at_base)
 
   614 
   614 
   615 (* function that evaluates a lambda term *)
 
   615 (* function that evaluates a lambda term *)
 
   616 nominal_primrec
 
   616 nominal_primrec
 
   617    eval :: "lam \<Rightarrow> lam" and
 
   617    eval :: "lam \<Rightarrow> lam" and
 
   618    apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 
   618    apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 
   839   apply(drule_tac x="lama" in meta_spec)
 
   839   apply(drule_tac x="lama" in meta_spec)
 
   840   apply(drule_tac x="c" in meta_spec)
 
   840   apply(drule_tac x="c" in meta_spec)
 
   841   apply(drule_tac x="namea" in meta_spec)
 
   841   apply(drule_tac x="namea" in meta_spec)
 
   842   apply(drule_tac x="lam" in meta_spec)
 
   842   apply(drule_tac x="lam" in meta_spec)
 
   843   apply(simp add: fresh_star_Pair)
 
   843   apply(simp add: fresh_star_Pair)
 
   844   apply(simp add: fresh_star_def fresh_at_base lam.fresh)
 
   844   apply(simp add: fresh_star_def fresh_at_base )
 
   845   apply(auto)[1]
 
   845   apply(auto)[1]
 
   846   apply(simp_all)[44]
 
   846   apply(simp_all)[44]
 
   847   apply(simp del: Product_Type.prod.inject)  
   847   apply(simp del: Product_Type.prod.inject)  
   848   oops
 
   848   oops
 
   849 
   849 
   878   apply(auto)[3]
 
   878   apply(auto)[3]
 
   879   apply(drule_tac x="name" in meta_spec)
 
   879   apply(drule_tac x="name" in meta_spec)
 
   880   apply(drule_tac x="name" in meta_spec)
 
   880   apply(drule_tac x="name" in meta_spec)
 
   881   apply(drule_tac x="lam" in meta_spec)
 
   881   apply(drule_tac x="lam" in meta_spec)
 
   882   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
 
   882   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
 
   883   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def)
 
   883   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
 
   884   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
 
   884   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
 
   885   apply simp_all
 
   885   apply simp_all
 
   886   apply (simp add: abs_same_binder)
 
   886   apply (simp add: abs_same_binder)
 
   887   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   887   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   888   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)
 
   888   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)
nominal2