equal
deleted
inserted
replaced
1056 (* - d is the cleaning part *) |
1056 (* - d is the cleaning part *) |
1057 |
1057 |
1058 lemma lifting_procedure: |
1058 lemma lifting_procedure: |
1059 assumes a: "A" |
1059 assumes a: "A" |
1060 and b: "A \<longrightarrow> B" |
1060 and b: "A \<longrightarrow> B" |
1061 and c: "B = C" |
1061 and c: "QUOT_TRUE D \<Longrightarrow> B = C" |
1062 and d: "C = D" |
1062 and d: "C = D" |
1063 shows "D" |
1063 shows "D" |
1064 using a b c d |
1064 using a b c d |
1065 by simp |
1065 by (simp add: QUOT_TRUE_def) |
1066 |
1066 |
1067 ML {* |
1067 ML {* |
1068 fun lift_match_error ctxt fun_str rtrm qtrm = |
1068 fun lift_match_error ctxt fun_str rtrm qtrm = |
1069 let |
1069 let |
1070 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1070 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1090 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1090 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1091 in |
1091 in |
1092 Drule.instantiate' [] |
1092 Drule.instantiate' [] |
1093 [SOME (cterm_of thy rtrm'), |
1093 [SOME (cterm_of thy rtrm'), |
1094 SOME (cterm_of thy reg_goal), |
1094 SOME (cterm_of thy reg_goal), |
|
1095 NONE, |
1095 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1096 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1096 end |
1097 end |
1097 *} |
1098 *} |
1098 |
1099 |
1099 ML {* |
1100 ML {* |
1103 THEN' gen_frees_tac ctxt |
1104 THEN' gen_frees_tac ctxt |
1104 THEN' CSUBGOAL (fn (goal, i) => |
1105 THEN' CSUBGOAL (fn (goal, i) => |
1105 let |
1106 let |
1106 val rthm' = atomize_thm rthm |
1107 val rthm' = atomize_thm rthm |
1107 val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) |
1108 val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) |
1108 val bare_goal = snd (Thm.dest_comb goal) |
|
1109 val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i} |
|
1110 in |
1109 in |
1111 (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i |
1110 (rtac rule THEN' rtac rthm') i |
1112 end) |
1111 end) |
1113 *} |
1112 *} |
1114 |
1113 |
1115 (* automatic proofs *) |
1114 (* automatic proofs *) |
1116 ML {* |
1115 ML {* |
1125 *} |
1124 *} |
1126 |
1125 |
1127 ML {* |
1126 ML {* |
1128 fun lift_tac ctxt rthm = |
1127 fun lift_tac ctxt rthm = |
1129 procedure_tac ctxt rthm |
1128 procedure_tac ctxt rthm |
1130 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1129 THEN' RANGE_WARN |
1131 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1130 [(regularize_tac ctxt, "Regularize proof failed."), |
1132 (clean_tac ctxt, "Cleaning proof failed.")] |
1131 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
|
1132 (clean_tac ctxt, "Cleaning proof failed.")] |
1133 *} |
1133 *} |
1134 |
1134 |
1135 section {* methods / interface *} |
1135 section {* methods / interface *} |
1136 ML {* |
1136 ML {* |
1137 fun mk_method1 tac thm ctxt = |
1137 fun mk_method1 tac thm ctxt = |