I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports "HOL-Data_Structures.Cmp" begin locale DYI_queue = fixes empty :: "'q" and push_front :: "'a \<Rightarrow> 'q \<Rightarrow> 'q" and push_back :: "'q \<Rightarrow> 'a \<Rightarrow> 'q" and pop_front :: "'q \<Rightarrow> ('a \<times> 'q)" and pop_back :: "'q \<Rightarrow> ('q \<times> 'a)" and invar :: "'q \<Rightarrow> bool" and \<alpha> :: "'q \<Rightarrow> 'a list" assumes "invar empty" and "\<alpha> empty = []" and "invar q \<Longrightarrow> \<alpha> (push_front x q) = x # \<alpha> q" and "invar q \<Longrightarrow> invar (push_front x q)" and "invar q \<Longrightarrow> \<alpha> (push_back q x) = \<alpha> q @ [x]" and "invar q \<Longrightarrow> invar (push_back q x)" and "\<lbrakk>invar q; q \<noteq> empty; pop_front q = (x, q')\<rbrakk> \<Longrightarrow> \<alpha> q = x # \<alpha> q'" and "\<lbrakk>invar q; q \<noteq> empty\<rbrakk> \<Longrightarrow> invar (snd (pop_front q))" and "\<lbrakk>invar q; q \<noteq> empty; pop_back q = (q', x)\<rbrakk> \<Longrightarrow> \<alpha> q = \<alpha> q' @ [x]" and "\<lbrakk>invar q; q \<noteq> empty\<rbrakk> \<Longrightarrow> invar (fst (pop_back q))" end

theory Submission imports Defs begin global_interpretation Q: DYI_queue where empty = undefined and push_front = undefined and push_back = undefined and pop_front = undefined and pop_back = undefined and invar = undefined and \<alpha> = undefined sorry (* start with: proof (standard, goal_cases) *) end

theory Check imports Submission begin end

Terms and Conditions