# HG changeset patch # User Cezary Kaliszyk # Date 1255599734 -7200 # Node ID 4f93c5a026d227b890fd1093c822d7f036cda2b2 # Parent 09f4d69f7b669f23230ba6cadf9ccface6271162 Reordering the code, part 3 diff -r 09f4d69f7b66 -r 4f93c5a026d2 QuotMain.thy --- a/QuotMain.thy Thu Oct 15 11:29:38 2009 +0200 +++ b/QuotMain.thy Thu Oct 15 11:42:14 2009 +0200 @@ -774,98 +774,10 @@ ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} -ML {* - fun dest_cbinop t = - let - val (t2, rhs) = Thm.dest_comb t; - val (bop, lhs) = Thm.dest_comb t2; - in - (bop, (lhs, rhs)) - end -*} - -ML {* - fun dest_ceq t = - let - val (bop, pair) = dest_cbinop t; - val (bop_s, _) = Term.dest_Const (Thm.term_of bop); - in - if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) - end -*} - -ML Thm.instantiate -ML {*@{thm arg_cong2}*} -ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} -ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} -ML {* - Toplevel.program (fn () => - Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2} - ) -*} - -ML {* - fun split_binop_conv t = - let - val (lhs, rhs) = dest_ceq t; - val (bop, _) = dest_cbinop lhs; - val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; - val [cmT, crT] = Thm.dest_ctyp cr2; - in - Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2} - end -*} - +(* Has all the theorems about fset plugged in. These should be parameters to the tactic *) ML {* - fun split_arg_conv t = - let - val (lhs, rhs) = dest_ceq t; - val (lop, larg) = Thm.dest_comb lhs; - val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; - in - Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong} - end -*} - -ML {* - fun split_binop_tac n thm = - let - val concl = Thm.cprem_of thm n; - val (_, cconcl) = Thm.dest_comb concl; - val rewr = split_binop_conv cconcl; - in - rtac rewr n thm - end - handle CTERM _ => Seq.empty -*} - -ML {* - fun split_arg_tac n thm = - let - val concl = Thm.cprem_of thm n; - val (_, cconcl) = Thm.dest_comb concl; - val rewr = split_arg_conv cconcl; - in - rtac rewr n thm - end - handle CTERM _ => Seq.empty -*} - -(* Has all the theorems about fset plugged in. These should be parameters to the tactic *) - -lemma trueprop_cong: - shows "(a \ b) \ (Trueprop a \ Trueprop b)" - by auto - -ML {* - Cong_Tac.cong_tac -*} - -thm QUOT_TYPE_I_fset.R_trans2 -ML {* - fun foo_tac' ctxt = + fun transconv_fset_tac' ctxt = REPEAT_ALL_NEW (FIRST' [ -(* rtac @{thm trueprop_cong},*) rtac @{thm list_eq_refl}, rtac @{thm cons_preserves}, rtac @{thm mem_respects}, @@ -874,8 +786,6 @@ CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext} -(* rtac @{thm eq_reflection},*) -(* CHANGED o (ObjectLogic.full_atomize_tac)*) ]) *} @@ -912,7 +822,7 @@ prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) done thm length_append (* Not true but worth checking that the goal is correct *) @@ -925,7 +835,7 @@ prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) sorry thm m2 @@ -938,7 +848,7 @@ prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) done thm list_eq.intros(4) @@ -954,7 +864,7 @@ prove zzz : {* Thm.term_of cgoal3 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) done lemma zzz' : @@ -982,7 +892,7 @@ prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) done section {* handling quantifiers - regularize *} @@ -1215,7 +1125,7 @@ prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) sorry ML {* @@ -1225,7 +1135,7 @@ val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; val cgoal = cterm_of @{theory} goal; val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); - val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1; + val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (transconv_fset_tac' @{context}) 1; val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; @@ -1380,7 +1290,7 @@ (*prove aaa: {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (atomize(full)) - apply (tactic {* foo_tac' @{context} 1 *}) + apply (tactic {* transconv_fset_tac' @{context} 1 *}) done*) (* diff -r 09f4d69f7b66 -r 4f93c5a026d2 Unused.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Unused.thy Thu Oct 15 11:42:14 2009 +0200 @@ -0,0 +1,74 @@ + +ML {* + fun dest_cbinop t = + let + val (t2, rhs) = Thm.dest_comb t; + val (bop, lhs) = Thm.dest_comb t2; + in + (bop, (lhs, rhs)) + end +*} + +ML {* + fun dest_ceq t = + let + val (bop, pair) = dest_cbinop t; + val (bop_s, _) = Term.dest_Const (Thm.term_of bop); + in + if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) + end +*} + +ML {* + fun split_binop_conv t = + let + val (lhs, rhs) = dest_ceq t; + val (bop, _) = dest_cbinop lhs; + val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; + val [cmT, crT] = Thm.dest_ctyp cr2; + in + Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2} + end +*} + + +ML {* + fun split_arg_conv t = + let + val (lhs, rhs) = dest_ceq t; + val (lop, larg) = Thm.dest_comb lhs; + val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; + in + Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong} + end +*} + +ML {* + fun split_binop_tac n thm = + let + val concl = Thm.cprem_of thm n; + val (_, cconcl) = Thm.dest_comb concl; + val rewr = split_binop_conv cconcl; + in + rtac rewr n thm + end + handle CTERM _ => Seq.empty +*} + + +ML {* + fun split_arg_tac n thm = + let + val concl = Thm.cprem_of thm n; + val (_, cconcl) = Thm.dest_comb concl; + val rewr = split_arg_conv cconcl; + in + rtac rewr n thm + end + handle CTERM _ => Seq.empty +*} + + +lemma trueprop_cong: + shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)" + by auto