diff -r 15d549bb986b -r 2b59bf690633 QuotMain.thy --- a/QuotMain.thy Tue Sep 22 09:42:27 2009 +0200 +++ b/QuotMain.thy Tue Sep 22 17:39:52 2009 +0200 @@ -607,16 +607,6 @@ term UNION thm UNION_def -(* Maybe the infrastructure should not allow this kind of definition, without showing that - the relation respects lenght... *) -(* cu: what does this mean? *) -local_setup {* - make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd -*} - -term length -term CARD -thm CARD_def thm QUOTIENT_fset @@ -636,15 +626,131 @@ using a by induct auto +fun + card1 :: "'a list \ nat" +where + card1_nil: "(card1 []) = 0" +| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" + +local_setup {* + make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} + +term card1 +term card +thm card_def + +(* text {* + Maybe make_const_def should require a theorem that says that the particular lifted function + respects the relation. With it such a definition would be impossible: + make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*} *) + +lemma card1_rsp: + fixes a b :: "'a list" + assumes e: "a \ b" + shows "card1 a = card1 b" + using e apply induct + apply (simp_all add:mem_respects) + done + +lemma card1_0: + fixes a :: "'a list" + shows "(card1 a = 0) = (a = [])" + apply (induct a) + apply (simp) + apply (simp_all) + apply meson + apply (simp_all) + done + +lemma not_mem_card1: + fixes x :: "'a" + fixes xs :: "'a list" + shows "~(x memb xs) \ card1 (x # xs) = Suc (card1 xs)" + by simp + + +lemma mem_cons: + fixes x :: "'a" + fixes xs :: "'a list" + assumes a : "x memb xs" + shows "x # xs \ xs" + using a apply (induct xs) + apply (simp_all) + apply (meson) + apply (simp_all add: list_eq.intros(4)) + proof - + fix a :: "'a" + fix xs :: "'a list" + assume a1 : "x # xs \ xs" + assume a2 : "x memb xs" + have a3 : "x # a # xs \ a # x # xs" using list_eq.intros(1)[of "x"] by blast + have a4 : "a # x # xs \ a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp + then show "x # a # xs \ a # xs" using a3 list_eq.intros(6) by blast + qed + +lemma card1_suc: + fixes xs :: "'a list" + fixes n :: "nat" + assumes c: "card1 xs = Suc n" + shows "\a ys. ~(a memb ys) \ xs \ (a # ys)" + using c apply (induct xs) + apply (simp) +(* apply (rule allI)*) + proof - + fix a :: "'a" + fix xs :: "'a list" + fix n :: "nat" + assume a1: "card1 xs = Suc n \ \a ys. \ a memb ys \ xs \ a # ys" + assume a2: "card1 (a # xs) = Suc n" + from a1 a2 show "\aa ys. \ aa memb ys \ a # xs \ aa # ys" + apply - + apply (rule True_or_False [of "a memb xs", THEN disjE]) + apply (simp_all add: card1_cons if_True simp_thms) + proof - + assume a1: "\a ys. \ a memb ys \ xs \ a # ys" + assume a2: "card1 xs = Suc n" + assume a3: "a memb xs" + from a1 obtain b ys where a5: "\ b memb ys \ xs \ b # ys" by blast + from a2 a3 a5 show "\aa ys. \ aa memb ys \ a # xs \ aa # ys" + apply - + apply (rule_tac x = "b" in exI) + apply (rule_tac x = "ys" in exI) + apply (simp_all) + proof - + assume a1: "a memb xs" + assume a2: "\ b memb ys \ xs \ b # ys" + then have a3: "xs \ b # ys" by simp + have "a # xs \ xs" using a1 mem_cons[of "a" "xs"] by simp + then show "a # xs \ b # ys" using a3 list_eq.intros(6) by blast + qed +next + assume a2: "\ a memb xs" + from a2 show "\aa ys. \ aa memb ys \ a # xs \ aa # ys" + apply - + apply (rule_tac x = "a" in exI) + apply (rule_tac x = "xs" in exI) + apply (simp) + apply (rule list_eq_sym) + done + qed +qed + lemma cons_preserves: fixes z assumes a: "xs \ ys" shows "(z # xs) \ (z # ys)" using a by (rule QuotMain.list_eq.intros(5)) -(* cu: what does unlam do? *) + +text {* + unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)' + to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left. +*} + ML {* -fun unlam_def orig_ctxt ctxt t = +fun unlam_def_aux orig_ctxt ctxt t = let val rhs = Thm.rhs_of t in (case try (Thm.dest_abs NONE) rhs of SOME (v, vt) => @@ -654,9 +760,11 @@ val nv = Free(vnname, vt) val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 - in unlam_def orig_ctxt ctxt tnorm end + in unlam_def_aux orig_ctxt ctxt tnorm end | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) - end + end; + +fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t *} local_setup {* @@ -666,7 +774,7 @@ term membship term IN thm IN_def -ML {* unlam_def @{context} @{context} @{thm IN_def} *} +ML {* unlam_def @{context} @{thm IN_def} *} lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] @@ -773,17 +881,20 @@ end | build_aux x = if is_const x then maybe_mk_rep_abs x else x - val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) + val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm); + val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm); + val concl2 = Logic.list_implies (prems, concl) +(* val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*) in - HOLogic.mk_eq ((build_aux concl), concl) + HOLogic.mk_eq ((build_aux concl2), concl2) end *} -ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *} -ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} -ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} -ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} -ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} -ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def CARD_def INSERT_def} *} +ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} +ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} +ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} +ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *} +ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *} +ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *} ML {* @@ -863,11 +974,20 @@ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} +notation ( output) "prop" ("#_" [1000] 1000) + prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (tactic {* print_tac "" *}) + thm arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="] +(* apply (rule arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])*) + apply (subst arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="]) apply (tactic {* foo_tac' @{context} 1 *}) - done - + apply (tactic {* foo_tac' @{context} 1 *}) + thm arg_cong2 [of "x memb []" "x memb []" False False "op ="] + (*apply (rule arg_cong2 [of "x memb []" "x memb []" False False "op ="]) + done *) + sorry thm length_append (* Not true but worth checking that the goal is correct *) ML {* @@ -878,7 +998,7 @@ *} prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (tactic {* foo_tac' @{context} 1 *}) +(* apply (tactic {* foo_tac' @{context} 1 *})*) sorry thm m2 @@ -890,8 +1010,8 @@ *} prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (tactic {* foo_tac' @{context} 1 *}) - done +(* apply (tactic {* foo_tac' @{context} 1 *}) + done *) sorry thm list_eq.intros(4) ML {* @@ -903,7 +1023,10 @@ *} (* It is the same, but we need a name for it. *) -prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry +prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} + apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (tactic {* foo_tac' @{context} 1 *}) + sorry lemma zzz : "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \ REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \ a # xs)" @@ -931,11 +1054,31 @@ ) *} +thm sym +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm sym})) + val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs +*} +ML {* + val cgoal = + Toplevel.program (fn () => + cterm_of @{theory} goal + ) +*} + + thm list_eq.intros(5) ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs - val cgoal = cterm_of @{theory} goal +*} +ML {* + val cgoal = + Toplevel.program (fn () => + cterm_of @{theory} goal + ) +*} +ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} @@ -943,6 +1086,40 @@ apply (tactic {* foo_tac' @{context} 1 *}) done + +thm list.induct +ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *} + +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct})) +*} +ML {* + val goal = + Toplevel.program (fn () => + build_goal m1_novars consts @{typ "'a list"} mk_rep_abs + ) +*} +ML {* + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) +*} + + +thm card1_suc + +ML {* + val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) +*} +ML {* + val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs +*} +ML {* + val cgoal = cterm_of @{theory} goal + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) +*} + + + (* datatype obj1 = OVAR1 "string"