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.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.97 -        |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
1.98 -        ||> Sign.parent_path;
1.99 +  val (ax_bisim_def, thy) =
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)
```