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/Foo2.thy
changeset 2579 dc988b07755e
parent 2578 64abcfddb0c1
child 2584 1eac050a36f4
equal deleted inserted replaced
2578:64abcfddb0c1 2579:dc988b07755e 
   275   fixes c :: "'a :: fs"
 
   275   fixes c :: "'a :: fs"
 
   276   and assg :: assg and trm :: trm
 
   276   and assg :: assg and trm :: trm
 
   277   assumes a0: "\<And>name c. P1 c (Var name)"
 
   277   assumes a0: "\<And>name c. P1 c (Var name)"
 
   278   and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"
 
   278   and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"
 
   279   and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"
 
   279   and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"
 
   280   and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>\<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"
 
   280   and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; \<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"
 
   281   and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"
 
   281   and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>{atom name1, atom name2} \<sharp>* c; \<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"
 
   282   and a5: "\<And>c. P2 c As_Nil"
 
   282   and a5: "\<And>c. P2 c As_Nil"
 
   283   and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"
 
   283   and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"
 
   284   shows "P1 c trm" "P2 c assg"
 
   284   shows "P1 c trm" "P2 c assg"
 
   285   using assms
 
   285   using assms
 
   286   apply(induction_schema)
 
   286   apply(induction_schema)
nominal2