src/HOL/Subst/Unify.ML
changeset 4089 96fba19bcbe2
parent 4071 4747aefbbc52
child 4153 e534c4c32d54
     1.1 --- a/src/HOL/Subst/Unify.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Subst/Unify.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -40,16 +40,16 @@
     1.4   *---------------------------------------------------------------------------*)
     1.5  Tfl.tgoalw Unify.thy [] unify.rules;
     1.6  (* Wellfoundedness of unifyRel *)
     1.7 -by (simp_tac (!simpset addsimps [unifyRel_def,
     1.8 +by (simp_tac (simpset() addsimps [unifyRel_def,
     1.9  				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
    1.10  				 wf_measure]) 1);
    1.11  (* TC *)
    1.12  by Safe_tac;
    1.13 -by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
    1.14 +by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
    1.15  				 lex_prod_def, measure_def, inv_image_def]) 1);
    1.16  by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
    1.17  by (Blast_tac 1);
    1.18 -by (asm_simp_tac (!simpset addsimps [less_eq, less_add_Suc1]) 1);
    1.19 +by (asm_simp_tac (simpset() addsimps [less_eq, less_add_Suc1]) 1);
    1.20  qed "tc0";
    1.21  
    1.22  
    1.23 @@ -72,7 +72,7 @@
    1.24  goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
    1.25       "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
    1.26      \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
    1.27 -by (asm_full_simp_tac (!simpset addsimps [measure_def, 
    1.28 +by (asm_full_simp_tac (simpset() addsimps [measure_def, 
    1.29                            less_eq, inv_image_def,add_assoc]) 1);
    1.30  by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
    1.31                  \  (vars_of D Un vars_of E Un vars_of F)) = \
    1.32 @@ -97,30 +97,30 @@
    1.33  by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
    1.34  (*uterm_less case*)
    1.35  by (asm_simp_tac
    1.36 -    (!simpset addsimps [less_eq, unifyRel_def, lex_prod_def,
    1.37 +    (simpset() addsimps [less_eq, unifyRel_def, lex_prod_def,
    1.38  			measure_def, inv_image_def]) 1);
    1.39  by (Blast_tac 1);
    1.40  (*finite_psubset case*)
    1.41  by (simp_tac
    1.42 -    (!simpset addsimps [unifyRel_def, lex_prod_def,
    1.43 +    (simpset() addsimps [unifyRel_def, lex_prod_def,
    1.44  			measure_def, inv_image_def]) 1);
    1.45 -by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
    1.46 +by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
    1.47  				 psubset_def, set_eq_subset]) 1);
    1.48  by (Blast_tac 1);
    1.49  (** LEVEL 9 **)
    1.50  (*Final case, also finite_psubset*)
    1.51  by (simp_tac
    1.52 -    (!simpset addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
    1.53 +    (simpset() addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
    1.54  			lex_prod_def, measure_def, inv_image_def]) 1);
    1.55  by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1);
    1.56  by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3);
    1.57 -by (ALLGOALS (asm_simp_tac(!simpset addsimps [srange_iff, vars_iff_occseq])));
    1.58 +by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq])));
    1.59  by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
    1.60  by (ALLGOALS (asm_full_simp_tac 
    1.61 -	      (!simpset addsimps [srange_iff, set_eq_subset]))); 
    1.62 +	      (simpset() addsimps [srange_iff, set_eq_subset]))); 
    1.63  by (ALLGOALS
    1.64 -    (fast_tac (!claset addEs [Var_intro RS disjE]
    1.65 -	               addss (!simpset addsimps [srange_iff]))));
    1.66 +    (fast_tac (claset() addEs [Var_intro RS disjE]
    1.67 +	               addss (simpset() addsimps [srange_iff]))));
    1.68  qed "var_elimR";
    1.69  
    1.70  
    1.71 @@ -153,15 +153,15 @@
    1.72  (* Apply induction *)
    1.73  by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
    1.74  by (ALLGOALS 
    1.75 -    (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
    1.76 +    (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)
    1.77  			    addsplits [expand_if])));
    1.78  (*Const-Const case*)
    1.79  by (simp_tac
    1.80 -    (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
    1.81 +    (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
    1.82  			inv_image_def, less_eq]) 1);
    1.83  (** LEVEL 7 **)
    1.84  (*Comb-Comb case*)
    1.85 -by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
    1.86 +by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
    1.87  by (strip_tac 1);
    1.88  by (rtac (trans_unifyRel RS transD) 1);
    1.89  by (Blast_tac 1);
    1.90 @@ -183,7 +183,7 @@
    1.91  \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
    1.92  \                            of None => None    \
    1.93  \                             | Some sigma => Some (theta <> sigma)))";
    1.94 -by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
    1.95 +by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
    1.96  			   addsplits [split_option_case]) 1);
    1.97  qed "unifyCombComb";
    1.98  
    1.99 @@ -194,7 +194,7 @@
   1.100  
   1.101  bind_thm ("unifyInduct",
   1.102  	  rule_by_tactic
   1.103 -	     (ALLGOALS (full_simp_tac (!simpset addsimps [unify_TC])))
   1.104 +	     (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC])))
   1.105  	     unifyInduct0);
   1.106  
   1.107  
   1.108 @@ -207,33 +207,33 @@
   1.109  
   1.110  goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
   1.111  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   1.112 -by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   1.113 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.114  (*Const-Const case*)
   1.115 -by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
   1.116 +by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
   1.117  (*Const-Var case*)
   1.118  by (stac mgu_sym 1);
   1.119 -by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   1.120 +by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
   1.121  (*Var-M case*)
   1.122 -by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   1.123 +by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
   1.124  (*Comb-Var case*)
   1.125  by (stac mgu_sym 1);
   1.126 -by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   1.127 +by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
   1.128  (** LEVEL 8 **)
   1.129  (*Comb-Comb case*)
   1.130 -by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
   1.131 +by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
   1.132  by (strip_tac 1);
   1.133  by (rotate_tac ~2 1);
   1.134  by (asm_full_simp_tac 
   1.135 -    (!simpset addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
   1.136 -by (safe_tac (!claset) THEN rename_tac "theta sigma gamma" 1);
   1.137 +    (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
   1.138 +by (safe_tac (claset()) THEN rename_tac "theta sigma gamma" 1);
   1.139  by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
   1.140  by (etac exE 1 THEN rename_tac "delta" 1);
   1.141  by (eres_inst_tac [("x","delta")] allE 1);
   1.142  by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
   1.143  (*Proving the subgoal*)
   1.144 -by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2
   1.145 -    THEN blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
   1.146 -by (blast_tac (!claset addIs [subst_trans, subst_cong, 
   1.147 +by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2
   1.148 +    THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2);
   1.149 +by (blast_tac (claset() addIs [subst_trans, subst_cong, 
   1.150  			      comp_assoc RS subst_sym]) 1);
   1.151  qed_spec_mp "unify_gives_MGU";
   1.152  
   1.153 @@ -245,16 +245,16 @@
   1.154  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   1.155  by (ALLGOALS 
   1.156      (asm_simp_tac 
   1.157 -       (!simpset addsimps [Var_Idem] 
   1.158 +       (simpset() addsimps [Var_Idem] 
   1.159  	         addsplits [expand_if,split_option_case])));
   1.160  (*Comb-Comb case*)
   1.161 -by (safe_tac (!claset));
   1.162 +by (safe_tac (claset()));
   1.163  by (REPEAT (dtac spec 1 THEN mp_tac 1));
   1.164 -by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
   1.165 +by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
   1.166  by (rtac Idem_comp 1);
   1.167  by (atac 1);
   1.168  by (atac 1);
   1.169 -by (best_tac (!claset addss (!simpset addsimps 
   1.170 +by (best_tac (claset() addss (simpset() addsimps 
   1.171  			     [MoreGeneral_def, subst_eq_iff, Idem_def])) 1);
   1.172  qed_spec_mp "unify_gives_Idem";
   1.173