QuotMain.thy
changeset 94 ecfc2e1fd15e
parent 93 ec29be471518
child 95 8c3a35da4560
equal deleted inserted replaced
93:ec29be471518 94:ecfc2e1fd15e
   392         val rec_term = regularise t' rty rel lthy2;
   392         val rec_term = regularise t' rty rel lthy2;
   393         val lam_term = Term.lambda_name (x, v) rec_term
   393         val lam_term = Term.lambda_name (x, v) rec_term
   394       in
   394       in
   395         Const(@{const_name "All"}, at) $ lam_term
   395         Const(@{const_name "All"}, at) $ lam_term
   396       end
   396       end
       
   397   | ((Const (@{const_name "All"}, at)) $ P) =>
       
   398       let
       
   399         val (_, [al, _]) = dest_Type (fastype_of P);
       
   400         val ([x], lthy2) = Variable.variant_fixes [""] lthy;
       
   401         val v = (Free (x, al));
       
   402         val abs = Term.lambda_name (x, v) (P $ v);
       
   403       in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
   397   | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
   404   | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
   398       if (needs_lift rty T) then let
   405       if (needs_lift rty T) then let
   399         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
   406         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
   400         val v = Free (x', T);
   407         val v = Free (x', T);
   401         val t' = subst_bound (v, t);
   408         val t' = subst_bound (v, t);
   416         val rec_term = regularise t' rty rel lthy2;
   423         val rec_term = regularise t' rty rel lthy2;
   417         val lam_term = Term.lambda_name (x, v) rec_term
   424         val lam_term = Term.lambda_name (x, v) rec_term
   418       in
   425       in
   419         Const(@{const_name "All"}, at) $ lam_term
   426         Const(@{const_name "All"}, at) $ lam_term
   420       end
   427       end
       
   428   | ((Const (@{const_name "Ex"}, at)) $ P) =>
       
   429       let
       
   430         val (_, [al, _]) = dest_Type (fastype_of P);
       
   431         val ([x], lthy2) = Variable.variant_fixes [""] lthy;
       
   432         val v = (Free (x, al));
       
   433         val abs = Term.lambda_name (x, v) (P $ v);
       
   434       in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
   421   | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
   435   | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
   422   | _ => trm
   436   | _ => trm
   423 
   437 
   424 *}
   438 *}
   425 
   439 
   426 ML {*
   440 ML {*
   427   cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
   441   cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
   428   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
   442   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
   429   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
   443   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
   430   cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context})
   444   cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
       
   445   cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
   431 *}
   446 *}
   432 
   447 
   433 
   448 
   434 
   449 
   435 
   450 
  1125   apply (atomize(full))
  1140   apply (atomize(full))
  1126   apply (tactic {* foo_tac' @{context} 1 *})
  1141   apply (tactic {* foo_tac' @{context} 1 *})
  1127   done
  1142   done
  1128 
  1143 
  1129 thm list.induct
  1144 thm list.induct
  1130 
  1145 lemma list_induct2:
  1131 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
  1146   shows "(P []) \<Longrightarrow> (\<forall> a list. ((P list) \<longrightarrow> (P (a # list)))) \<Longrightarrow> \<forall>l :: 'a list. (P l)"
       
  1147   apply (rule allI)
       
  1148   apply (rule list.induct)
       
  1149   apply (assumption)
       
  1150   apply (auto)
       
  1151   done
       
  1152 
       
  1153 ML {* ObjectLogic.atomize (cprop_of @{thm list_induct2}) *}
       
  1154 ML {* (atomize_thm @{thm list_induct2}) *}
       
  1155 
       
  1156 ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct2}) *}
  1132 
  1157 
  1133 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *)
  1158 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *)
  1134 lemma RIGHT_RES_FORALL_REGULAR:
  1159 lemma RIGHT_RES_FORALL_REGULAR:
  1135   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
  1160   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
  1136   shows "All P ==> Ball R Q"
  1161   shows "All P ==> Ball R Q"
  1145   apply (metis COMBC_def Collect_def Collect_mem_eq a)
  1170   apply (metis COMBC_def Collect_def Collect_mem_eq a)
  1146   done
  1171   done
  1147 
  1172 
  1148 prove {*
  1173 prove {*
  1149  Logic.mk_implies
  1174  Logic.mk_implies
  1150    ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}),
  1175    ((prop_of li),
  1151    (prop_of li)) *}
  1176    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
  1152   apply (simp only: equiv_res_forall[OF equiv_list_eq])
  1177   apply (simp only: equiv_res_forall[OF equiv_list_eq])
  1153   thm LEFT_RES_FORALL_REGULAR
  1178   thm RIGHT_RES_FORALL_REGULAR
  1154   apply (rule LEFT_RES_FORALL_REGULAR)
  1179   apply (rule RIGHT_RES_FORALL_REGULAR)
  1155   prefer 2
  1180   prefer 2
  1156   apply (assumption)
  1181   apply (assumption)
  1157   apply (erule thin_rl)
       
  1158   apply (rule allI)
  1182   apply (rule allI)
  1159   apply (rule conjI)
       
  1160   prefer 2
       
  1161   apply (rule impI)
  1183   apply (rule impI)
  1162 
  1184   apply (rule impI)
  1163   apply (auto)
  1185   apply (assumption)
  1164   
  1186   done
  1165   apply (simp)
       
  1166   apply (thin_tac 1)
       
  1167 .
       
  1168   apply (simp)
       
  1169 
       
  1170   apply (unfold Ball_def)
       
  1171   apply (simp only: IN_RESPECTS)
       
  1172   apply (simp add: expand_fun_eq)
       
  1173 
       
  1174 
       
  1175   apply (tactic {* foo_tac' @{context} 1 *})
       
  1176   apply (atomize(full))
       
  1177   apply (simp)
       
  1178   prefer 2
       
  1179   apply (simp only: IN_RESPECTS)
       
  1180   apply (simp add:list_eq_refl)
       
  1181   apply (tactic {* foo_tac' @{context} 1 *})
       
  1182   prefer 2
       
  1183   apply (auto)
       
  1184   sorry
       
  1185 
  1187 
  1186 ML {*
  1188 ML {*
  1187   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
  1189   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
  1188 *}
  1190 *}
  1189 
  1191