diff -r f078dbf557b7 -r d98224cafb86 QuotMain.thy --- a/QuotMain.thy Mon Sep 28 19:10:27 2009 +0200 +++ b/QuotMain.thy Mon Sep 28 19:15:19 2009 +0200 @@ -151,18 +151,18 @@ |> map Free in lambda c - (HOLogic.exists_const ty $ + (HOLogic.exists_const ty $ lambda x (HOLogic.mk_eq (c, (rel $ x)))) end (* makes the new type definitions and proves non-emptyness*) fun typedef_make (qty_name, rel, ty) lthy = -let +let val typedef_tac = EVERY1 [rewrite_goal_tac @{thms mem_def}, - rtac @{thm exI}, - rtac @{thm exI}, + rtac @{thm exI}, + rtac @{thm exI}, rtac @{thm refl}] in LocalTheory.theory_result @@ -217,7 +217,7 @@ rtac @{thm QUOT_TYPE.QUOTIENT}, rtac quot_type_thm] in - Goal.prove lthy [] [] goal + Goal.prove lthy [] [] goal (K typedef_quotient_thm_tac) end *} @@ -324,8 +324,8 @@ | app "trm" "trm" | lam "nat" "trm" -axiomatization - RR :: "trm \ trm \ bool" +axiomatization + RR :: "trm \ trm \ bool" where r_eq: "EQUIV RR" @@ -480,7 +480,7 @@ ML {* fun exchange_ty rty qty ty = - if ty = rty + if ty = rty then qty else (case ty of @@ -674,7 +674,7 @@ fixes xs :: "'a list" assumes a : "x memb xs" shows "x # xs \ xs" - using a + using a apply (induct xs) apply (auto intro: list_eq.intros) done @@ -684,10 +684,10 @@ fixes n :: "nat" assumes c: "card1 xs = Suc n" shows "\a ys. ~(a memb ys) \ xs \ (a # ys)" - using c + using c apply(induct xs) apply (metis Suc_neq_Zero card1_0) -apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons) +apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons) done lemma cons_preserves: @@ -698,13 +698,13 @@ text {* - Unlam_def converts a definition given as + Unlam_def converts a definition given as c \ %x. %y. f x y - to a theorem of the form - - c x y \ f x y + to a theorem of the form + + c x y \ f x y This function is needed to rewrite the right-hand side to the left-hand side. @@ -817,8 +817,8 @@ ML {* fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) - val consts = [@{const_name "Nil"}, @{const_name "append"}, - @{const_name "Cons"}, @{const_name "membship"}, + val consts = [@{const_name "Nil"}, @{const_name "append"}, + @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}] *} @@ -865,7 +865,7 @@ let fun is_const (Const (x, t)) = member (op =) constructors x | is_const _ = false - + fun maybe_mk_rep_abs t = let val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t) @@ -892,7 +892,7 @@ end | build_aux _ x = if is_const x then maybe_mk_rep_abs x else x - + val concl2 = term_of (#prop (crep_thm thm)) in Logic.mk_equals (build_aux ctxt concl2, concl2) @@ -1004,16 +1004,8 @@ *} ML {* -<<<<<<< variant A val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs ->>>>>>> variant B - val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) - val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs -####### Ancestor - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) - val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs -======= end val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} @@ -1043,17 +1035,13 @@ prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (atomize (full)) - - apply (rule trueprop_cong) apply (tactic {* foo_tac' @{context} 1 *}) - thm eq_reflection done thm length_append (* Not true but worth checking that the goal is correct *) ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) - val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs + val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} @@ -1065,7 +1053,7 @@ thm m2 ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) - val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs + val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} @@ -1077,7 +1065,7 @@ thm list_eq.intros(4) ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) - val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs + val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) @@ -1105,7 +1093,7 @@ 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 goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs *} ML {* val cgoal = @@ -1148,7 +1136,7 @@ fun lift_theorem_fset_aux thm lthy = let val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; - val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs; + val goal = build_goal @{context} novars consts @{typ "'a list"} mk_rep_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 (foo_tac' @{context}) 1; @@ -1237,7 +1225,7 @@ ML {* @{term "\x. P x"} *} ML {* Thm.bicompose *} prove {* (Thm.term_of cgoal2) *} - apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (tactic {* foo_tac' @{context} 1 *})