1000 |
1000 |
1001 section {* The General Shape of the Lifting Procedure *} |
1001 section {* The General Shape of the Lifting Procedure *} |
1002 |
1002 |
1003 (* - A is the original raw theorem *) |
1003 (* - A is the original raw theorem *) |
1004 (* - B is the regularized theorem *) |
1004 (* - B is the regularized theorem *) |
1005 (* - C is the rep/abs injected version of B *) |
1005 (* - C is the rep/abs injected version of B *) |
1006 (* - D is the lifted theorem *) |
1006 (* - D is the lifted theorem *) |
1007 (* *) |
1007 (* *) |
1008 (* - b is the regularization step *) |
1008 (* - 1st prem is the regularization step *) |
1009 (* - c is the rep/abs injection step *) |
1009 (* - 2nd prem is the rep/abs injection step *) |
1010 (* - d is the cleaning part *) |
1010 (* - 3rd prem is the cleaning part *) |
1011 (* *) |
1011 (* *) |
1012 (* the QUOT_TRUE premise in c records the lifted theorem *) |
1012 (* the QUOT_TRUE premise in 2 records the lifted theorem *) |
1013 |
1013 |
1014 lemma lifting_procedure: |
1014 ML {* |
1015 assumes a: "A" |
1015 val lifting_procedure = |
1016 and b: "A \<longrightarrow> B" |
1016 @{lemma "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)} |
1017 and c: "QUOT_TRUE D \<Longrightarrow> B = C" |
1017 *} |
1018 and d: "C = D" |
|
1019 shows "D" |
|
1020 using a b c d |
|
1021 by (simp add: QUOT_TRUE_def) |
|
1022 |
1018 |
1023 ML {* |
1019 ML {* |
1024 fun lift_match_error ctxt fun_str rtrm qtrm = |
1020 fun lift_match_error ctxt fun_str rtrm qtrm = |
1025 let |
1021 let |
1026 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1022 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1047 in |
1043 in |
1048 Drule.instantiate' [] |
1044 Drule.instantiate' [] |
1049 [SOME (cterm_of thy rtrm'), |
1045 [SOME (cterm_of thy rtrm'), |
1050 SOME (cterm_of thy reg_goal), |
1046 SOME (cterm_of thy reg_goal), |
1051 NONE, |
1047 NONE, |
1052 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1048 SOME (cterm_of thy inj_goal)] lifting_procedure |
1053 end |
1049 end |
1054 *} |
1050 *} |
1055 |
1051 |
1056 ML {* |
1052 ML {* |
1057 (* the tactic leaves three subgoals to be proved *) |
1053 (* the tactic leaves three subgoals to be proved *) |
1070 section {* Automatic Proofs *} |
1066 section {* Automatic Proofs *} |
1071 |
1067 |
1072 ML {* |
1068 ML {* |
1073 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
1069 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
1074 |
1070 |
|
1071 (* prints warning, if goal is unsolved *) |
1075 fun WARN (tac, msg) i st = |
1072 fun WARN (tac, msg) i st = |
1076 case Seq.pull ((SOLVES' tac) i st) of |
1073 case Seq.pull ((SOLVES' tac) i st) of |
1077 NONE => (warning msg; Seq.single st) |
1074 NONE => (warning msg; Seq.single st) |
1078 | seqcell => Seq.make (fn () => seqcell) |
1075 | seqcell => Seq.make (fn () => seqcell) |
1079 |
1076 |
1080 fun RANGE_WARN xs = RANGE (map WARN xs) |
1077 fun RANGE_WARN xs = RANGE (map WARN xs) |
1081 *} |
1078 *} |
1082 |
1079 |
1083 ML {* |
1080 ML {* |
|
1081 local |
|
1082 |
|
1083 val msg1 = "Regularize proof failed." |
|
1084 val msg2 = cat_lines ["Injection proof failed.", |
|
1085 "This is probably due to missing respects lemmas.", |
|
1086 "Try invoking the injection_tac manually to see", |
|
1087 "which lemmas are missing."] |
|
1088 val msg3 = "Cleaning proof failed." |
|
1089 |
|
1090 in |
|
1091 |
1084 fun lift_tac ctxt rthm = |
1092 fun lift_tac ctxt rthm = |
1085 procedure_tac ctxt rthm |
1093 procedure_tac ctxt rthm |
1086 THEN' RANGE_WARN |
1094 THEN' RANGE_WARN |
1087 [(regularize_tac ctxt, "Regularize proof failed."), |
1095 [(regularize_tac ctxt, msg1), |
1088 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1096 (all_inj_repabs_tac ctxt, msg2), |
1089 (clean_tac ctxt, "Cleaning proof failed.")] |
1097 (clean_tac ctxt, msg3)] |
|
1098 |
|
1099 end |
1090 *} |
1100 *} |
1091 |
1101 |
1092 section {* Methods / Interface *} |
1102 section {* Methods / Interface *} |
1093 |
1103 |
1094 ML {* |
1104 ML {* |