Removed rprod from the WF relation; simplified proofs;
authorpaulson
Wed May 21 10:53:02 1997 +0200 (1997-05-21)
changeset 326689e5f4163663
parent 3265 8358e19d0d4c
child 3267 7203f4dbc0c5
Removed rprod from the WF relation; simplified proofs;
induction rule is now curried
src/HOL/Subst/Unify.ML
     1.1 --- a/src/HOL/Subst/Unify.ML	Wed May 21 10:09:21 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Wed May 21 10:53:02 1997 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4  (*  Title:      Subst/Unify
     1.5 +    ID:         $Id$
     1.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.7      Copyright   1997  University of Cambridge
     1.8  
     1.9 @@ -39,41 +40,27 @@
    1.10   *---------------------------------------------------------------------------*)
    1.11  Tfl.tgoalw Unify.thy [] unify.rules;
    1.12  (* Wellfoundedness of unifyRel *)
    1.13 -by (simp_tac (!simpset addsimps [unifyRel_def, uterm_less_def,
    1.14 +by (simp_tac (!simpset addsimps [unifyRel_def,
    1.15  				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
    1.16  				 wf_rel_prod, wf_measure]) 1);
    1.17  (* TC *)
    1.18  by (Step_tac 1);
    1.19  by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
    1.20 -				 lex_prod_def, measure_def,
    1.21 -				 inv_image_def]) 1);
    1.22 +				 lex_prod_def, measure_def, inv_image_def]) 1);
    1.23  by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
    1.24  by (Blast_tac 1);
    1.25 -by (asm_simp_tac (!simpset addsimps [rprod_def, less_eq, less_add_Suc1]) 1);
    1.26 +by (asm_simp_tac (!simpset addsimps [less_eq, less_add_Suc1]) 1);
    1.27  qed "tc0";
    1.28  
    1.29  
    1.30  (*---------------------------------------------------------------------------
    1.31 - * Eliminate tc0 from the recursion equations and the induction theorem.
    1.32 - *---------------------------------------------------------------------------*)
    1.33 -val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
    1.34 -val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
    1.35 -                     unify.rules;
    1.36 -
    1.37 -val unifyInduct0 = [wfr,tc] MRS unify.induct 
    1.38 -                  |> read_instantiate [("P","split Q")]
    1.39 -                  |> rewrite_rule [split RS eq_reflection]
    1.40 -                  |> standard;
    1.41 -
    1.42 -
    1.43 -(*---------------------------------------------------------------------------
    1.44   * Termination proof.
    1.45   *---------------------------------------------------------------------------*)
    1.46  
    1.47 -goalw Unify.thy [unifyRel_def,uterm_less_def,measure_def] "trans unifyRel";
    1.48 +goalw Unify.thy [unifyRel_def, measure_def] "trans unifyRel";
    1.49  by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, 
    1.50  			 trans_finite_psubset, trans_less_than,
    1.51 -			 trans_rprod, trans_inv_image] 1));
    1.52 +			 trans_inv_image] 1));
    1.53  qed "trans_unifyRel";
    1.54  
    1.55  
    1.56 @@ -85,7 +72,7 @@
    1.57  goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
    1.58       "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
    1.59      \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
    1.60 -by (asm_full_simp_tac (!simpset addsimps [uterm_less_def, measure_def, rprod_def,
    1.61 +by (asm_full_simp_tac (!simpset addsimps [measure_def, 
    1.62                            less_eq, inv_image_def,add_assoc]) 1);
    1.63  by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
    1.64                  \  (vars_of D Un vars_of E Un vars_of F)) = \
    1.65 @@ -110,8 +97,7 @@
    1.66  by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
    1.67  (*uterm_less case*)
    1.68  by (asm_simp_tac
    1.69 -    (!simpset addsimps [less_eq, unifyRel_def, uterm_less_def,
    1.70 -			rprod_def, lex_prod_def,
    1.71 +    (!simpset addsimps [less_eq, unifyRel_def, lex_prod_def,
    1.72  			measure_def, inv_image_def]) 1);
    1.73  by (Blast_tac 1);
    1.74  (*finite_psubset case*)
    1.75 @@ -155,9 +141,19 @@
    1.76  
    1.77  
    1.78  (*---------------------------------------------------------------------------
    1.79 + * Eliminate tc0 from the recursion equations and the induction theorem.
    1.80 + *---------------------------------------------------------------------------*)
    1.81 +val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
    1.82 +val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
    1.83 +                     unify.rules;
    1.84 +
    1.85 +val unifyInduct0 = [wfr,tc] MRS unify.induct;
    1.86 +
    1.87 +
    1.88 +(*---------------------------------------------------------------------------
    1.89   * The nested TC. Proved by recursion induction.
    1.90   *---------------------------------------------------------------------------*)
    1.91 -val [tc1,tc2,tc3] = unify.tcs;
    1.92 +val [_,_,tc3] = unify.tcs;
    1.93  goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3));
    1.94  (*---------------------------------------------------------------------------
    1.95   * The extracted TC needs the scope of its quantifiers adjusted, so our 
    1.96 @@ -177,7 +173,7 @@
    1.97  (*Const-Const case*)
    1.98  by (simp_tac
    1.99      (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
   1.100 -			inv_image_def, less_eq, uterm_less_def, rprod_def]) 1);
   1.101 +			inv_image_def, less_eq]) 1);
   1.102  (** LEVEL 7 **)
   1.103  (*Comb-Comb case*)
   1.104  by (subst_case_tac "unify(M1a, M2a)");
   1.105 @@ -194,7 +190,7 @@
   1.106  by (asm_simp_tac HOL_ss 2);
   1.107  by (rtac Rassoc 1);
   1.108  by (Blast_tac 1);
   1.109 -qed_spec_mp "unify_TC2";
   1.110 +qed_spec_mp "unify_TC";
   1.111  
   1.112  
   1.113  (*---------------------------------------------------------------------------
   1.114 @@ -211,7 +207,7 @@
   1.115  \                             | Subst sigma => Subst (theta <> sigma)))";
   1.116  by (asm_simp_tac (!simpset addsimps unifyRules0) 1);
   1.117  by (subst_case_tac "unify(M1, M2)");
   1.118 -by (asm_simp_tac (!simpset addsimps [unify_TC2]) 1);
   1.119 +by (asm_simp_tac (!simpset addsimps [unify_TC]) 1);
   1.120  qed "unifyCombComb";
   1.121  
   1.122  
   1.123 @@ -219,20 +215,10 @@
   1.124  
   1.125  Addsimps unifyRules;
   1.126  
   1.127 -val prems = goal Unify.thy 
   1.128 -"   [| !!m n. Q (Const m) (Const n);      \
   1.129 -\      !!m M N. Q (Const m) (Comb M N); !!m x. Q (Const m) (Var x);     \
   1.130 -\      !!x M. Q (Var x) M; !!M N x. Q (Comb M N) (Const x);     \
   1.131 -\      !!M N x. Q (Comb M N) (Var x);   \
   1.132 -\      !!M1 N1 M2 N2.   \
   1.133 -\         (! theta.     \
   1.134 -\             unify (M1, M2) = Subst theta -->  \
   1.135 -\             Q (N1 <| theta) (N2 <| theta)) & Q M1 M2   \
   1.136 -\         ==> Q (Comb M1 N1) (Comb M2 N2) |] ==> Q M1 M2";
   1.137 -by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
   1.138 -by (ALLGOALS (asm_simp_tac (!simpset addsimps (unify_TC2::prems))));
   1.139 -qed "unifyInduct";
   1.140 -
   1.141 +bind_thm ("unifyInduct",
   1.142 +	  rule_by_tactic
   1.143 +	     (ALLGOALS (full_simp_tac (!simpset addsimps [unify_TC])))
   1.144 +	     unifyInduct0);
   1.145  
   1.146  
   1.147  (*---------------------------------------------------------------------------
   1.148 @@ -242,8 +228,8 @@
   1.149   * approach of M&W, who used idempotence and MGU-ness in the termination proof.
   1.150   *---------------------------------------------------------------------------*)
   1.151  
   1.152 -goal Unify.thy "!theta. unify(P,Q) = Subst theta --> MGUnifier theta P Q";
   1.153 -by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
   1.154 +goal Unify.thy "!theta. unify(M,N) = Subst theta --> MGUnifier theta M N";
   1.155 +by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1);
   1.156  by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   1.157  (*Const-Const case*)
   1.158  by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
   1.159 @@ -273,8 +259,8 @@
   1.160  by (eres_inst_tac [("x","delta")] allE 1);
   1.161  by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
   1.162  (*Proving the subgoal*)
   1.163 -by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2);
   1.164 -by (blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
   1.165 +by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2
   1.166 +    THEN blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
   1.167  by (blast_tac (!claset addIs [subst_trans, subst_cong, 
   1.168  			      comp_assoc RS subst_sym]) 1);
   1.169  qed_spec_mp "unify_gives_MGU";
   1.170 @@ -283,30 +269,19 @@
   1.171  (*---------------------------------------------------------------------------
   1.172   * Unify returns idempotent substitutions, when it succeeds.
   1.173   *---------------------------------------------------------------------------*)
   1.174 -goal Unify.thy "!theta. unify(P,Q) = Subst theta --> Idem theta";
   1.175 -by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
   1.176 +goal Unify.thy "!theta. unify(M,N) = Subst theta --> Idem theta";
   1.177 +by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1);
   1.178  by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem] 
   1.179  			             setloop split_tac[expand_if])));
   1.180  (*Comb-Comb case*)
   1.181  by (safe_tac (!claset));
   1.182  by (subst_case_tac "unify(M1, M2)");
   1.183  by (subst_case_tac "unify(N1 <| list, N2 <| list)");
   1.184 -by (hyp_subst_tac 1);
   1.185 -by prune_params_tac;
   1.186 -by (rename_tac "theta sigma" 1);
   1.187 -(** LEVEL 8 **)
   1.188 -by (dtac unify_gives_MGU 1);
   1.189 -by (dtac unify_gives_MGU 1);
   1.190 -by (rewrite_tac [MGUnifier_def]);
   1.191 -by (safe_tac (!claset));
   1.192 +by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
   1.193  by (rtac Idem_comp 1);
   1.194  by (atac 1);
   1.195  by (atac 1);
   1.196 -
   1.197 -by (eres_inst_tac [("x","q")] allE 1);
   1.198 -by (asm_full_simp_tac (!simpset addsimps [MoreGeneral_def]) 1);
   1.199 -by (safe_tac (!claset));
   1.200 -by (asm_full_simp_tac
   1.201 -    (!simpset addsimps [srange_iff, subst_eq_iff, Idem_def]) 1);
   1.202 +by (best_tac (!claset addss (!simpset addsimps 
   1.203 +			     [MoreGeneral_def, subst_eq_iff, Idem_def])) 1);
   1.204  qed_spec_mp "unify_gives_Idem";
   1.205