Cookies disclaimer

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.

Rev rev

We defined a function to reverse a list.
If it worked properly, it should produce the original list after applying it twice. Can you show that?

We gave you some lemma as a hint.

Resources

Download Files

Definitions File

theory Defs
  imports Main 
begin

fun rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = rev xs @ [x]"

end

Template File

theory Submission
  imports Defs
begin
 
  
lemma rev_append: "rev (xs @ ys) = rev ys @ rev xs"
  sorry
  
lemma doublerev: "rev (rev xs) = xs"
  sorry


end

Check File

theory Check
imports Submission
begin
 

lemma "rev (rev xs) = xs" 
by (rule Submission.doublerev) 

end
Download Files

Definitions File

theory Defs
  imports Main 
begin

fun rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = rev xs @ [x]"

end

Template File

theory Submission
  imports Defs
begin
 
  
lemma rev_append: "rev (xs @ ys) = rev ys @ rev xs"
  sorry
  
lemma doublerev: "rev (rev xs) = xs"
  sorry


end

Check File

theory Check
imports Submission
begin
 

lemma "rev (rev xs) = xs" 
by (rule Submission.doublerev) 

end

Terms and Conditions