Quotient-Paper/Paper.thy
changeset 2373 4cc4390d5d25
parent 2371 86c73a06ba4b
child 2374 0321e89e66a3
child 2376 44a5388d1d30
equal deleted inserted replaced
2372:06574b438b8f 2373:4cc4390d5d25
   854   regularized theorem based on @{text "raw_thm"} and
   854   regularized theorem based on @{text "raw_thm"} and
   855   @{text "quot_thm"}. Then we define the statement of the injected theorem, based
   855   @{text "quot_thm"}. Then we define the statement of the injected theorem, based
   856   on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
   856   on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
   857   which can all be performed independently from each other.
   857   which can all be performed independently from each other.
   858 
   858 
   859   We first define the function @{text REG}, which takes terms of the 
   859   We first define the function @{text REG}, which takes the terms of the 
   860   @{text "raw_thm"} and @{text "quot_thm"} as input and returns
   860   @{text "raw_thm"} and @{text "quot_thm"} as input and returns
   861   @{text "reg_thm"}. The intuition
   861   @{text "reg_thm"}. The idea
   862   behind this function is that it replaces quantifiers and
   862   behind this function is that it replaces quantifiers and
   863   abstractions involving raw types by bounded ones, and equalities
   863   abstractions involving raw types by bounded ones, and equalities
   864   involving raw types are replaced by appropriate aggregate
   864   involving raw types by appropriate aggregate
   865   equivalence relations. It is defined by simultaneously recursing on 
   865   equivalence relations. It is defined by simultaneously recursing on 
   866   the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
   866   the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
   867 
   867 
   868   \begin{center}
   868   \begin{center}
   869   \begin{tabular}{rcl}
   869   \begin{tabular}{rcl}
   991   variables that include raw types with respects by quantifiers
   991   variables that include raw types with respects by quantifiers
   992   over variables that include quotient types. We show here only
   992   over variables that include quotient types. We show here only
   993   the lambda preservation theorem. Given
   993   the lambda preservation theorem. Given
   994   @{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:
   994   @{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:
   995 
   995 
   996     @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
   996   @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
   997 
   997 
   998   \noindent
   998   \noindent
   999   Next, relations over lifted types are folded to equalities.
   999   Next, relations over lifted types are folded to equalities.
  1000   For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
  1000   For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
  1001 
  1001