--- a/QuotMain.thy Sun Dec 06 06:58:24 2009 +0100
+++ b/QuotMain.thy Sun Dec 06 11:09:51 2009 +0100
@@ -255,6 +255,31 @@
fun NDT ctxt s tac thm = tac thm
*}
+section {* Matching of terms and types *}
+
+ML {*
+fun matches_typ (ty, ty') =
+ case (ty, ty') of
+ (_, TVar _) => true
+ | (TFree x, TFree x') => x = x'
+ | (Type (s, tys), Type (s', tys')) =>
+ s = s' andalso
+ if (length tys = length tys')
+ then (List.all matches_typ (tys ~~ tys'))
+ else false
+ | _ => false
+*}
+ML {*
+fun matches_term (trm, trm') =
+ case (trm, trm') of
+ (_, Var _) => true
+ | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
+ | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
+ | (Bound i, Bound j) => i = j
+ | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
+ | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s')
+ | _ => false
+*}
section {* Infrastructure for collecting theorems for starting the lifting *}
@@ -344,30 +369,6 @@
*}
ML {*
-fun matches_typ (ty, ty') =
- case (ty, ty') of
- (_, TVar _) => true
- | (TFree x, TFree x') => x = x'
- | (Type (s, tys), Type (s', tys')) =>
- s = s' andalso
- if (length tys = length tys')
- then (List.all matches_typ (tys ~~ tys'))
- else false
- | _ => false
-*}
-ML {*
-fun matches_term (trm, trm') =
- case (trm, trm') of
- (_, Var _) => true
- | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
- | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
- | (Bound i, Bound j) => i = j
- | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
- | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s')
- | _ => false
-*}
-
-ML {*
val mk_babs = Const (@{const_name Babs}, dummyT)
val mk_ball = Const (@{const_name Ball}, dummyT)
val mk_bex = Const (@{const_name Bex}, dummyT)
@@ -742,7 +743,7 @@
| (_, Const (@{const_name "op ="}, _)) => rtrm
- (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+ (* FIXME: check here that rtrm is the corresponding definition for the const *)
| (_, Const (_, T')) =>
let
val rty = fastype_of rtrm
@@ -757,20 +758,6 @@
section {* RepAbs Injection Tactic *}
-(* Not used anymore *)
-(* FIXME/TODO: do not handle everything *)
-ML {*
-fun instantiate_tac thm =
- Subgoal.FOCUS (fn {concl, ...} =>
- let
- val pat = Drule.strip_imp_concl (cprop_of thm)
- val insts = Thm.first_order_match (pat, concl)
- in
- rtac (Drule.instantiate insts thm) 1
- end
- handle _ => no_tac)
-*}
-
ML {*
fun quotient_tac ctxt =
REPEAT_ALL_NEW (FIRST'
@@ -784,6 +771,28 @@
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
*}
+ML {*
+fun solve_quotient_assums ctxt thm =
+ let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
+ thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
+ end
+ handle _ => error "solve_quotient_assums"
+*}
+
+(* It proves the Quotient assumptions by calling quotient_tac *)
+ML {*
+fun solve_quotient_assum i ctxt thm =
+ let
+ val tac =
+ (compose_tac (false, thm, i)) THEN_ALL_NEW
+ (quotient_tac ctxt);
+ val gc = Drule.strip_imp_concl (cprop_of thm);
+ in
+ Goal.prove_internal [] gc (fn _ => tac 1)
+ end
+ handle _ => error "solve_quotient_assum"
+*}
+
definition
"QUOT_TRUE x \<equiv> True"
@@ -802,58 +811,6 @@
end
*}
-(* It proves the Quotient assumptions by calling quotient_tac *)
-ML {*
-fun solve_quotient_assum i ctxt thm =
- let
- val tac =
- (compose_tac (false, thm, i)) THEN_ALL_NEW
- (quotient_tac ctxt);
- val gc = Drule.strip_imp_concl (cprop_of thm);
- in
- Goal.prove_internal [] gc (fn _ => tac 1)
- end
- handle _ => error "solve_quotient_assum"
-*}
-
-ML {*
-fun solve_quotient_assums ctxt thm =
- let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
- thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
- end
- handle _ => error "solve_quotient_assums"
-*}
-
-ML {*
-val apply_rsp_tac =
- Subgoal.FOCUS (fn {concl, asms, context,...} =>
- case ((HOLogic.dest_Trueprop (term_of concl))) of
- ((R2 $ (f $ x) $ (g $ y))) =>
- (let
- val (asmf, asma) = find_qt_asm (map term_of asms);
- in
- if (fastype_of asmf) = (fastype_of f) then no_tac else let
- val ty_a = fastype_of x;
- val ty_b = fastype_of asma;
- val ty_c = range_type (type_of f);
- val thy = ProofContext.theory_of context;
- val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
- val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
- val te = solve_quotient_assums context thm
- val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
- val thm = Drule.instantiate' [] t_inst te
- in
- compose_tac (false, thm, 2) 1
- end
- end
- handle ERROR "find_qt_asm: no pair" => no_tac)
- | _ => no_tac)
-*}
-
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
(*
To prove that the regularised theorem implies the abs/rep injected,
we try:
@@ -944,6 +901,35 @@
*}
ML {*
+val apply_rsp_tac =
+ Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ case ((HOLogic.dest_Trueprop (term_of concl))) of
+ ((R2 $ (f $ x) $ (g $ y))) =>
+ (let
+ val (asmf, asma) = find_qt_asm (map term_of asms);
+ in
+ if (fastype_of asmf) = (fastype_of f) then no_tac else let
+ val ty_a = fastype_of x;
+ val ty_b = fastype_of asma;
+ val ty_c = range_type (type_of f);
+ val thy = ProofContext.theory_of context;
+ val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+ val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+ val te = solve_quotient_assums context thm
+ val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+ val thm = Drule.instantiate' [] t_inst te
+ in
+ compose_tac (false, thm, 2) 1
+ end
+ end
+ handle ERROR "find_qt_asm: no pair" => no_tac)
+ | _ => no_tac)
+*}
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
case (bare_concl goal) of
@@ -1034,8 +1020,6 @@
REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
*}
-
-
section {* Cleaning of the theorem *}
ML {*