src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35774 218e9766a848
parent 35663 ada7bc39c6b1
child 35775 9b7e2e17be69
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 14:30:38 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 15:18:25 2010 -0800
     1.3 @@ -16,7 +16,7 @@
     1.4      -> theory -> thm list * theory;
     1.5  
     1.6    val comp_theorems :
     1.7 -      bstring * Domain_Library.eq list ->
     1.8 +      binding * Domain_Library.eq list ->
     1.9        Domain_Take_Proofs.take_induct_info ->
    1.10        theory -> thm list * theory
    1.11  
    1.12 @@ -207,11 +207,12 @@
    1.13  (******************************************************************************)
    1.14  
    1.15  fun prove_induction
    1.16 -    (comp_dnam, eqs : eq list)
    1.17 +    (comp_dbind : binding, eqs : eq list)
    1.18      (take_rews : thm list)
    1.19      (take_info : Domain_Take_Proofs.take_induct_info)
    1.20      (thy : theory) =
    1.21  let
    1.22 +  val comp_dname = Sign.full_name thy comp_dbind;
    1.23    val dnames = map (fst o fst) eqs;
    1.24    val conss  = map  snd        eqs;
    1.25    fun dc_take dn = %%:(dn^"_take");
    1.26 @@ -286,7 +287,7 @@
    1.27      val is_emptys = map warn n__eqs;
    1.28      val is_finite = #is_finite take_info;
    1.29      val _ = if is_finite
    1.30 -            then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
    1.31 +            then message ("Proving finiteness rule for domain "^comp_dname^" ...")
    1.32              else ();
    1.33    end;
    1.34    val _ = trace " Proving finite_ind...";
    1.35 @@ -400,12 +401,12 @@
    1.36      ((Binding.empty, [rule]),
    1.37       [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
    1.38  
    1.39 -in thy |> Sign.add_path comp_dnam
    1.40 -       |> snd o PureThy.add_thmss [
    1.41 -           ((Binding.name "finite_ind" , [finite_ind]), []),
    1.42 -           ((Binding.name "ind"        , [ind]       ), [])]
    1.43 -       |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
    1.44 -       |> Sign.parent_path
    1.45 +in
    1.46 +  thy
    1.47 +  |> snd o PureThy.add_thmss [
    1.48 +     ((Binding.qualified true "finite_ind" comp_dbind, [finite_ind]), []),
    1.49 +     ((Binding.qualified true "ind"        comp_dbind, [ind]       ), [])]
    1.50 +  |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
    1.51  end; (* prove_induction *)
    1.52  
    1.53  (******************************************************************************)
    1.54 @@ -413,13 +414,13 @@
    1.55  (******************************************************************************)
    1.56  
    1.57  fun prove_coinduction
    1.58 -    (comp_dnam, eqs : eq list)
    1.59 +    (comp_dbind : binding, eqs : eq list)
    1.60      (take_lemmas : thm list)
    1.61      (thy : theory) : theory =
    1.62  let
    1.63  
    1.64  val dnames = map (fst o fst) eqs;
    1.65 -val comp_dname = Sign.full_bname thy comp_dnam;
    1.66 +val comp_dname = Sign.full_name thy comp_dbind;
    1.67  fun dc_take dn = %%:(dn^"_take");
    1.68  val x_name = idx_name dnames "x"; 
    1.69  val n_eqs = length eqs;
    1.70 @@ -433,7 +434,7 @@
    1.71    open HOLCF_Library
    1.72    val dtypes  = map (Type o fst) eqs;
    1.73    val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
    1.74 -  val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
    1.75 +  val bisim_bind = Binding.suffix_name "_bisim" comp_dbind;
    1.76    val bisim_type = relprod --> boolT;
    1.77  in
    1.78    val (bisim_const, thy) =
    1.79 @@ -449,10 +450,6 @@
    1.80    fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
    1.81    fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
    1.82  
    1.83 -  val comp_dname = Sign.full_bname thy comp_dnam;
    1.84 -  val dnames = map (fst o fst) eqs;
    1.85 -  val x_name = idx_name dnames "x"; 
    1.86 -
    1.87    fun one_con (con, args) =
    1.88      let
    1.89        val nonrec_args = filter_out is_rec args;
    1.90 @@ -494,11 +491,9 @@
    1.91           mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
    1.92  
    1.93  in
    1.94 -  val ([ax_bisim_def], thy) =
    1.95 -      thy
    1.96 -        |> Sign.add_path comp_dnam
    1.97 -        |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
    1.98 -        ||> Sign.parent_path;
    1.99 +  val (ax_bisim_def, thy) =
   1.100 +      yield_singleton add_defs_infer
   1.101 +        (Binding.qualified true "bisim_def" comp_dbind, bisim_eqn) thy;
   1.102  end; (* local *)
   1.103  
   1.104  (* ----- theorem concerning coinduction ------------------------------------- *)
   1.105 @@ -555,20 +550,19 @@
   1.106      in pg [] goal (K tacs) end;
   1.107  end; (* local *)
   1.108  
   1.109 -in thy |> Sign.add_path comp_dnam
   1.110 -       |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
   1.111 -       |> Sign.parent_path
   1.112 +in thy |> snd o PureThy.add_thmss
   1.113 +                  [((Binding.qualified true "coind" comp_dbind, [coind]), [])]
   1.114  end; (* let *)
   1.115  
   1.116  fun comp_theorems
   1.117 -    (comp_dnam : string, eqs : eq list)
   1.118 +    (comp_dbind : binding, eqs : eq list)
   1.119      (take_info : Domain_Take_Proofs.take_induct_info)
   1.120      (thy : theory) =
   1.121  let
   1.122  val map_tab = Domain_Take_Proofs.get_map_tab thy;
   1.123  
   1.124  val dnames = map (fst o fst) eqs;
   1.125 -val comp_dname = Sign.full_bname thy comp_dnam;
   1.126 +val comp_dname = Sign.full_name thy comp_dbind;
   1.127  
   1.128  (* ----- getting the composite axiom and definitions ------------------------ *)
   1.129  
   1.130 @@ -596,11 +590,11 @@
   1.131  (* prove induction rules, unless definition is indirect recursive *)
   1.132  val thy =
   1.133      if is_indirect then thy else
   1.134 -    prove_induction (comp_dnam, eqs) take_rews take_info thy;
   1.135 +    prove_induction (comp_dbind, eqs) take_rews take_info thy;
   1.136  
   1.137  val thy =
   1.138      if is_indirect then thy else
   1.139 -    prove_coinduction (comp_dnam, eqs) take_lemmas thy;
   1.140 +    prove_coinduction (comp_dbind, eqs) take_lemmas thy;
   1.141  
   1.142  in
   1.143    (take_rews, thy)