# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260192945 -3600
# Node ID 5d932e7a856cfd4002ff40339a6c937ec915fdd3
# Parent  1e07e38ed6c5e57c693bf2217a5f30e3a7050118
List moved after QuotMain

diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory FSet
-imports "../QuotMain"
+imports "../QuotMain" List
 begin
 
 inductive
diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx
-imports "../QuotMain"
+imports "../QuotList"
 begin
 
 fun
diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -118,7 +118,7 @@
 lemma mult_raw_rsp[quotient_rsp]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 apply(auto)
-apply(simp add: mult algebra_simps)
+apply(simp add: algebra_simps)
 sorry
 
 lemma le_raw_rsp[quotient_rsp]:
@@ -144,11 +144,11 @@
 lemma mult_assoc_raw:
   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
 by (cases i, cases j, cases k) 
-   (simp add: mult algebra_simps)
+   (simp add: algebra_simps)
 
 lemma mult_sym_raw:
   shows "mult_raw i j \<approx> mult_raw j i"
-by (cases i, cases j) (simp)
+by (cases i, cases j) (simp add: algebra_simps)
 
 lemma mult_one_raw:
   shows "mult_raw  (1, 0) i \<approx> i"
@@ -157,7 +157,7 @@
 lemma mult_plus_comm_raw:
   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 by (cases i, cases j, cases k) 
-   (simp add: mult algebra_simps)
+   (simp add: algebra_simps)
 
 lemma one_zero_distinct:
   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
@@ -297,7 +297,7 @@
   "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
 apply(cases i, cases j, cases k)
-apply(auto simp add: mult algebra_simps)
+apply(auto simp add: algebra_simps)
 sorry
 
 
@@ -383,13 +383,13 @@
 class number = -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
-use "~~/src/HOL/Tools/numeral.ML"
+(*use "~~/src/HOL/Tools/numeral.ML"
 
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
 use "~~/src/HOL/Tools/numeral_syntax.ML"
-(*
+
 setup NumeralSyntax.setup
 
 abbreviation
@@ -433,4 +433,4 @@
 
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
-*)
\ No newline at end of file
+*)
diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/Examples/LFex.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory LFex
-imports Nominal "../QuotMain"
+imports Nominal "../QuotList"
 begin
 
 atom_decl name ident
diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory LamEx
-imports Nominal "../QuotMain"
+imports Nominal "../QuotList"
 begin
 
 atom_decl name
diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/QuotList.thy
--- a/Quot/QuotList.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/QuotList.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotList
-imports QuotScript List
+imports QuotMain List
 begin
 
 fun
@@ -10,7 +10,9 @@
 | "list_rel R [] (x#xs) = False"
 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
 
-lemma list_equivp:
+declare [[map list = (map, list_rel)]]
+
+lemma list_equivp[quotient_equiv]:
   assumes a: "equivp R"
   shows "equivp (list_rel R)"
   unfolding equivp_def
@@ -38,7 +40,7 @@
   apply(metis)
   done
 
-lemma list_quotient:
+lemma list_quotient[quotient_thm]:
   assumes q: "Quotient R Abs Rep"
   shows "Quotient (list_rel R) (map Abs) (map Rep)"
   unfolding Quotient_def
@@ -57,13 +59,20 @@
   apply(rule list_rel_rel[OF q])
   done
 
+lemma map_id: "map id \<equiv> id"
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (rule_tac list="x" in list.induct)
+  apply (simp_all)
+  done
+
 
 lemma cons_prs:
   assumes q: "Quotient R Abs Rep"
   shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
 by (induct t) (simp_all add: Quotient_abs_rep[OF q])
 
-lemma cons_rsp:
+lemma cons_rsp[quotient_rsp]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_rel R ===> list_rel R) op # op #"
 by (auto)
@@ -73,7 +82,7 @@
   shows "map Abs [] \<equiv> []"
 by (simp)
 
-lemma nil_rsp:
+lemma nil_rsp[quotient_rsp]:
   assumes q: "Quotient R Abs Rep"
   shows "list_rel R [] []"
 by simp
@@ -132,7 +141,7 @@
          induct     doesn't accept 'rule'.
    that's why the proof uses manual generalisation and needs assumptions
    both in conclusion for induction and in assumptions. *)
-lemma foldl_rsp:
+lemma foldl_rsp[quotient_rsp]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
@@ -153,10 +162,6 @@
 
 (* TODO: Rest are unused *)
 
-lemma list_map_id:
-  shows "map (\<lambda>x. x) = (\<lambda>x. x)"
-  by simp
-
 lemma list_rel_eq:
   shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
diff -r 1e07e38ed6c5 -r 5d932e7a856c Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotMain
-imports QuotScript QuotList QuotProd Prove
+imports QuotScript QuotProd Prove
 uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
@@ -142,24 +142,24 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-declare [[map list = (map, list_rel)]]
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
+(* FIXME: This should throw an exception:
+declare [[map "option" = (bla, blu)]]
+*)
 
 (* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
-  fun_quotient list_quotient prod_quotient
+  fun_quotient prod_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp
+  quot_rel_rsp pair_rsp
 
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
 lemmas [quotient_equiv] =
-  identity_equivp list_equivp prod_equivp
+  identity_equivp prod_equivp
 
-
-ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 
@@ -217,21 +217,16 @@
 
 section {* infrastructure about id *}
 
+(* TODO: think where should this be *)
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
   by (rule eq_reflection) (simp add: prod_fun_def)
 
-lemma map_id: "map id \<equiv> id"
-  apply (rule eq_reflection)
-  apply (rule ext)
-  apply (rule_tac list="x" in list.induct)
-  apply (simp_all)
-  done
-
+(* FIXME: make it a list and add map_id to it *)
 lemmas id_simps =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
-  prod_fun_id map_id
+  prod_fun_id
 
 ML {*
 fun simp_ids thm =