equal
deleted
inserted
replaced
662 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
662 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
663 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
663 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
664 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
664 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
665 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
665 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
666 by (simp_all add: QUOT_TRUE_def ext) |
666 by (simp_all add: QUOT_TRUE_def ext) |
667 |
|
668 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
|
669 by (simp add: QUOT_TRUE_def) |
|
670 |
667 |
671 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
668 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
672 by (simp add: QUOT_TRUE_def) |
669 by (simp add: QUOT_TRUE_def) |
673 |
670 |
674 ML {* |
671 ML {* |
1012 simp_tac (simps thms2), |
1009 simp_tac (simps thms2), |
1013 TRY o rtac refl] |
1010 TRY o rtac refl] |
1014 end |
1011 end |
1015 *} |
1012 *} |
1016 |
1013 |
1017 section {* Tactic for genralisation of free variables in a goal *} |
1014 section {* Tactic for Genralisation of Free Variables in a Goal *} |
1018 |
1015 |
1019 ML {* |
1016 ML {* |
1020 fun inst_spec ctrm = |
1017 fun inst_spec ctrm = |
1021 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
1018 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
1022 |
1019 |
1044 end) |
1041 end) |
1045 *} |
1042 *} |
1046 |
1043 |
1047 section {* General Shape of the Lifting Procedure *} |
1044 section {* General Shape of the Lifting Procedure *} |
1048 |
1045 |
1049 (* - A is the original raw theorem *) |
1046 (* - A is the original raw theorem *) |
1050 (* - B is the regularized theorem *) |
1047 (* - B is the regularized theorem *) |
1051 (* - C is the rep/abs injected version of B *) |
1048 (* - C is the rep/abs injected version of B *) |
1052 (* - D is the lifted theorem *) |
1049 (* - D is the lifted theorem *) |
1053 (* *) |
1050 (* *) |
1054 (* - b is the regularization step *) |
1051 (* - b is the regularization step *) |
1055 (* - c is the rep/abs injection step *) |
1052 (* - c is the rep/abs injection step *) |
1056 (* - d is the cleaning part *) |
1053 (* - d is the cleaning part *) |
|
1054 (* *) |
|
1055 (* the QUOT_TRUE premise records the lifted theorem *) |
1057 |
1056 |
1058 lemma lifting_procedure: |
1057 lemma lifting_procedure: |
1059 assumes a: "A" |
1058 assumes a: "A" |
1060 and b: "A \<longrightarrow> B" |
1059 and b: "A \<longrightarrow> B" |
1061 and c: "QUOT_TRUE D \<Longrightarrow> B = C" |
1060 and c: "QUOT_TRUE D \<Longrightarrow> B = C" |
1109 in |
1108 in |
1110 (rtac rule THEN' rtac rthm') i |
1109 (rtac rule THEN' rtac rthm') i |
1111 end) |
1110 end) |
1112 *} |
1111 *} |
1113 |
1112 |
1114 (* automatic proofs *) |
1113 section {* Automatic Proofs *} |
|
1114 |
1115 ML {* |
1115 ML {* |
1116 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
1116 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
1117 |
1117 |
1118 fun WARN (tac, msg) i st = |
1118 fun WARN (tac, msg) i st = |
1119 case Seq.pull ((SOLVES' tac) i st) of |
1119 case Seq.pull ((SOLVES' tac) i st) of |
1130 [(regularize_tac ctxt, "Regularize proof failed."), |
1130 [(regularize_tac ctxt, "Regularize proof failed."), |
1131 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1131 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1132 (clean_tac ctxt, "Cleaning proof failed.")] |
1132 (clean_tac ctxt, "Cleaning proof failed.")] |
1133 *} |
1133 *} |
1134 |
1134 |
1135 section {* methods / interface *} |
1135 section {* Methods / Interface *} |
|
1136 |
1136 ML {* |
1137 ML {* |
1137 fun mk_method1 tac thm ctxt = |
1138 fun mk_method1 tac thm ctxt = |
1138 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1139 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1139 |
1140 |
1140 fun mk_method2 tac ctxt = |
1141 fun mk_method2 tac ctxt = |