--- a/Quot/Examples/FSet.thy Thu Dec 10 03:48:39 2009 +0100
+++ b/Quot/Examples/FSet.thy Thu Dec 10 04:23:13 2009 +0100
@@ -84,7 +84,7 @@
using c
apply(induct xs)
apply (metis Suc_neq_Zero card1_0)
-apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons)
+apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons)
done
definition
@@ -107,7 +107,7 @@
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
apply (induct X)
apply (simp)
- apply (metis List.member.simps(1) QUOT_TYPE_I_fset.R_trans list_eq_refl mem_cons)
+ apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
done
quotient_def
--- a/Quot/Examples/LFex.thy Thu Dec 10 03:48:39 2009 +0100
+++ b/Quot/Examples/LFex.thy Thu Dec 10 04:23:13 2009 +0100
@@ -80,8 +80,6 @@
and TRM = trm / atrm
by (auto intro: alpha_equivps)
-print_quotients
-
quotient_def
TYP :: "TYP :: KIND"
where
--- a/Quot/ROOT.ML Thu Dec 10 03:48:39 2009 +0100
+++ b/Quot/ROOT.ML Thu Dec 10 04:23:13 2009 +0100
@@ -3,6 +3,7 @@
no_document use_thys
["QuotMain",
"Examples/FSet",
+ "Examples/FSet2",
"Examples/IntEx",
"Examples/IntEx2",
"Examples/LFex",
--- a/Quot/quotient.ML Thu Dec 10 03:48:39 2009 +0100
+++ b/Quot/quotient.ML Thu Dec 10 04:23:13 2009 +0100
@@ -158,38 +158,11 @@
(* FIXME: the relation needs to be a string, since its type needs *)
(* FIXME: to recalculated in for example REGULARIZE *)
- (* storing of the equiv_thm under a name *)
- val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm,
- [internal_attr equiv_rules_add]) lthy3
-
- (* interpretation *)
- val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
- val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
- val eqn1i = Thm.prop_of (symmetric eqn1pre)
- val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
- val eqn2i = Thm.prop_of (symmetric eqn2pre)
-
- val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
- val exp_term = Morphism.term exp_morphism;
- val exp = Morphism.thm exp_morphism;
-
- val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
- ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
- val mthdt = Method.Basic (fn _ => mthd)
- val bymt = Proof.global_terminal_proof (mthdt, NONE)
- val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
- Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
in
- lthy6
+ lthy3
|> note (quot_thm_name, quot_thm, [])
||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
- ||> Local_Theory.theory (fn thy =>
- let
- val global_eqns = map exp_term [eqn2i, eqn1i];
- (* Not sure if the following context should not be used *)
- val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
- val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
- in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
+ ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add])
end
--- a/Unused.thy Thu Dec 10 03:48:39 2009 +0100
+++ b/Unused.thy Thu Dec 10 04:23:13 2009 +0100
@@ -97,3 +97,30 @@
(*lemma equality_twice:
"a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
by auto*)
+
+
+(*interpretation code *)
+(*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
+ val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
+ val eqn1i = Thm.prop_of (symmetric eqn1pre)
+ val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
+ val eqn2i = Thm.prop_of (symmetric eqn2pre)
+
+ val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
+ val exp_term = Morphism.term exp_morphism;
+ val exp = Morphism.thm exp_morphism;
+
+ val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
+ ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
+ val mthdt = Method.Basic (fn _ => mthd)
+ val bymt = Proof.global_terminal_proof (mthdt, NONE)
+ val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
+ Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*)
+
+(*||> Local_Theory.theory (fn thy =>
+ let
+ val global_eqns = map exp_term [eqn2i, eqn1i];
+ (* Not sure if the following context should not be used *)
+ val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
+ val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
+ in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)
\ No newline at end of file