--- a/QuotMain.thy Thu Oct 15 11:20:50 2009 +0200
+++ b/QuotMain.thy Thu Oct 15 11:25:25 2009 +0200
@@ -300,171 +300,6 @@
|> writeln
*}
-text {* tyRel takes a type and builds a relation that a quantifier over this
- type needs to respect. *}
-ML {*
-fun tyRel ty rty rel lthy =
- if ty = rty then rel
- else (case ty of
- Type (s, tys) =>
- let
- val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
- val ty_out = ty --> ty --> @{typ bool};
- val tys_out = tys_rel ---> ty_out;
- in
- (case (lookup (ProofContext.theory_of lthy) s) of
- SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
- | NONE => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
- )
- end
- | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
-*}
-
-ML {*
- cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
-*}
-
-definition
- Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
- "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-
-(* TODO: Consider defining it with an "if"; sth like:
- Babs p m = \<lambda>x. if x \<in> p then m x else undefined
-*)
-
-ML {*
-fun needs_lift (rty as Type (rty_s, _)) ty =
- case ty of
- Type (s, tys) =>
- (s = rty_s) orelse (exists (needs_lift rty) tys)
- | _ => false
-
-*}
-
-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
-
-*}
-
-ML {*
- cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
-*}
-
-
-
-
-ML {*
-fun atomize_thm thm =
-let
- val thm' = forall_intr_vars thm
- val thm'' = ObjectLogic.atomize (cprop_of thm')
-in
- Simplifier.rewrite_rule [thm''] thm'
-end
-*}
-
-thm list.induct
-ML {* atomize_thm @{thm list.induct} *}
-
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
- trm == new_trm
-*)
-
-
text {* produces the definition for a lifted constant *}
ML {*
@@ -1153,6 +988,175 @@
apply (tactic {* foo_tac' @{context} 1 *})
done
+section {* handling quantifiers - regularize *}
+
+text {* tyRel takes a type and builds a relation that a quantifier over this
+ type needs to respect. *}
+ML {*
+fun tyRel ty rty rel lthy =
+ if ty = rty then rel
+ else (case ty of
+ Type (s, tys) =>
+ let
+ val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
+ val ty_out = ty --> ty --> @{typ bool};
+ val tys_out = tys_rel ---> ty_out;
+ in
+ (case (lookup (ProofContext.theory_of lthy) s) of
+ SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+ | NONE => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
+ )
+ end
+ | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
+*}
+
+ML {*
+ cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
+*}
+
+definition
+ Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+
+(* TODO: Consider defining it with an "if"; sth like:
+ Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+*)
+
+ML {*
+fun needs_lift (rty as Type (rty_s, _)) ty =
+ case ty of
+ Type (s, tys) =>
+ (s = rty_s) orelse (exists (needs_lift rty) tys)
+ | _ => false
+
+*}
+
+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
+
+*}
+
+ML {*
+ cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+*}
+
+
+
+
+ML {*
+fun atomize_thm thm =
+let
+ val thm' = forall_intr_vars thm
+ val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+ Simplifier.rewrite_rule [thm''] thm'
+end
+*}
+
+thm list.induct
+ML {* atomize_thm @{thm list.induct} *}
+
+(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
+ trm == new_trm
+*)
+
+
+
+
ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
prove {*
@@ -1251,7 +1255,7 @@
local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
thm card1_suc_r
-ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}
+(* ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}*)
(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
thm m1_lift