simpdata.ML
changeset 206 7b9a06035a92
parent 204 21c405b4039f
child 227 d0320f916936
equal deleted inserted replaced
205:ccbbe1264c0f 206:7b9a06035a92
    68   (fn [prem] => [rewtac prem, rtac refl 1]);
    68   (fn [prem] => [rewtac prem, rtac refl 1]);
    69 
    69 
    70 val eq_sym_conv = prover "(x=y) = (y=x)";
    70 val eq_sym_conv = prover "(x=y) = (y=x)";
    71 
    71 
    72 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
    72 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
    73 val conj_commute = prover "(P&Q) = (Q&P)";
       
    74 val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
       
    75 val conj_comms = [conj_commute, conj_left_commute];
       
    76 
    73 
    77 val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
    74 val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
    78  (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    75  (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    79 
    76 
    80 val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y"
    77 val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y"
    91  (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
    88  (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
    92 	 rtac (if_P RS ssubst) 2,
    89 	 rtac (if_P RS ssubst) 2,
    93 	 rtac (if_not_P RS ssubst) 1,
    90 	 rtac (if_not_P RS ssubst) 1,
    94 	 REPEAT(fast_tac HOL_cs 1) ]);
    91 	 REPEAT(fast_tac HOL_cs 1) ]);
    95 
    92 
       
    93 val if_bool_eq = prove_goal HOL.thy "if(P,Q,R) = ((P-->Q) & (~P-->R))"
       
    94   (fn _ => [rtac expand_if 1]);
       
    95 
    96 infix addcongs;
    96 infix addcongs;
    97 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    97 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    98 
    98 
    99 val mksimps_pairs =
    99 val mksimps_pairs =
   100   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   100   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   101    ("All", [spec]), ("True", []), ("False", [])];
   101    ("All", [spec]), ("True", []), ("False", []),
       
   102    ("if", [if_bool_eq RS iffD1])];
   102 
   103 
   103 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
   104 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
   104 
   105 
   105 val HOL_ss = empty_ss
   106 val HOL_ss = empty_ss
   106       setmksimps (mksimps mksimps_pairs)
   107       setmksimps (mksimps mksimps_pairs)
   149 val let_weak_cong = prove_goal HOL.thy
   150 val let_weak_cong = prove_goal HOL.thy
   150   "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
   151   "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
   151   (fn [prem] => [rtac (prem RS arg_cong) 1]);
   152   (fn [prem] => [rtac (prem RS arg_cong) 1]);
   152 
   153 
   153 end;
   154 end;
       
   155 
       
   156 fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]);
       
   157 
       
   158 prove "conj_commute" "(P&Q) = (Q&P)";
       
   159 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
       
   160 val conj_comms = [conj_commute, conj_left_commute];
       
   161 
       
   162 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
       
   163 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";