Simplified proofs using expand_option_case
authorpaulson
Mon May 26 12:32:35 1997 +0200 (1997-05-26)
changeset 3334ec558598ee1d
parent 3333 0bbf06e86c06
child 3335 b0139b83a5ee
Simplified proofs using expand_option_case
src/HOL/Subst/Unify.ML
     1.1 --- a/src/HOL/Subst/Unify.ML	Mon May 26 12:29:55 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Mon May 26 12:32:35 1997 +0200
     1.3 @@ -160,18 +160,11 @@
     1.4  			inv_image_def, less_eq]) 1);
     1.5  (** LEVEL 7 **)
     1.6  (*Comb-Comb case*)
     1.7 -by (option_case_tac "unify(M1a, M2a)" 1);
     1.8 -by (rename_tac "theta" 1);
     1.9 -by (option_case_tac "unify(N1 <| theta, N2 <| theta)" 1);
    1.10 -by (rename_tac "sigma" 1);
    1.11 -by (REPEAT (rtac allI 1));
    1.12 -by (rename_tac "P Q" 1); 
    1.13 +by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
    1.14 +by (strip_tac 1);
    1.15  by (rtac (trans_unifyRel RS transD) 1);
    1.16  by (Blast_tac 1);
    1.17  by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
    1.18 -by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \
    1.19 -                \ (Comb M1a (Comb N1 P), Comb M2a (Comb N2 Q))) :unifyRel" 1);
    1.20 -by (asm_simp_tac HOL_ss 2);
    1.21  by (rtac Rassoc 1);
    1.22  by (Blast_tac 1);
    1.23  qed_spec_mp "unify_TC";
    1.24 @@ -189,9 +182,8 @@
    1.25  \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
    1.26  \                            of None => None    \
    1.27  \                             | Some sigma => Some (theta <> sigma)))";
    1.28 -by (asm_simp_tac (!simpset addsimps unifyRules0) 1);
    1.29 -by (option_case_tac "unify(M1, M2)" 1);
    1.30 -by (asm_simp_tac (!simpset addsimps [unify_TC]) 1);
    1.31 +by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
    1.32 +			   setloop split_tac [expand_option_case]) 1);
    1.33  qed "unifyCombComb";
    1.34  
    1.35  
    1.36 @@ -225,21 +217,16 @@
    1.37  (*Comb-Var case*)
    1.38  by (stac mgu_sym 1);
    1.39  by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
    1.40 +(** LEVEL 8 **)
    1.41  (*Comb-Comb case*)
    1.42 -by (safe_tac (!claset));
    1.43 -by (option_case_tac "unify(M1, M2)" 1);
    1.44 -by (option_case_tac "unify(N1 <| a, N2 <| a)" 1);
    1.45 -by (hyp_subst_tac 1);
    1.46 -by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1);
    1.47 -(** LEVEL 13 **)
    1.48 -by (safe_tac (!claset));
    1.49 -by (rename_tac "theta sigma gamma" 1);
    1.50 -by (rewrite_goals_tac [MoreGeneral_def]);
    1.51 -by (rotate_tac ~3 1);
    1.52 -by (eres_inst_tac [("x","gamma")] allE 1);
    1.53 -by (Asm_full_simp_tac 1);
    1.54 -by (etac exE 1);
    1.55 -by (rename_tac "delta" 1);
    1.56 +by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
    1.57 +by (strip_tac 1);
    1.58 +by (rotate_tac ~2 1);
    1.59 +by (asm_full_simp_tac 
    1.60 +    (!simpset addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
    1.61 +by (safe_tac (!claset) THEN rename_tac "theta sigma gamma" 1);
    1.62 +by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
    1.63 +by (etac exE 1 THEN rename_tac "delta" 1);
    1.64  by (eres_inst_tac [("x","delta")] allE 1);
    1.65  by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
    1.66  (*Proving the subgoal*)
    1.67 @@ -255,12 +242,13 @@
    1.68   *---------------------------------------------------------------------------*)
    1.69  goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta";
    1.70  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
    1.71 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem] 
    1.72 -			             setloop split_tac[expand_if])));
    1.73 +by (ALLGOALS 
    1.74 +    (asm_simp_tac 
    1.75 +       (!simpset addsimps [Var_Idem] 
    1.76 +	         setloop split_tac[expand_if, expand_option_case])));
    1.77  (*Comb-Comb case*)
    1.78  by (safe_tac (!claset));
    1.79 -by (option_case_tac "unify(M1, M2)" 1);
    1.80 -by (option_case_tac "unify(N1 <| a, N2 <| a)" 1);
    1.81 +by (REPEAT (dtac spec 1 THEN mp_tac 1));
    1.82  by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
    1.83  by (rtac Idem_comp 1);
    1.84  by (atac 1);