equal
deleted
inserted
replaced
88 |
88 |
89 section {* type definition for the quotient type *} |
89 section {* type definition for the quotient type *} |
90 |
90 |
91 (* the auxiliary data for the quotient types *) |
91 (* the auxiliary data for the quotient types *) |
92 use "quotient_info.ML" |
92 use "quotient_info.ML" |
|
93 |
|
94 ML {* print_mapsinfo @{context} *} |
93 |
95 |
94 declare [[map "fun" = (fun_map, fun_rel)]] |
96 declare [[map "fun" = (fun_map, fun_rel)]] |
95 |
97 |
96 lemmas [quot_thm] = fun_quotient |
98 lemmas [quot_thm] = fun_quotient |
97 |
99 |
994 in |
996 in |
995 rtac rule i |
997 rtac rule i |
996 end) |
998 end) |
997 *} |
999 *} |
998 |
1000 |
999 section {* General Shape of the Lifting Procedure *} |
1001 section {* The General Shape of the Lifting Procedure *} |
1000 |
1002 |
1001 (* - A is the original raw theorem *) |
1003 (* - A is the original raw theorem *) |
1002 (* - B is the regularized theorem *) |
1004 (* - B is the regularized theorem *) |
1003 (* - C is the rep/abs injected version of B *) |
1005 (* - C is the rep/abs injected version of B *) |
1004 (* - D is the lifted theorem *) |
1006 (* - D is the lifted theorem *) |
1005 (* *) |
1007 (* *) |
1006 (* - b is the regularization step *) |
1008 (* - b is the regularization step *) |
1007 (* - c is the rep/abs injection step *) |
1009 (* - c is the rep/abs injection step *) |
1008 (* - d is the cleaning part *) |
1010 (* - d is the cleaning part *) |
1009 (* *) |
1011 (* *) |
1010 (* the QUOT_TRUE premise records the lifted theorem *) |
1012 (* the QUOT_TRUE premise in c records the lifted theorem *) |
1011 |
1013 |
1012 lemma lifting_procedure: |
1014 lemma lifting_procedure: |
1013 assumes a: "A" |
1015 assumes a: "A" |
1014 and b: "A \<longrightarrow> B" |
1016 and b: "A \<longrightarrow> B" |
1015 and c: "QUOT_TRUE D \<Longrightarrow> B = C" |
1017 and c: "QUOT_TRUE D \<Longrightarrow> B = C" |