# HG changeset patch # User Cezary Kaliszyk # Date 1262762677 -3600 # Node ID cd3fa86be45f04efa6c578d93738db041958fafb # Parent 77506496e6fd4cd691be3b24ea541994b2ac9337 Sledgehammer bug. diff -r 77506496e6fd -r cd3fa86be45f Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Tue Jan 05 18:10:20 2010 +0100 +++ b/Quot/Examples/FSet3.thy Wed Jan 06 08:24:37 2010 +0100 @@ -234,10 +234,11 @@ as "concat" -lemma fconcat_rsp[quot_respect]: +(*lemma fconcat_rsp[quot_respect]: shows "((list_rel op \) ===> op \) concat concat" apply(auto) sorry +*) (* PROBLEM: these lemmas needs to be restated, since *) (* concat.simps(1) and concat.simps(2) contain the *) @@ -251,17 +252,42 @@ shows "concat (x # xs) \ x @ concat xs" by (simp) +lemma concat_rsp[quot_respect]: + shows "(list_rel op \ OO op \ OO list_rel op \ ===> op \) concat concat" +sorry + +lemma nil_rsp2: "(list_rel op \ OO op \ OO list_rel op \) [] []" +sledgehammer +apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) +atp_minimize [atp=remote_vampire] FSet3.nil_rsp list_rel.simps(1) pred_comp.intros +thm pred_comp_def + lemma fconcat_empty: shows "fconcat {||} = {||}" apply(lifting_setup concat1) apply(regularize) -apply(injection) defer apply(cleaning) apply(simp add: comp_def) apply(cleaning) apply(fold fempty_def[simplified id_simps]) apply(rule refl) +apply(injection) +apply(rule apply_rsp[of "(list_rel (op \)) OO (op \) OO (list_rel (op \))" _ _ "op \" "concat" _ "[]" "((map rep_fset \ rep_fset) ((abs_fset \ map abs_fset) []))"]) +prefer 2 +ML_prf {* fun dest_comb (f $ a) = (f, a) *} +apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *}) +prefer 3 +apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *}) +apply(rule rep_abs_rsp[of _ "(abs_fset \ map abs_fset)" "(map rep_fset \ rep_fset)"]) +prefer 3 +apply(rule rep_abs_rsp[of _ "((map rep_fset \ rep_fset) ---> abs_fset)" "(abs_fset \ map abs_fset) ---> rep_fset"]) +prefer 2 +apply(rule concat_rsp) +prefer 3 +thm nil_rsp +apply(tactic {* rep_abs_rsp_tac @{context} 1 *}) +apply(rule rep_abs_rsp) sorry lemma fconcat_insert: diff -r 77506496e6fd -r cd3fa86be45f Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Tue Jan 05 18:10:20 2010 +0100 +++ b/Quot/quotient_tacs.ML Wed Jan 06 08:24:37 2010 +0100 @@ -1,11 +1,13 @@ signature QUOTIENT_TACS = sig val regularize_tac: Proof.context -> int -> tactic + val injection_tac: Proof.context -> int -> tactic val all_injection_tac: Proof.context -> int -> tactic val clean_tac: Proof.context -> int -> tactic val procedure_tac: Proof.context -> thm -> int -> tactic val lift_tac: Proof.context -> thm -> int -> tactic val quotient_tac: Proof.context -> int -> tactic + val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic end; structure Quotient_Tacs: QUOTIENT_TACS = @@ -637,4 +639,4 @@ (all_injection_tac ctxt, msg2), (clean_tac ctxt, msg3)] -end; (* structure *) \ No newline at end of file +end; (* structure *)