src/HOL/Datatype.ML
changeset 12918 bca45be2d25b
parent 11954 3d1780208bf3
child 14981 e73f8140af78
equal deleted inserted replaced
12917:0fd3caa5d8b2 12918:bca45be2d25b
    60   val recs = thms "prod.recs";
    60   val recs = thms "prod.recs";
    61   val simps = thms "prod.simps";
    61   val simps = thms "prod.simps";
    62   val size = thms "prod.size";
    62   val size = thms "prod.size";
    63 end;
    63 end;
    64 
    64 
       
    65 structure option =
       
    66 struct
       
    67   val distinct = thms "option.distinct";
       
    68   val inject = thms "option.inject";
       
    69   val exhaust = thm "option.exhaust";
       
    70   val cases = thms "option.cases";
       
    71   val split = thm "option.split";
       
    72   val split_asm = thm "option.split_asm";
       
    73   val induct = thm "option.induct";
       
    74   val recs = thms "option.recs";
       
    75   val simps = thms "option.simps";
       
    76   val size = thms "option.size";
       
    77 end;
    65 
    78 
    66 (** sum_case -- the selection operator for sums **)
    79 val elem_o2s = thm "elem_o2s";
    67 
    80 val not_None_eq = thm "not_None_eq";
    68 (*compatibility*)
    81 val not_Some_eq = thm "not_Some_eq";
    69 val [sum_case_Inl, sum_case_Inr] = sum.cases;
    82 val o2s_empty_eq = thm "o2s_empty_eq";
    70 bind_thm ("sum_case_Inl", sum_case_Inl);
    83 val option_caseE = thm "option_caseE";
    71 bind_thm ("sum_case_Inr", sum_case_Inr);
    84 val option_map_None = thm "option_map_None";
    72 
    85 val option_map_Some = thm "option_map_Some";
    73 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    86 val option_map_def = thm "option_map_def";
    74 by (EVERY1 [res_inst_tac [("s","s")] sumE,
    87 val option_map_eq_Some = thm "option_map_eq_Some";
    75             etac ssubst, rtac sum_case_Inl,
    88 val option_map_o_sum_case = thm "option_map_o_sum_case";
    76             etac ssubst, rtac sum_case_Inr]);
    89 val ospec = thm "ospec";
    77 qed "surjective_sum";
    90 val sum_case_inject = thm "sum_case_inject";
    78 
    91 val sum_case_weak_cong = thm "sum_case_weak_cong";
    79 (*Prevents simplification of f and g: much faster*)
    92 val surjective_sum = thm "surjective_sum";
    80 Goal "s=t ==> sum_case f g s = sum_case f g t";
       
    81 by (etac arg_cong 1);
       
    82 qed "sum_case_weak_cong";
       
    83 
       
    84 val [p1,p2] = Goal
       
    85   "[| sum_case f1 f2 = sum_case g1 g2;  \
       
    86 \     [| f1 = g1; f2 = g2 |] ==> P |] \
       
    87 \  ==> P";
       
    88 by (rtac p2 1);
       
    89 by (rtac ext 1);
       
    90 by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
       
    91 by (Asm_full_simp_tac 1);
       
    92 by (rtac ext 1);
       
    93 by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
       
    94 by (Asm_full_simp_tac 1);
       
    95 qed "sum_case_inject";