Quot/Examples/FSet.thy
changeset 767 37285ec4387d
parent 766 df053507edba
child 768 e9e205b904e2
equal deleted inserted replaced
766:df053507edba 767:37285ec4387d
    24 
    24 
    25 quotient_type 
    25 quotient_type 
    26   fset = "'a list" / "list_eq"
    26   fset = "'a list" / "list_eq"
    27   by (rule equivp_list_eq)
    27   by (rule equivp_list_eq)
    28 
    28 
    29 quotient_def
    29 quotient_definition
    30    "EMPTY :: 'a fset"
    30    "EMPTY :: 'a fset"
    31 as
    31 as
    32   "[]::'a list"
    32   "[]::'a list"
    33 
    33 
    34 quotient_def
    34 quotient_definition
    35    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
    35    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
    36 as
    36 as
    37   "op #"
    37   "op #"
    38 
    38 
    39 quotient_def
    39 quotient_definition
    40    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
    40    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
    41 as
    41 as
    42   "op @"
    42   "op @"
    43 
    43 
    44 fun
    44 fun
    45   card1 :: "'a list \<Rightarrow> nat"
    45   card1 :: "'a list \<Rightarrow> nat"
    46 where
    46 where
    47   card1_nil: "(card1 []) = 0"
    47   card1_nil: "(card1 []) = 0"
    48 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
    48 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
    49 
    49 
    50 quotient_def
    50 quotient_definition
    51    "CARD :: 'a fset \<Rightarrow> nat"
    51    "CARD :: 'a fset \<Rightarrow> nat"
    52 as
    52 as
    53   "card1"
    53   "card1"
    54 
    54 
    55 (* text {*
    55 (* text {*
   108   apply (induct X)
   108   apply (induct X)
   109   apply (simp)
   109   apply (simp)
   110   apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
   110   apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
   111   done
   111   done
   112 
   112 
   113 quotient_def
   113 quotient_definition
   114    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
   114    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
   115 as
   115 as
   116   "op mem"
   116   "op mem"
   117 
   117 
   118 quotient_def
   118 quotient_definition
   119    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
   119    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
   120 as
   120 as
   121   "fold1"
   121   "fold1"
   122 
   122 
   123 quotient_def
   123 quotient_definition
   124   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
   124   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
   125 as
   125 as
   126   "map"
   126   "map"
   127 
   127 
   128 lemma mem_rsp:
   128 lemma mem_rsp:
   272 done
   272 done
   273 
   273 
   274 quotient_type fset2 = "'a list" / "list_eq"
   274 quotient_type fset2 = "'a list" / "list_eq"
   275   by (rule equivp_list_eq)
   275   by (rule equivp_list_eq)
   276 
   276 
   277 quotient_def
   277 quotient_definition
   278    "EMPTY2 :: 'a fset2"
   278    "EMPTY2 :: 'a fset2"
   279 as
   279 as
   280   "[]::'a list"
   280   "[]::'a list"
   281 
   281 
   282 quotient_def
   282 quotient_definition
   283    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
   283    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
   284 as
   284 as
   285   "op #"
   285   "op #"
   286 
   286 
   287 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
   287 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
   290 
   290 
   291 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"
   291 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"
   292 apply (lifting list_induct_part)
   292 apply (lifting list_induct_part)
   293 done
   293 done
   294 
   294 
   295 quotient_def
   295 quotient_definition
   296   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
   296   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
   297 as
   297 as
   298   "list_rec"
   298   "list_rec"
   299 
   299 
   300 quotient_def
   300 quotient_definition
   301   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
   301   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
   302 as
   302 as
   303   "list_case"
   303   "list_case"
   304 
   304 
   305 (* Probably not true without additional assumptions about the function *)
   305 (* Probably not true without additional assumptions about the function *)