src/HOL/Subst/Unify.ML

 
 (*---------------------------------------------------------------------------
  * Termination proof.
  *---------------------------------------------------------------------------*)
 
-goalw Unify.thy [unifyRel_def, measure_def] "trans unifyRel";
+Goalw [unifyRel_def, measure_def] "trans unifyRel";
 by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, 
 			 trans_finite_psubset, trans_less_than,
 			 trans_inv_image] 1));
 qed "trans_unifyRel";
 

 (*---------------------------------------------------------------------------
  * The following lemma is used in the last step of the termination proof for 
  * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
  * about term structure.
  *---------------------------------------------------------------------------*)
-goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
+Goalw [unifyRel_def,lex_prod_def, inv_image_def]
      "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
     \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
 by (asm_full_simp_tac (simpset() addsimps [measure_def, 
                           less_eq, inv_image_def,add_assoc]) 1);
 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \

 
 (*---------------------------------------------------------------------------
  * This lemma proves the nested termination condition for the base cases 
  * 3, 4, and 6. 
  *---------------------------------------------------------------------------*)
-goal Unify.thy
+Goal
  "!!x. ~(Var x <: M) ==>        \
 \   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
 \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
 by (case_tac "Var x = M" 1);
 by (hyp_subst_tac 1);

 (*---------------------------------------------------------------------------
  * Now for elimination of nested TC from unify.rules and induction. 
  *---------------------------------------------------------------------------*)
 
 (*Desired rule, copied from the theory file.  Could it be made available?*)
-goal Unify.thy 
+Goal 
   "unify(Comb M1 N1, Comb M2 N2) =      \
 \      (case unify(M1,M2)               \
 \        of None => None                \
 \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
 \                            of None => None    \

  * algorithm terminates and is not needed to prove the algorithm correct, 
  * if you are only interested in an MGU.  This is in contrast to the
  * approach of M&W, who used idempotence and MGU-ness in the termination proof.
  *---------------------------------------------------------------------------*)
 
-goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
+Goal "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
 by (ALLGOALS Asm_simp_tac);
 (*Const-Const case*)
 by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
 (*Const-Var case*)

 
 
 (*---------------------------------------------------------------------------
  * Unify returns idempotent substitutions, when it succeeds.
  *---------------------------------------------------------------------------*)
-goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta";
+Goal "!theta. unify(M,N) = Some theta --> Idem theta";
 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
 by (ALLGOALS 
     (asm_simp_tac 
        (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
 (*Comb-Comb case*)