--- 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 \<Rightarrow> trm \<Rightarrow> bool"
+axiomatization
+ RR :: "trm \<Rightarrow> trm \<Rightarrow> 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 \<approx> 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 "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (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 \<equiv> %x. %y. f x y
- to a theorem of the form
-
- c x y \<equiv> f x y
+ to a theorem of the form
+
+ c x y \<equiv> 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 "\<exists>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 *})