merged
authorwenzelm
Wed, 25 Sep 2013 12:52:21 +0200
changeset 53874 7cec5a4d5532
parent 53871 a1a52423601f (diff)
parent 53873 08594daabcd9 (current diff)
child 53877 028ec3e310ec
merged
--- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 25 12:52:21 2013 +0200
@@ -172,15 +172,6 @@
    (if b then f y else if b' then x' else f y')"
   by simp
 
-lemma if_then_else_True_False:
-  "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
-  "(if p then True else r) \<longleftrightarrow> p \<or> r"
-  "(if p then q else False) \<longleftrightarrow> p \<and> q"
-  "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
-by simp_all
-
-lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
-
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 12:52:21 2013 +0200
@@ -30,6 +30,7 @@
      case_conv_ifs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
+  val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
 
   val rep_compat_prefix: string
 
@@ -39,9 +40,9 @@
   val mk_ctr: typ list -> term -> term
   val mk_case: typ list -> typ -> term -> term
   val mk_disc_or_sel: typ list -> term -> term
-
   val name_of_ctr: term -> string
   val name_of_disc: term -> string
+  val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
 
   val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (((bool * bool) * term list) * binding) *
@@ -103,6 +104,27 @@
    expands = map (Morphism.thm phi) expands,
    case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
 
+fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
+    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
+  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
+
+structure Data = Generic_Data
+(
+  type T = ctr_sugar Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  val merge = Symtab.merge eq_ctr_sugar;
+);
+
+fun ctr_sugar_of ctxt =
+  Symtab.lookup (Data.get (Context.Proof ctxt))
+  #> Option.map (morph_ctr_sugar
+    (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
+
+fun register_ctr_sugar key ctr_sugar =
+  Local_Theory.declaration {syntax = false, pervasive = true}
+    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
+
 val rep_compat_prefix = "new";
 
 val isN = "is_";
@@ -193,6 +215,28 @@
 
 val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
 
+fun dest_case ctxt s Ts t =
+  (case Term.strip_comb t of
+    (Const (c, _), args as _ :: _) =>
+    (case ctr_sugar_of ctxt s of
+      SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
+      if case_name = c then
+        let
+          val n = length discs0;
+          val (branches, obj :: leftovers) = chop n args;
+          val discs = map (mk_disc_or_sel Ts) discs0;
+          val selss = map (map (mk_disc_or_sel Ts)) selss0;
+          val conds = map (rapp obj) discs;
+          val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+          val branches' = map2 (curry Term.betapplys) branches branch_argss;
+        in
+          SOME (conds, branches')
+        end
+      else
+        NONE
+    | _ => NONE)
+  | _ => NONE);
+
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
 fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
@@ -787,19 +831,23 @@
         val notes' =
           [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
+        val ctr_sugar =
+          {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
+           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
+           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
+           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+           collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms};
       in
-        ({ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
-          nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
-          case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
-          split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
-          discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
-          collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms},
+        (ctr_sugar,
          lthy
          |> not rep_compat ?
             (Local_Theory.declaration {syntax = false, pervasive = true}
                (fn phi => Case_Translation.register
                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
-         |> Local_Theory.notes (notes' @ notes) |> snd)
+         |> Local_Theory.notes (notes' @ notes) |> snd
+         |> register_ctr_sugar dataT_name ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 12:52:21 2013 +0200
@@ -51,11 +51,6 @@
 val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
 fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
   strip_qnt_body @{const_name all} t)
-fun s_not @{const True} = @{const False}
-  | s_not @{const False} = @{const True}
-  | s_not (@{const Not} $ t) = t
-  | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
-  | s_not t = HOLogic.mk_not t
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
 fun invert_prems [t] = map s_not (HOLogic.disjuncts t)
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 12:52:21 2013 +0200
@@ -51,6 +51,7 @@
      nested_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
+  val s_not: term -> term
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
   val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ list ->
@@ -60,9 +61,8 @@
   val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
   val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ list -> typ ->
     term -> term
-  val fold_rev_corec_code_rhs: Proof.context -> (term -> term list -> 'a -> 'a) -> typ list ->
-    term -> 'a -> 'a
-  val simplify_bool_ifs: theory -> term -> term list
+  val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
+    typ list -> term -> 'a -> 'a
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list) * local_theory
@@ -139,6 +139,12 @@
 fun unexpected_corec_call ctxt t =
   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
 
+fun s_not @{const True} = @{const False}
+  | s_not @{const False} = @{const True}
+  | s_not (@{const Not} $ t) = t
+  | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not t = HOLogic.mk_not t
+
 fun factor_out_types ctxt massage destU U T =
   (case try destU U of
     SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
@@ -175,7 +181,7 @@
             val map' = mk_map (length fs) Us ran_Ts map0;
             val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
           in
-            list_comb (map', fs')
+            Term.list_comb (map', fs')
           end
         | NONE => raise AINT_NO_MAP t)
       | massage_map _ _ t = raise AINT_NO_MAP t
@@ -197,28 +203,32 @@
     massage_call
   end;
 
-(* TODO: also support old-style datatypes.
-   (Ideally, we would have a proper registry for these things.) *)
-fun case_of ctxt =
-  fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
-
 fun fold_rev_let_if_case ctxt f bound_Ts =
   let
-    fun fld t =
+    val thy = Proof_Context.theory_of ctxt;
+
+    fun fld conds t =
       (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
-      | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
+        (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
+      | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
+        fld (cond :: conds) then_branch o fld (s_not cond :: conds) else_branch
       | (Const (c, _), args as _ :: _) =>
-        let val (branches, obj) = split_last args in
-          (case fastype_of1 (bound_Ts, obj) of
-            Type (T_name, _) => if case_of ctxt T_name = SOME c then fold_rev fld branches else f t
-          | _ => f t)
+        let val n = num_binder_types (Sign.the_const_type thy c) in
+          (case fastype_of1 (bound_Ts, nth args (n - 1)) of
+            Type (s, Ts) =>
+            (case dest_case ctxt s Ts t of
+              NONE => f conds t
+            | SOME (conds', branches) =>
+              fold_rev (uncurry fld) (map (fn cond => cond :: conds) conds' ~~ branches))
+          | _ => f conds t)
         end
-      | _ => f t)
+      | _ => f conds t)
   in
-    fld
+    fld []
   end;
 
+fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
+
 fun massage_let_if_case ctxt has_call massage_leaf bound_Ts U =
   let
     val typof = curry fastype_of1 bound_Ts;
@@ -228,7 +238,7 @@
       (case Term.strip_comb t of
         (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
       | (Const (@{const_name If}, _), obj :: branches) =>
-        list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
+        Term.list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
       | (Const (c, _), args as _ :: _) =>
         let val (branches, obj) = split_last args in
           (case fastype_of1 (bound_Ts, obj) of
@@ -238,7 +248,7 @@
                 val branches' = map massage_rec branches;
                 val casex' = Const (c, map typof branches' ---> typof obj);
               in
-                list_comb (casex', branches') $ tap check_obj obj
+                Term.list_comb (casex', branches') $ tap check_obj obj
               end
             else
               massage_leaf t
@@ -273,7 +283,7 @@
             val map' = mk_map (length fs) dom_Ts Us map0;
             val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
           in
-            list_comb (map', fs')
+            Term.list_comb (map', fs')
           end
         | NONE => raise AINT_NO_MAP t)
       | massage_map _ _ t = raise AINT_NO_MAP t
@@ -292,7 +302,8 @@
             (case try (dest_ctr ctxt s) t of
               SOME (f, args) =>
               let val f' = mk_ctr Us f in
-                list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
+                Term.list_comb (f',
+                  map3 massage_call (binder_types (typof f')) (map typof args) args)
               end
             | NONE =>
               (case t of
@@ -312,16 +323,9 @@
   end;
 
 fun expand_ctr_term ctxt s Ts t =
-  (case fp_sugar_of ctxt s of
-    SOME fp_sugar =>
-    let
-      val T = Type (s, Ts);
-      val {ctrs = ctrs0, casex = case0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
-      val ctrs = map (mk_ctr Ts) ctrs0;
-      val casex = mk_case Ts T case0;
-    in
-      list_comb (casex, ctrs) $ t
-    end
+  (case ctr_sugar_of ctxt s of
+    SOME {ctrs, casex, ...} =>
+    Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
   | NONE => raise Fail "expand_ctr_term");
 
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
@@ -337,16 +341,8 @@
 fun massage_corec_code_rhs ctxt massage_ctr =
   massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
 
-fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb);
-
-fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
-  | add_conjuncts t = cons t;
-
-fun conjuncts t = add_conjuncts t [];
-
-fun simplify_bool_ifs thy =
-  Raw_Simplifier.rewrite_term thy @{thms bool_if_simps[THEN eq_reflection]} []
-  #> conjuncts #> (fn [@{term True}] => [] | ts => ts);
+fun fold_rev_corec_code_rhs ctxt f =
+  fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
 fun indexedd xss = fold_map indexed xss;
--- a/src/HOL/IMP/Compiler.thy	Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Wed Sep 25 12:52:21 2013 +0200
@@ -21,16 +21,16 @@
   where @{term i} is an @{typ int}.
 *}
 fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
-"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
+"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
 
 text {*
   The only additional lemma we need about this function 
   is indexing over append:
 *}
 lemma inth_append [simp]:
-  "0 \<le> n \<Longrightarrow>
-  (xs @ ys) !! n = (if n < size xs then xs !! n else ys !! (n - size xs))"
-by (induction xs arbitrary: n) (auto simp: algebra_simps)
+  "0 \<le> i \<Longrightarrow>
+  (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
+by (induction xs arbitrary: i) (auto simp: algebra_simps)
 
 subsection "Instructions and Stack Machine"