Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Examples/AbsRepTest.thy
changeset 787 5cf83fa5b36c
parent 786 d6407afb913c
child 790 3a48ffcf0f9a
equal deleted inserted replaced
786:d6407afb913c 787:5cf83fa5b36c 
     3 begin
 
     3 begin
 
     4 
     4 
     5 print_maps
 
     5 print_maps
 
     6 
     6 
     7 quotient_type 
     7 quotient_type 
     8   fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
     8   'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
       
     9   apply(rule equivpI)
 
       
    10   unfolding reflp_def symp_def transp_def
 
       
    11   apply(auto)
 
       
    12   done
 
       
    13 
       
    14 quotient_type 
       
    15   'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
     9   apply(rule equivpI)
 
    16   apply(rule equivpI)
 
    10   unfolding reflp_def symp_def transp_def
 
    17   unfolding reflp_def symp_def transp_def
 
    11   apply(auto)
 
    18   apply(auto)
 
    12   done
 
    19   done
 
    13 
    20 
    15 
    22 
    16 ML{*
 
    23 ML{*
 
    17 Quotient_Info.quotient_rules_get @{context}
 
    24 Quotient_Info.quotient_rules_get @{context}
 
    18 *}
 
    25 *}
 
    19 
    26 
    20 fun
 
    27 quotient_type int = "nat \<times> nat" / "\<lambda>(x, y) (u, v). x + v = u + (y::nat)"
 
    21   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 
    28   apply(rule equivpI)
 
    22 where
 
    29   unfolding reflp_def symp_def transp_def
 
    23   "intrel (x, y) (u, v) = (x + v = u + y)"
 
    30   apply(auto)
 
    24 
    31   done
 
    25 quotient_type int = "nat \<times> nat" / intrel
 
       
    26   sorry
 
       
    27 
    32 
    28 print_quotients
 
    33 print_quotients
 
    29 
    34 
    30 ML {*
 
    35 ML {*
 
    31 open Quotient_Term;
 
    36 open Quotient_Term;
 
    32 *}
 
    37 *}
 
    33 
    38 
    34 ML {*
 
    39 ML {*
 
    35 absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"})
 
    40 absrep_fun_chk absF @{context} 
       
    41      (@{typ "(('a * 'a) list) list"}, 
       
    42       @{typ "(('a * 'a) fset) fset"})
 
    36 |> Syntax.string_of_term @{context}
 
    43 |> Syntax.string_of_term @{context}
 
    37 |> writeln
 
    44 |> writeln
 
    38 *}
 
    45 *}
 
       
    46 
       
    47 (*
 
       
    48 ML {*
 
       
    49 absrep_fun_chk absF @{context} 
       
    50      (@{typ "('a * 'a) list"}, 
       
    51       @{typ "'a foo"})
 
       
    52 |> Syntax.string_of_term @{context}
 
       
    53 |> writeln
 
       
    54 *}
 
       
    55 *)
 
    39 
    56 
    40 term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"
 
    57 term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"
 
    41 term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"
 
    58 term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"
 
    42 term "option_map (map rep_int \<circ> rep_fset)"
 
    59 term "option_map (map rep_int \<circ> rep_fset)"
 
    43 term "option_map (abs_fset o (map abs_int))"
 
    60 term "option_map (abs_fset o (map abs_int))"
nominal2