Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finally merged the code of the versions of regularize and tested examples.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 30 Oct 2009 16:24:07 +0100
changeset 248 6ed87b3d358c
parent 247 e83a6e452843
child 250 1dd7f7f98040
Finally merged the code of the versions of regularize and tested examples.
FSet.thy file | annotate | diff | comparison | revisions
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/FSet.thy	Fri Oct 30 15:52:47 2009 +0100
+++ b/FSet.thy	Fri Oct 30 16:24:07 2009 +0100
@@ -169,9 +169,9 @@
 
 (* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list)"
+  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
 term map
 term fmap
@@ -309,6 +309,7 @@
 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
 by (simp add: list_eq_refl)
 
+(* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
@@ -319,16 +320,18 @@
 
 thm fold1.simps(2)
 thm list.recs(2)
+thm list.cases
+
 
 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
-(*  prove {* build_regularize_goal ind_r_a rty rel @{context} *}
+(*prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
          (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
          (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}
-  apply (tactic {* tac @{context} 1 *}) *)
+  apply (tactic {* tac @{context} 1 *})*)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
--- a/QuotMain.thy	Fri Oct 30 15:52:47 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 16:24:07 2009 +0100
@@ -447,106 +447,6 @@
 *}
 
 ML {*
-(* trm \<Rightarrow> new_trm *)
-fun regularise trm rty rel lthy =
-  case trm of
-    Abs (x, T, t) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of trm;
-        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
-        val rabs_term = (rabs $ res_term) $ lam_term;
-      in
-        rabs_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-      in
-        Term.lambda_name (x, v) rec_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "All"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
-  | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "Ex"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "Ex"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
-  | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
-  | _ => trm
-
-*}
-
-(* my version of regularise *)
-(****************************)
-
-(* some helper functions *)
-
-
-ML {*
 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
@@ -566,47 +466,51 @@
   | _ => f trm
 *}
 
-
-(* FIXME: assumes always the typ is qty! *)
 (* FIXME: if there are more than one quotient, then you have to look up the relation *)
 ML {*
-fun my_reg rel trm =
+fun my_reg lthy rel rty trm =
   case trm of
     Abs (x, T, t) =>
-       let 
-          val ty1 = fastype_of trm
-       in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    
-       end
-  | Const (@{const_name "All"}, ty) $ t =>
-       let 
+       if (needs_lift rty T) then
+         let
+            val rrel = tyRel T rty rel lthy
+         in
+           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
+         end
+       else
+         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
+  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
+       let
           val ty1 = domain_type ty
           val ty2 = domain_type ty1
+          val rrel = tyRel T rty rel lthy
        in
-         (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
+         if (needs_lift rty T) then
+           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+         else
+           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | Const (@{const_name "Ex"}, ty) $ t =>
-       let 
+  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
+       let
           val ty1 = domain_type ty
           val ty2 = domain_type ty1
+          val rrel = tyRel T rty rel lthy
        in
-         (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
+         if (needs_lift rty T) then
+           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+         else
+           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
+  | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
 
-
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
-  trm == new_trm
-*)
-
 text {* Assumes that the given theorem is atomized *}
 ML {*
   fun build_regularize_goal thm rty rel lthy =
      Logic.mk_implies
        ((prop_of thm),
-       (regularise (prop_of thm) rty rel lthy))
+       (my_reg lthy rel rty (prop_of thm)))
 *}
 
 ML {*
nominal2