--- a/QuotMain.thy Sun Dec 06 22:57:44 2009 +0100
+++ b/QuotMain.thy Sun Dec 06 22:58:03 2009 +0100
@@ -255,6 +255,32 @@
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 +370,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)
@@ -492,14 +494,6 @@
*)
-(* FIXME: they should be in in the new Isabelle *)
-lemma [mono]:
- "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
-by blast
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-by auto
-
(* FIXME: OPTION_equivp, PAIR_equivp, ... *)
ML {*
fun equiv_tac rel_eqvs =
@@ -509,6 +503,8 @@
rtac @{thm list_equivp}])
*}
+thm ball_reg_eqv
+
ML {*
fun ball_reg_eqv_simproc rel_eqvs ss redex =
let
@@ -608,6 +604,9 @@
end
*}
+thm ball_reg_eqv_range
+thm bex_reg_eqv_range
+
ML {*
fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
let
@@ -742,7 +741,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 +756,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 +769,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 +809,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 +899,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
@@ -968,42 +952,51 @@
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
| (Const (@{const_name "op ="},_) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+
(* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
| Const (@{const_name "op ="},_) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+
(* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-| Const (@{const_name "op ="},_) $ _ $ _ =>
+
(* reflexivity of operators arising from Cong_tac *)
- rtac @{thm refl} ORELSE'
- (resolve_tac trans2 THEN' RANGE [
- quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+| Const (@{const_name "op ="},_) $ _ $ _
+ => rtac @{thm refl} ORELSE'
+ (resolve_tac trans2 THEN' RANGE [
+ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
(Const (@{const_name fun_rel}, _) $ _ $ _) $
(Const (@{const_name fun_rel}, _) $ _ $ _)
=> rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
-| _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *)
- (* respectfulness of constants; in particular of a simple relation *)
- resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
-| _ $ _ $ _ =>
+
+ (* respectfulness of constants; in particular of a simple relation *)
+| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
(* observe ---> *)
- rep_abs_rsp_tac ctxt
+| _ $ _ $ _
+ => rep_abs_rsp_tac ctxt
+
| _ => error "inj_repabs_tac not a relation"
) i)
*}
@@ -1034,8 +1027,6 @@
REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
*}
-
-
section {* Cleaning of the theorem *}
ML {*