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

### 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```

### 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```

### 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