# HG changeset patch # User Christian Urban # Date 1279524878 -3600 # Node ID 4cc4390d5d2576fb852677364174f7bffdcc67bd # Parent 06574b438b8fab3ffe87f4684032f40dfdd3a5e8 corrected lambda-preservation theorem diff -r 06574b438b8f -r 4cc4390d5d25 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Mon Jul 19 07:49:10 2010 +0100 +++ b/Quotient-Paper/Paper.thy Mon Jul 19 08:34:38 2010 +0100 @@ -856,12 +856,12 @@ on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, which can all be performed independently from each other. - We first define the function @{text REG}, which takes terms of the + We first define the function @{text REG}, which takes the terms of the @{text "raw_thm"} and @{text "quot_thm"} as input and returns - @{text "reg_thm"}. The intuition + @{text "reg_thm"}. The idea behind this function is that it replaces quantifiers and abstractions involving raw types by bounded ones, and equalities - involving raw types are replaced by appropriate aggregate + involving raw types by appropriate aggregate equivalence relations. It is defined by simultaneously recursing on the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows: @@ -993,7 +993,7 @@ the lambda preservation theorem. Given @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have: - @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]} + @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]} \noindent Next, relations over lifted types are folded to equalities.